4.5. Second-order logic

In set theory, the powerset and exponentiation were set-valued 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 criteria for constructions of types in first-order logic: set theory sees them essentially well-determined by its own powerset and exponentiation, but they are not translatable as abbreviations in the initial theory. Thus allowing 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 5.

Second-order structures

Over a given list of sets, a first-order structure was a relation (or operation) with domains (and target) picked from this list. Now a second-order structure, is a relation (or operation) also using second-order constructed type(s) over them; its symbol is in the language of the second-order theory taking these sets as base types.
With only one involvement of a second-order type Y, some cases are uninteresting: Let us focus on the simplest case beyond this: the 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, whose list of types is made of (1) base type(s), and (2) types of structure(s) over these, with no claim of exhaustivity. This will suffice for most theories, which make no use of the other side Y\K of that unary relation on Y.
Elements of K are given their role as n-ary structures, by an evaluator symbol S (whose kind is that of those structures plus the argument of type K to be evaluated; its curried view gives the intended injection 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. Injectivity is expressed by the following axiom, separating K by S: This pack components: a type, a structure and an axiom, to be added to a theory T, plays the role of a structure in the sense of how it modifies the category of models: it has We mentioned that second-order structures with variables in base types and values in second-order types, are just a curried view on first-order structures; but when the involved second-order types are mere types of structures with no claim of exhaustivity, it is no more a priori necessary for such curried forms of first-order structures to admit these types as targets, thus making them have a given type as target constitutes an implicit sort of axiom beyond the mere data of a first-order structure symbol.

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 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 :

∀(parameters), ∃AK, ∀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 scheme, admitting more models) to the strongest (wider comprehension scheme, 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.

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 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 K for variables under ∀ at their root. The method is to replace each such axiom by a scheme of axioms, one for each defining expression.
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 all bound variables in F are of base types (none of type K). Comprehension axioms whose formulas also accept parameters of type K eliminate some incomplete interpretations of K 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 K, by another comprehension axiom whose more complex formula without K is obtained by substitution. For this quality of "cleaning up without strengthening", comprehension schemes with such parameters are usually prefered to those without.

Henkin semantics

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

Set theoretical interpretations

The integration of first-order theories in a set theory, initially described in 1.3, 1.7, 3. (algebra) and 4.2, 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. 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
4.7. Ordinals and cardinals
4.8. Undecidability of the axiom of choice
4.9. Second-order arithmetic
4.10. The Incompleteness Theorem