In formal logic, nonfirstorderizability is the inability of a natural-language statement to be adequately captured by a formula of first-order logic. Specifically, a statement is nonfirstorderizable if there is no formula of first-order logic which is true in a model if and only if the statement holds in that model. Nonfirstorderizable statements are sometimes presented as evidence that first-order logic is not adequate to capture the nuances of meaning in natural language.
The term was coined by George Boolos in his paper "To Be is to Be a Value of a Variable (or to Be Some Values of Some Variables)".[1] Quine argued that such sentences call for second-order symbolization, which can be interpreted as plural quantification over the same domain as first-order quantifiers use, without postulation of distinct "second-order objects" (properties, sets, etc.).
A standard example is the Geach–Kaplan sentence: "Some critics admire only one another." If Axy is understood to mean "x admires y," and the universe of discourse is the set of all critics, then a reasonable translation of the sentence into second order logic is:
That this formula has no first-order equivalent can be seen by turning it into a formula in the language of arithmetic . Substitute the formula for Axy. The result,
A model of a formal theory of arithmetic, such as first-order Peano arithmetic, is called standard if it only contains the familiar natural numbers 0, 1, 2, ... as elements. The model is called non-standard otherwise. Therefore, the formula given above is true only in non-standard models, because, in the standard model, the set X must contain all available numbers 0, 1, 2, .... In addition, there is a set X satisfying the formula in every non-standard model.
Let us assume that there is a first-order rendering of the above formula called E. If were added to the Peano axioms, it would mean that there were no non-standard models of the augmented axioms. However, the usual argument for the existence of non-standard models would still go through, proving that there are non-standard models after all. This is a contradiction, so we can conclude that no such formula E exists in first-order logic.
There is no formula A in 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.[2] Suppose there is a formula A which is true in all and only models with finite domains. We can express, for any positive integer n, the sentence "there are at least n elements in the domain". For a given n, call the formula expressing that there are at least n elements Bn. For example, the formula B3 is: