4.6. 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
- Monadic second-order logic describes theories with only one type X
called the base type, and its powerset, RelX(1).
- Full second-order logic admits a list of base types, and the full type of
structures of every kind over them, each of which is the set of all structures of that
kind with nonzero arity over base types. If there is only one base type X, these are
RelX(n) and OpX(n)
for every n∈ℕ*. This allows quantifiers on all variable structures ranging over all
structures of a chosen kind over base types. A full type of structures is said to be second-order
constructed from base types, which differs from first-order constructions like the powerset differs from operators complying
to the set generation principle.
Higher-order logic allows more types which can be listed by
construction order, from a list of base types to successively constructed
types, either first-order or second-order constructions (which amount to a powerset
or an exponentiation, done after a finitary product for arities >1).
We saw two natural second-order theories: arithmetic, and the concept of
Another one is geometry, which will be the object of section 5.
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 full type(s) of structures over them; its
symbol is in the language of the second-order theory taking these sets as base types.
Second-order structures given as parts of constructions are "non-structuring"
(like connectives and equality). Those with only one full type of structures as target
are mere curried views of first-order structures.
In practice (for geometry), the only useful second-order structures are unary
relations on some full type of structures Y. First-order logic cannot express
the exhaustivity of Y, but can bypass Y to describe any unary relation
there as a type P meant as a subset of Y, and called a type of structures.
This will usually suffice, as the other side Y\P is not explicitly needed.
Elements of P 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 P to be evaluated; its
curried view gives the intended injection from P 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 P by S:
This pack of 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
- For a relation : ∀k,k'∈P, (∀x1,...,xn,
⇔ (x1,..., xn)∈k')
⇒ k = k' (axiom of extensionality)
- For an operation :
⇒ k = k' (axiom of effectiveness)
A theory whose list of types is made of base types and types of structures
over these (with no claim of fullness), forms a weak second-order
- Enough structures to prevent any new symmetry: the above axiom
requests the evaluator to be «structuring enough» over P to prevent,
for any isomorphism between 2 models of T, any multiplicity of
extensions to interpretations of P forming isomorphisms between
- Not «enough axioms» to "define" (essentially determine) the extension
of the model, in the sense that, unlike in constructions, it does not ensure the
existence of an extension of any isomorphism to interpretations of P;
not «too much axioms», so the theory remains consistent, with existing models.
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), ∃A∈P, ∀x∈X,
x ∈ A ⇔ F(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
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.
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
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
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,
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
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.
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.
- Each of bare arithmetic, Presburger arithmetic and geometry is both logically and semantically complete.
- First-order versions of them are semantically incomplete, with
non-standard models elementarily equivalent but not isomorphic to
- Full arithmetic and set theories are logically incomplete, though full arithmetic
is semantically complete.
Set theory and foundations
1. First foundations of
2. Set theory (continued)
3. Algebra 1
4. Model Theory
4.2. The Completeness Theorem
4.3. Non-standard models of Arithmetic
4.4. Development of theories
4.6. Second-order logic
4.8. Ordinals and cardinals
4.9. Undecidability of the axiom of
4.11. The Incompleteness