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
- 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 all
second-order constructed types from them, each of which is the set of all structures
of a given kind with nonzero arity over them: from one base type X, these are
for all n∈ℕ*. This means to allow quantifiers on variable structures over base types,
but may also serve to conceive new kinds of structures.
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 (powerset or an exponentiation,
to be done after a finitary product to serve arities >1).
We saw two natural examples of second-order theory: arithmetic and the concept of
Another one is geometry, which will be the object of section 5.
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).
- For a relation : ∀k,k'∈K, (∀x1,...,xn,
⇔ (x1,..., xn)∈k')
⇒ k = k'
- For an operation :
⇒ k = k'
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), ∃A∈K, ∀x∈X,
x ∈ A ⇔ F(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
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.
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.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,
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
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: 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.
- Presburger arithmetic
and geometry are 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. How theories develop
4.5. Second-order logic
4.6. Well-foundedness and ordinals
4.7. Undecidability of the axiom of
4.9. The Incompleteness