Cantor's diagonal argument is a proof that there is no one-to-one correspondence between the natural numbers and the real numbers. It is typically expressed in the language of set theory or first-order logic, and is not directly related to finite model theory.

However, it is possible to use Ehrenfeucht-Fraïssé games to prove the uncountability of a set, which is a concept related to Cantor's diagonal argument. This involves constructing a game between two players, where one player tries to show that a set is countable by constructing a one-to-one correspondence between the set and the natural numbers, while the other player tries to show that the set is uncountable by showing that no such correspondence exists.

If a formal system can express Cantor's Diagonal Theory, it means that the system is able to reason about infinite sets. In that sense, it is beyond the scope of finite model theory, which is concerned with systems that reason about finite structures. Cantor's Diagonal Theory is used to prove that there are infinite sets that cannot be put into a one-to-one correspondence with the natural numbers. This result implies the existence of uncountable sets, which are infinite sets that are too large to be put into a one-to-one correspondence with the natural numbers. Therefore, a system that can express Cantor's Diagonal Theory is capable of reasoning about infinite structures and is not limited to the scope of finite model theory.