Second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies only variables that range over individuals ; second-order logic, in addition, quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not is true. Second-order logic also includes quantification over sets, functions, and other variables. Both first-order and second-order logic use the idea of a domain of discourse. The domain is a set over which individual elements may be quantified.
Examples
First-order logic can quantify over individuals, but not over properties. That is, we can take an atomic sentence like Cube and obtain a quantified sentence by replacing the name with a variable and attaching a quantifier:However, we cannot do the same with the predicate. That is, the following expression:
is not a sentence of first-order logic, but this is a legitimate sentence of second-order logic. Here, P is a predicate variable and is semantically a set of individuals.
As a result, second-order logic has greater expressive power than first-order logic. For example, there is no way in first-order logic to identify the set of all cubes and tetrahedrons. But the existence of this set can be asserted in second-order logic as:
We can then assert properties of this set. For instance, the following says that the set of all cubes and tetrahedrons does not contain any dodecahedrons:
Second-order quantification is especially useful because it gives the ability to express reachability properties. For example, if Parent denotes that x is a parent of y, then first-order logic cannot express the property that x is an ancestor of y. In second-order logic we can express this by saying that every set of people containing y and closed under the Parent relation contains x:
It is notable that while we have variables for predicates in second-order-logic, we don't have variables for properties of predicates. We cannot say, for example, that there is a property Shape that is true for the predicates P Cube, Tet, and Dodec. This would require third-order logic.
Syntax and fragments
The syntax of second-order logic prescribes which expressions are well formed formulas. In addition to the syntax of first-order logic, second-order logic includes many new sorts of variables. These are:- A sort of variables that range over sets of individuals. If S is a variable of this sort and t is a first-order term then the expression t ∈ S is an atomic formula. Sets of individuals can also be viewed as unary relations on the domain.
- For each natural number k there is a sort of variables that ranges over all k-ary relations on the individuals. If R is such a k-ary relation variable and t1,...,tk are first-order terms then the expression R is an atomic formula.
- For each natural number k there is a sort of variables that ranges over all functions taking k elements of the domain and returning a single element of the domain. If f is such a k-ary function variable and t1,...,tk are first-order terms then the expression f is a first-order term.
It's possible to forgo the introduction of function variables in the definition given above because an n-ary function variable can be represented by a relation variable of arity n+1 and an appropriate formula for the uniqueness of the "result" in the n+1 argument of the relation.
Monadic second-order logic is a restriction of second-order logic in which only quantification over unary relations is allowed. Quantification over functions, owing to the equivalence to relations as described above, is thus also not allowed. The second-order logic without these restrictions is sometimes called full second-order logic to distinguish it from the monadic version. Monadic second-order logic is particularly used in the context of Courcelle's theorem, an algorithmic meta-theorem in graph theory. The MSO theory of the complete infinite binary tree is decidable. By contrast, full second-order logic over any infinite set can interpret the true second-order arithmetic.
Just as in first-order logic, second-order logic may include non-logical symbols in a particular second-order language. These are restricted, however, in that all terms that they form must be either first-order terms or second-order terms.
A formula in second-order logic is said to be of first-order if its quantifiers range only over variables of first order, although it may have free variables of second order. A formula is one additionally having some existential quantifiers over second-order variables, i.e., where is a first-order formula. The fragment of second-order logic consisting only of existential second-order formulas is called existential second-order logic and abbreviated as ESO, as, or even as ∃SO. The fragment of formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for any k > 0 by mutual recursion: has the form, where is a formula, and similar, has the form, where is a formula.
Semantics
The semantics of second-order logic establish the meaning of each sentence. Unlike first-order logic, which has only one standard semantics, there are two different semantics that are commonly used for second-order logic: standard semantics and Henkin semantics. In each of these semantics, the interpretations of the first-order quantifiers and the logical connectives are the same as in first-order logic. Only the ranges of quantifiers over second-order variables differ in the two types of semantics.In standard semantics, also called full semantics, the quantifiers range over all sets or functions of the appropriate sort. A model with this condition is called a full model, and these are the same as models in which the range of the second-order quantifiers is the powerset of the model's first-order part. Thus once the domain of the first-order variables is established, the meaning of the remaining quantifiers is fixed. It is these semantics that give second-order logic its expressive power, and they will be assumed for the remainder of this article.
Leon Henkin defined an alternative kind of semantics for second-order and higher-order theories, in which the meaning of the higher-order domains is partly determined by an explicit axiomatisation, drawing on type theory, of the properties of the sets or functions ranged over. Henkin semantics is a kind of many-sorted first-order semantics, where there are a class of models of the axioms, instead of the semantics being fixed to just the standard model as in the standard semantics. A model in Henkin semantics will provide a set of sets or set of functions as the interpretation of higher-order domains, which may be a proper subset of all sets or functions of that sort. For his axiomatisation, Henkin proved that Gödel's completeness theorem and compactness theorem, which hold for first-order logic, carry over to second-order logic with Henkin semantics. Since also the Löwenheim–Skolem theorems hold for Henkin semantics, Lindström's theorem imports that Henkin models are just disguised first-order models.
For theories such as second-order arithmetic, the existence of non-standard interpretations of higher-order domains isn't just a deficiency of the particular axiomatisation derived from type theory that Henkin used, but a necessary consequence of Gödel's incompleteness theorem: Henkin's axioms can't be supplemented further to ensure the standard interpretation is the only possible model. Henkin semantics are commonly used in the study of second-order arithmetic.
Jouko Väänänen argued that the distinction between Henkin semantics and full semantics for second-order logic is analogous to the distinction between provability in ZFC and truth in V, in that the former obeys model-theoretic properties like the Löwenheim–Skolem theorem and compactness, and the latter has categoricity phenomena. For example, "we cannot meaningfully ask whether the as defined in is the real. But if we reformalize inside, then we can note that the reformalized ... has countable models and hence cannot be categorical."
Expressive power
Second-order logic is more expressive than first-order logic. For example, if the domain is the set of all real numbers, one can assert in first-order logic the existence of an additive inverse of each real number by writing but one needs second-order logic to assert the least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum. If the domain is the set of all real numbers, the following second-order sentence expresses the least upper bound property:Here, the part of the first line involving represents the assumption that is nonempty. The rest of the first line represents the assumption that is bounded from above. The second line expresses the existence of a least upper bound. It asserts that is an upper bound and that, if any number is also an upper bound, then. Any ordered field that satisfies this property is isomorphic to the real number field. On the other hand, the set of first-order sentences valid in the reals has arbitrarily large models due to the compactness theorem. Thus the least-upper-bound property cannot be expressed by any set of sentences in first-order logic.
In second-order logic, it is possible to write formal sentences that say “the domain is finite” or “the domain is of countable cardinality.” To say that the domain is finite, use the sentence that says that every surjective function from the domain to itself is injective. To say that the domain has countable cardinality, use the sentence that says that there is a bijection between every two infinite subsets of the domain. It follows from the compactness theorem and the upward Löwenheim–Skolem theorem that it is not possible to characterize finiteness or countability, respectively, in first-order logic.
Certain fragments of second-order logic like ESO are also more expressive than first-order logic even though they are strictly less expressive than the full second-order logic. ESO also enjoys translation equivalence with some extensions of first-order logic that allow non-linear ordering of quantifier dependencies, like first-order logic extended with Henkin quantifiers, Hintikka and Sandu’s independence-friendly logic, and Väänänen’s dependence logic.