5.2. Second-order logic
Second-order constructions allow
them forms new logical
frameworks for theories:
- 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. 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.
-
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).
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 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
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.
- 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
standard ones.
- Full arithmetic and set theories are logically incomplete, though full arithmetic
is semantically complete.
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
More philosophical notes :