4.5. Second-order logic

In set theory, the powerset and exponentiation (and infinitary products), were the only set construction operators not justified by the set generation principle. Similarly in model theory, the powerset and the exponentiation of types, are sorts of «constructions» failing at our stated criteria for constructions of types in first-order logic: set theory sees them essentially well-determined, but they cannot be reduced to abbreviations of uses of the initial theory. Thus allowing them forms new logical frameworks for theories: Higher-order theories can be translated as second-order theories by taking as base types a copy of all types used in any second-order construction, and giving for each one 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 examples of second-order theory: arithmetic and the concept of standard universe. Another one is geometry, which will be the object of section 5.

Second-order structures

A first-order structure over a given list of sets, was a choice of operation or relation between them. Now a second-order structure, is an operation or relation using some second-order constructed type(s) Y over them (constants in Y are first-order structures of type Y; second-order structures already given to form the second-order constructions are "non-structuring"). It thus belongs to the second-order theory taking these sets as base types.
Let us focus on the simple case of a unary relation on a second-order type Y. Like with the construction of a subset from a unary relation, it can be presented as a type K with a structure of injection from K to Y, giving K the role of a subset of Y. Now first-order logic cannot express the exhaustivity of Y, but can bypass the use of Y to describe K in the following form called a weak second-order theory. This will suffice for most theories, which make no use of the other side Y\K of that unary relation on Y.
The role of type K as a set of some n-ary structures, is given by one structure symbol (interpreter) S of that kind plus one argument of type K: the curried view interprets it as a function from K to Y. To reflect this role, S(k, x1,...,xn) will be abbreviated as (x1,...,xn)∈k if a relation, or as k(x1,...,xn) if an operation. Its injectivity is expressed by the axiom of extensionality, separating K by S: Such a type with this structure and this axiom plays the role of a structure in the sense of how adding this pack of components to a theory T modifies its category of models, having «enough structures» to ensure, for any isomorphism between 2 models of T, the uniqueness of its extension to the additional type to form an isomorphism between extended models (absence of new symmetry), but not «enough axioms» to ensure its existence like in a construction (this "structure" remains usually "undefined" as axioms do not essentially determine this extension as unique up to isomorphism).

Translating second-order theories to first-order logic

Let us focus on the case of only one second-order type Y for simplicity, but the generalization is straightforward.
The concept of weak second-order theory can serve as an incomplete scheme for second-order constructions, translating second-order theories to first-order ones. What misses is the possibility to fully express by first-order axioms (beyond the case of finite sets), the wish that K exhausts the intended type Y of structures of that kind, i.e. that our injection from K to Y is surjective. Still it can be partially expressed by axioms making K 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 (the case of exponentiation is similar, replacing ⇔ by =):

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

The strength of this formalization depends on the chosen "definability" concept: what kind of formulas may F be. The main options will be reviewed from the weakest (a restricted comprehension scheme, admitting more models) to the strongest (wider comprehension scheme, more selective on models).
While first-order logic has a clear concept of provability, second-order logic can only get one from there, that is the provability in a first-order translated version of a theory. Stronger options may give a wider range of theorems than weaker ones.

First-order definable structures

A weak method, already used for arithmetic, bypasses K by letting a variable structure of its type range over all those defined by expressions with base type variables. It is only applicable to such theories without second-order structure, only using K for variables under ∀ at the root of axioms. The method is to replace each such axiom by a schema of axioms, one for each expression defining that variable.
But the direct use of K can give more means to express and develop theories, with the same proving strength obtained by the comprehension axioms where F can only bound base type variables (none of type K). Admitting parameters of type K eliminates some incomplete interpretations of K but still allows the minimal one, that is the set of all such structures defined with base type variables. Indeed any comprehension axiom with parameters in K, is ensured to be true for each tuple of values of parameters each defined without K, by another comprehension axiom whose more complex formula without K is obtained by substitution. Therefore such parameters are usually accepted in the scheme for elegance.

Henkin semantics

Admitting bound second-order variables (= of type K) in comprehension axioms, completes the range of those which first-order logic can express with these types : the base types and the second-order ones (K). These requirements transcend any concept of «definable structures» or other conceivable intrinsic property of the elements of K, by the use K itself in the defining expressions of the structures which K must contain.

Set theoretical interpretations

The integration of first-order theories in a set theory, initially described in 1.3 and 1.7, 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 parameters taking any value in the universe and bound variables ranging inside any set, are implicitly given by the definition of the set builder in our formalism. Viewed by that set theory seeing its own universe as fixed, this determines the interpretations of second-order types from those of the base type (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 proving power of set theory converted to a first-order theory (as in 1.10), but this power depends on a chosen axiomatic set theory. There is no end to the possible power of set theories as sources of provability in second-order logic, as (by the incompleteness theorem) there can be no most powerful algorithmic concept of proof for arithmetic : it is always possible to find better ones.

Our set theory with powerset, infinity and choice, which is most convenient to develop all ordinary mathematics, is quite powerful (the same as Mac Lane set theory). As a little step further, Zermelo set theory adds comprehension with bound variables over the universe. Much larger leaps in power come by stating 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 its union U, which is the smallest standard model of Zermelo and Mac Lane set theories, leads to the existence of many more sets beyond it, namely all ℘n(U). Zermelo-Frankel set theory not only does this, but 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: theories which are logically incomplete by the weakest algorithm remain logically incomplete by any stronger ones, which may reduce the range of undecidability but never eliminate it.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Non-standard models of Arithmetic
4.4. How theories develop
4.5. Second-order logic
4.6. Well-foundedness and ordinals
4.7. Undecidability of the axiom of choice
4.8. Second-order arithmetic
4.9. The Incompleteness Theorem