Second-order logic

In mathematical logic, second-order logic differs from first-order logic in that it allows quantification over subsets of a domain, or functions from the domain into itself, rather than only over individual members of the domain. Thus, 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 of the real numbers:

and insert in place of the dots a statement that if A is nonempty and has an upper bound in R then A has a least upper bound in R.

Why second-order logic is not reducible to first-order logic

An optimist might attempt to reduce second-order logic to first-order logic in the following way. Expand the domain from the set of all real numbers to the union of that set with the set of all sets of real numbers. Add a new binary predicate to the language: the membership relation. Then sentences that were second-order become first-order.

But notice that the domain was asserted to include all sets of real numbers. That requirement has not been reduced to a first-order sentence! But might there be some way to accomplish the reduction? The classic Löwenheim-Skolem theorem entails that there is not. That theorem implies that there is some countably infinite subset of R, whose members we will call internal numbers, and some countably infinite set of sets of internal numbers, whose members we will call "internal sets", such that the domain consisting of internal numbers and internal sets satisfies all of the first-order sentences satisfied by the domain of real-numbers-and-sets-of-real-numbers. In particular, it satisfies a sort of least-upper-bound axiom that says, in effect:

Every nonempty internal set that has an internal upper bound has a least internal upper bound.

Countability of the set of all internal numbers (in conjunction with the fact that those form a densely ordered set) necessarily implies that that set does not satisfy the full least-upper-bound axiom. Countability of the set of all internal sets necessarily implies that is not the set of all subsets of the set of all internal numbers (since Cantor's theorem implies that the set of all subsets of a countably infinite set is an uncountably infinite set).

Yet another profound difference between first-order and second-order logic is the topic of the next section.

Second-order logic lacks soundness and completeness theorems

It is a corollary of Gödel's incompleteness theorem that one cannot have any notion of provability of second-order formulas that simultaneously satisfies these three desiderata:

• (Soundness) Every provable second-order sentence is universally valid, i.e., true in all domains.

• (Completeness) Every universally valid second-order formula is provable.

• ("Effectiveness") There is a proof-checking algorithm. (This third condition is often taken so much for granted that it is not explicitly stated.)

This is sometimes expressed by saying that second-order logic does not admit a proof theory.

In this respect second-order logic differs from first-order logic.