Editing Nonfirstorderizability (section)

=== Finiteness of the domain ===
There is no formula {{mvar|A}} in [[First-order logic#Equality and its axioms|first-order logic with equality]] which is true of all and only models with finite domains. In other words, there is no first-order formula which can express "there is only a finite number of things".

This is implied by the [[compactness theorem]] as follows.<ref>{{cite book |title=Intermediate Logic |publisher=Open Logic Project |pages=235 |url=https://builds.openlogicproject.org/courses/intermediate-logic/il-screen.pdf |access-date=21 March 2022}}</ref> Suppose there is a formula {{mvar|A}} which is true in all and only models with finite domains. We can express, for any positive integer {{mvar|n}}, the sentence "there are at least {{mvar|n}} elements in the domain". For a given {{mvar|n}}, call the formula expressing that there are at least {{mvar|n}} elements {{mvar|B<sub>n</sub>}}. For example, the formula {{mvar|B<sub>3</sub>}} is:
<math display="block">\exists x \exists y \exists z (x \neq y \wedge x \neq z \wedge y \neq z)</math>
which expresses that there are at least three distinct elements in the domain. Consider the infinite set of formulae
<math display="block">A, B_2, B_3, B_4, \ldots</math>
Every finite subset of these formulae has a model: given a subset, find the greatest {{mvar|n}} for which the formula {{mvar|B<sub>n</sub>}} is in the subset. Then a model with a domain containing {{mvar|n}} elements will satisfy {{mvar|A}} (because the domain is finite) and all the {{mvar|B}} formulae in the subset. Applying the compactness theorem, the entire infinite set must also have a model. Because of what we assumed about {{mvar|A}}, the model must be finite. However, this model cannot be finite, because if the model has only {{mvar|m}} elements, it does not satisfy the formula {{mvar|B<sub>m+1</sub>}}. This contradiction shows that there can be no formula {{mvar|A}} with the property we assumed.