Second-order logic

Second-order logic also includes quantification over sets, functions, and other variables (see section below).

For example, there is no way in first-order logic to identify the set of all cubes and tetrahedrons.

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.

We cannot say, for example, that there is a property Shape(P) that is true for the predicates P Cube, Tet, and Dodec.

The syntax of second-order logic tells which expressions are well formed formulas.

These are: Each of the variables just defined may be universally and/or existentially quantified over, to build up formulas.

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 (S2S) is decidable.

formulas is defined dually, it is called universal second-order logic.

Only the ranges of quantifiers over second-order variables differ in the two types of semantics.

[3] 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 (1950) 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.

[4] 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.

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 Lowenheim-Skolem theorem and compactness, and the latter has categoricity phenomena.

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 fact, every real-closed field satisfies the same first-order sentences in the signature

Several deductive systems can be used for second-order logic, although none can be complete for the standard semantics (see below).

Each of these systems is sound, which means any sentence they can be used to prove is logically valid in the appropriate semantics.

But notice that the domain was asserted to include all sets of real numbers.

This example illustrates that the question of whether a sentence in second-order logic is consistent is extremely subtle.

It is a corollary of Gödel's incompleteness theorem that there is no deductive system (that is, no notion of provability) for second-order formulas that simultaneously satisfies these three desired attributes:[d] This corollary is sometimes expressed by saying that second-order logic does not admit a complete proof theory.

[6] As mentioned above, Henkin proved that the standard deductive system for first-order logic is sound, complete, and effective for second-order logic with Henkin semantics, and the deductive system with comprehension and choice principles is sound, complete, and effective for Henkin semantics using only models that satisfy these principles.

[citation needed] This rejection was actively advanced by some logicians, most notably W. V. Quine.

Quine advanced the view[citation needed] that in predicate-language sentences like Fx the "x" is to be thought of as a variable or name denoting an object and hence can be quantified over, as in "For all things, it is the case that .

Boolos furthermore points to the claimed nonfirstorderizability of sentences such as "Some critics admire only each other" and "Some of Fianchetto's men went into the warehouse unaccompanied by anyone else", which he argues can only be expressed by the full force of second-order quantification.

The expressive power of various forms of second-order logic on finite structures is intimately tied to computational complexity theory.

A string w = w1···wn in a finite alphabet A can be represented by a finite structure with domain D = {1,...,n}, unary predicates Pa for each a ∈ A, satisfied by those indices i such that wi = a, and additional predicates that serve to uniquely identify which index is which (typically, one takes the graph of the successor function on D or the order relation <, possibly with other arithmetic predicates).

This identification leads to the following characterizations of variants of second-order logic over finite structures: Relationships among these classes directly impact the relative expressiveness of the logics over finite structures; for example, if PH = PSPACE, then adding a transitive closure operator to second-order logic would not make it any more expressive over finite structures.