Template:Short description Template:TechIn 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)".<ref name="boolos-to-be">Template:Cite journal Reprinted in Template:Cite book</ref> 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.).
ExamplesEdit
Geach-Kaplan sentenceEdit
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: <math display="block">\exists X \big( (\exists x \neg Xx) \land \exists x,y (Xx \land Xy \land Axy) \land \forall x\, \forall y (Xx \land Axy \rightarrow Xy)\big)</math> In words, this states that there exists a collection of critics with the following properties: The collection forms a proper subclass of all the critics; it is inhabited (and thus non-empty) by a member that admires a critic that is also a member; and it is such that if any of its members admires anyone, then the latter is necessarily also a member.
That this formula has no first-order equivalent can be seen by turning it into a formula in the language of arithmetic. To this end, substitute the formula <math display="inline"> ( y = x + 1 \lor x = y + 1 ) </math> for Axy. This expresses that the two terms are successors of one another, in some way. The resulting proposition, <math display="block">\exists X \big( (\exists x \neg Xx) \land \exists x,y (Xx \land Xy \land (y = x + 1 \lor x = y + 1)) \land \forall x\, \forall y (Xx \land (y = x + 1 \lor x = y + 1) \rightarrow Xy)\big)</math> states that there is a set Template:Mvar with the following three properties:
- There is a number that does not belong to Template:Mvar, i.e. Template:Mvar does not contain all numbers.
- The set Template:Mvar is inhabited, and here this indeed immediately means there are at least two numbers in it.
- If a number Template:Mvar belongs to Template:Mvar and if Template:Mvar is either Template:Math or Template:Math, then Template:Mvar also belongs to Template:Mvar.
Recall 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 as elements (i.e., Template:Math). The model is called non-standard otherwise. The formula above is true only in non-standard models: In the standard model Template:Mvar would be a proper subset of all numbers that also would have to contain all available numbers (Template:Math), and so it fails. And then on the other hand, in every non-standard model there is a subset Template:Mvar satisfying the formula.
Let us now assume that there is a first-order rendering of the above formula called Template:Mvar. If <math>\neg E</math> 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 Template:Mvar exists in first-order logic.
Finiteness of the domainEdit
There is no formula Template:Mvar 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.<ref>Template:Cite book</ref> Suppose there is a formula Template:Mvar which is true in all and only models with finite domains. We can express, for any positive integer Template:Mvar, the sentence "there are at least Template:Mvar elements in the domain". For a given Template:Mvar, call the formula expressing that there are at least Template:Mvar elements Template:Mvar. For example, the formula Template:Mvar 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 Template:Mvar for which the formula Template:Mvar is in the subset. Then a model with a domain containing Template:Mvar elements will satisfy Template:Mvar (because the domain is finite) and all the Template:Mvar formulae in the subset. Applying the compactness theorem, the entire infinite set must also have a model. Because of what we assumed about Template:Mvar, the model must be finite. However, this model cannot be finite, because if the model has only Template:Mvar elements, it does not satisfy the formula Template:Mvar. This contradiction shows that there can be no formula Template:Mvar with the property we assumed.
Other examplesEdit
- The concept of identity cannot be defined in first-order languages, merely indiscernibility.<ref>Template:Cite SEP</ref>
- The Archimedean property that may be used to identify the real numbers among the real closed fields.
- The compactness theorem implies that graph connectivity cannot be expressed in first-order logic.Template:Clarify
See alsoEdit
- Definable set
- Branching quantifier
- Generalized quantifier
- Plural quantification
- Reification (linguistics)