5.2. Second-order logic

Second-order constructions allow them forms new logical frameworks for theories: Higher-order theories are reducible to second-order theories, by taking, as base types, copies of all types used in any second-order construction, then giving for each of those second-order constructed from others (such as Y = ℘(X)), the structure and axioms of a bijection identifying it (Y) with that actually constructed version (℘(X)).
We saw two natural second-order theories: arithmetic, and the concept of standard universe. Another one is geometry, which will be the object of section 6.

Translating second-order theories to first-order ones

Let us focus on the case of only one second-order type Y for simplicity, but the generalization is straightforward.
The above concept of weak second-order theory can serve as the minimal basis of an incomplete formalization simulating second-order constructions and theories into first-order logic. What misses is the possibility to fully express by first-order axioms (beyond the case of finite sets), the wish that P exhausts the intended type Y of structures of that kind, i.e. that our injection from P to Y is surjective. Still it can be partially expressed by axioms making P contain all such structures definable with parameters. In the case of the powerset they are called comprehension axioms, depending on a defining formula F with one distinguished free variable of type X :

∀(parameters), ∃AP, ∀xX, xAF(x, parameters).

The case of exponentiation is similar, replacing ⇔ by =.
The strength of this formalization depends on the chosen range of definability: what kind of formulas may F be. The main options will be reviewed from the weakest (a restricted comprehension schema, admitting more models) to the strongest (wider comprehension schema, more selective on models).
Only first-order logic has a clear, built-in concept of provability. Provability concepts for second-order logic can only be drawn from there, by conceiving provability for a second-order theory as given by that of some chosen first-order translated version of it. Stronger translations may induce a wider range of theorems than weaker ones.

Using first-order axiom schemas

A weak method, already used for arithmetic, bypasses P by letting a variable structure of its type range over all those defined by first-order expressions with only base type variables (bound variables as well as parameters). It is only applicable to such theories without second-order structure, and whose axioms only use P for variables under ∀ at their root. The method is to replace each such axiom by a schema of axioms, one for each defining expression.
But the direct use of P can give more means to express and develop theories, with the same proving strength obtained by the comprehension axioms where all bound variables in F are of base types (none of type P). Comprehension axioms whose formulas also accept parameters of type P eliminate some incomplete interpretations of P but still allow the minimal one, that is the set of all such structures defined with base type variables only. Indeed their truth is ensured there for each tuple of values of parameters each defined without P, by another comprehension axiom whose more complex formula without P is obtained by substitution. For this quality of "cleaning up without strengthening", comprehension schemas with such parameters are usually prefered to those without.

Henkin semantics

Admitting bound second-order variables (= of type P), completes the range of those comprehension axioms which first-order logic can express with these types : the base types and the second-order ones (P). This impredicative requirement, using P itself in the defining expressions of the structures which it requests P to contain, makes it transcend any concept of «definable structures» or other intrinsic property of the elements of P.

Set theoretical interpretations

The integration of first-order theories in a set theory, initially described in 1.3, 1.7, 3. (algebra) and 4.6, is naturally extensible to second-order theories using the set theoretical powerset and exponentiation operators. This expands the list of comprehension axioms beyond Henkin semantics, by letting more kinds of variables in formulas. Comprehension axioms with any values of parameters in the universe, and bound variables with range any set, are implicitly given by our definition of the set builder. Viewed by that set theory seeing its own universe as fixed, this determines the interpretations of second-order types from those of the base types (making any bijection between base types of 2 systems uniquely extensible as an isomorphism of the second-order constructions from them), but by Skolem's paradox, multiple non-isomorphic interpretations re-appear from an external viewpoint admitting a diversity of non-standard universes.

This is the most powerful kind of formalization for second-order logic, giving it the whole proving power of set theory (in the sense of its converted form as a first-order theory sketched in 1.10), but its precise power depends on the specific version (axioms list) of set theory that is chosen. There is no end to the possible power of set theories as sources of provability in second-order logic, as more generally there can be no most powerful algorithmic concept of proof for arithmetic (any good one can always be surpassed by a better one, as the incompleteness theorem will show).

Our set theory with powerset, infinity and choice, which is most convenient to develop all ordinary mathematics, is quite powerful (it is equivalent to Mac Lane set theory). As a little step further, Zermelo set theory adds to this comprehension with bound variables over the universe. Much larger leaps in power come by adding to axioms the existence of more sets or objects, starting with what may be abusively written (while ℘ is not a function) as the recursive sequence (℘n(ℕ))n∈ℕ. Indeed once its union U, which is the smallest standard model of Zermelo and Mac Lane set theories, is accepted as a set, this leads to the existence of many more sets beyond it, namely all ℘n(U). Zermelo-Frankel set theory not only does this, but, as we shall see, it goes so much further after this, that the structure of the resulting hierarchy of powersets transcends any possible description.

Completeness properties of theories

Semantic completeness

A theory is called semantically complete if all its models are isomorphic to each other.

Löwenheim-Skolem theorem. Any first-order theory with an infinite model, has multiple non-equinumerous ones, thus is semantically incomplete.

Sketch of proof for a countable theory. The completeness theorem gives it a countable model. An extended version of this theorem to the case of uncountable languages (which requires more work on infinities, using AC to apply to all cases), gives it uncountable models, as adding an uncountable set of constants with the axioms making their interpretation injective, preserves its consistency. ∎

Semantic completeness takes a more interesting sense for a second-order theory with an infinite model, interpreted in a fixed universe : the claim that all its standard models (= respecting the powersets) are isomorphic to each other.

Logical completeness

A theory is called logically complete if all its ground formulas are decidable from its axioms.
This makes direct sense in first-order logic, meaning that all models fall into a single class of elementary equivalence. The news is its meaningfulness for the main useful second order theories, i.e. its independence from the choice of first-order expression: logically incomplete theories in the sense of the weakest algorithm (with first-order definable structures) remain logically incomplete by any stronger ones (such as from axiomatic set theories), as their range of undecidable formulas (thus their range of elementary equivalence classes of models) can be shrinked but never eliminated, even among formulas which only use first-order types of variables.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Arithmetic and first-order foundations
5. Second-order foundations
5.1. Second-order structures and invariants
5.2. Second-order logic
5.3. Well-foundedness
5.4. Ordinals and cardinals
5.5. Undecidability of the axiom of choice
5.6. Second-order arithmetic
5.7. The Incompleteness Theorem
More philosophical notes :
Gödelian arguments against mechanism : what was wrong and how to do instead
Philosophical proof of consistency of the Zermelo-Fraenkel axiomatic system