Nonfirstorderizability
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)".[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.).
Examples
Geach-Kaplan sentence
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: 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 for Axy. This expresses that the two terms are successors of one another, in some way. The resulting proposition, 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 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 domain
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.[2] 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: which expresses that there are at least three distinct elements in the domain. Consider the infinite set of formulae 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 examples
- The concept of identity cannot be defined in first-order languages, merely indiscernibility.[3]
- 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 also
- Definable set
- Branching quantifier
- Generalized quantifier
- Plural quantification
- Reification (linguistics)