1.11. Second-order universal quantifiersFirst-order logic will allow the use of variable structure
symbols as abbreviations of fixed expressions defining these structures, but this way can only bind them
on some restricted ranges respectively determined by these expressions (see 1.B).
Now let us call second-order quantifier, a quantifier binding a variable structure symbol over
the range of all structures of its symbol
type. This may either be conceived as the range of all definable ones (with all possible
defining expressions whose free variables may have any list of parameters beyond the given
arguments) or as the full set theoretical range (of all such operations which
exist in the universe, relating the given interpreted types).
Using second-order quantifiers means working in some wider logical framework such as
some version of second-order logic (described in part 5),
depending on details.
As we shall do for the axioms of equality (below) and for set theory (in 2.1 and 2.2), a theory
may be first expressed in second-order logic for intuitive reasons, before formally interpreting
this as a convenient meta level tool to abbreviate a first-order formalization, as follows.
Let T be
a first-order theory, T' its extension by a structure symbol s
(without further axiom) and F a statement of T' (in first-order logic)
also denoted F(s) when seen as a formula of T using the
variable structure symbol s in second-order logic.
Second-order Universal Introduction. If T'⊢F then T
entails the second-order statement (∀s, F(s)).
This holds for any model and the full set theoretical range of s, independently of
the universe in which models and structures s are searched for.
Second-order Universal Elimination. Once a second-order statement
(∀s, F(s)) is accepted in a theory T,
it is manifested in first-order logic as a schema of statements,
that is an infinite list of statements of the form (∀parameters, F(s)) for each
possible replacement of s by a defining expression with parameters.
Applying second-order universal elimination after second-order universal introduction,
means deducing from T a schema of theorems, each one deducible
in first-order logic by replacing s by its respective definition in the original proof.
Incompleteness of second-order logic
The above rules of proof, which will suffice for our needs, are clearly sound,
but unlike first-order logic, second-order logic does not admit any sound and complete
proof theory. In the above, the only complete rule of proof is that second-order universal
elimination completely formalizes the consequences of ∀ meant as ranging over definable structures.
No rule can exhaust the consequences of applying ∀ to the range of "all structures" (including
undefinable ones) for the following reason whose details will be developed later.
Arithmetic (the theory describing the system ℕ of natural numbers with four symbols 0, 1, +, ⋅ )
can be "completely" formalized in second-order logic (axioms listed in 4.3 and 4.4) in the sense of
excluding non-standard models, thus determining in principle the values of all its first-order statements
as true or false. The only component of this formalization beyond first-order logic is the axiom of induction,
using a ∀ ranging over "all unary predicates" (including undefinable ones). However the incompleteness theorem will refute
the possibility for any algorithm to give the correct values of all first-order statements of arithmetic.
But the range of the mere definable structures of a type cannot be completely described either for the same reason,
since describing the exact infinite range of all possible defining expressions, amounts to describing ℕ.
Defining new binders
Definitions of new binders B to be used in a first-order theory T (namely
in set theory which we shall formalize with its translation as a first-order theory) are expressible
in second-order logic, by an arbitrary defining expression here abbreviated as
F(A) as it involves (beyond the language of T)
a variable symbol A of unary structure (whose argument will be bound by B) :
similarly to how a functor symbol f defined by a term t with variable x is
declared by the axiom ∀x, f(x) = t(x),
this definition of B is stated as
∀A, (Bx, A(x)) = F(A)
(where = becomes ⇔ if values are Boolean)
By second-order universal elimination, this comes down to a schema of definitions in first-order logic :
for each expression defining A, it defines (Bx, A(x)) like a structure symbol,
by the expression F(A) whose available free variables are the parameters
of F plus those of A.
Axioms of equality
In first-order logic with given types and a given language, some statements involving
= are valid (always true) for the range of interpretations keeping = as the = predicate
of set theory, but no more for the larger range of interpretations letting
it become any other predicate. A possible list of axioms of equality, is a list of
some of such statements which suffice to imply all others in this context. One such list
consists in the following 2 axioms per type, where the latter is meant as an axiom schema
by second-order universal elimination of the variable unary predicate A:
Variables x and y can also serve among parameters in definitions of A.
This can be understood by re-ordering quantifiers as (∀x,
∀y, ∀A), or as deduced from cases only using other free variables a, b, by
adapting a logically valid statement from 1.10 as
- ∀x, x = x (reflexivity)
∀A,∀x,∀y, (x = y ∧ A(y)) ⇒ A(x).
(∀x, ∀y, R(a, b, x,y)) ⇒ R(a, b, a,b).
Diverse definitions of A give diverse statements (assuming reflexivity):
3. ∀x,∀y, x = y ⇒ y = x
4. ∀x, ∀y, ∀z, (x = y ∧ y = z) ⇒
x = z
5. ∀f, ∀x, ∀y, x = y ⇒ f(x) = f(y)
6. ∀A, ∀x, ∀y, x = y ⇒ (A(x) ⇔ A(y))
7. ∀x, ∀y, ∀z, (x = y ∧ z = y) ⇒
z = x
| A(u) used
y = u
u = z
f(u) = f(y)
z = u
5. is a schema of statements with f ranging among functors between any two types.
6. can also be deduced from symmetry.
We shall abbreviate (x = y
∧ y = z) as x = y = z.
Remark. (1.∧7.) ⇒ 3., then 3. ⇒ (4. ⇔ 7) so that (1.∧7.) ⇔ (1.∧3.∧4.).
Another possible list of axioms of equality consists in statements 1. to 5. where f and
A range over the mere symbols of the language, each taken once per argument :
the full scheme of 2. is implied by successive deductions for each occurrence of symbol
in A. This will be further justified in 2.11 (equivalence
Introducing a variable x defined by a term t by writing (x = t ⇒ ...),
in other words putting the axiom x = t, can be
seen as justified by the rules in this way :
t = t ∴
∃x, (x = t ∴ ...).
FR : 1.11. Quantificateurs
du second ordre