1.11. Second-order universal quantifiers
First-order logic can be developed to allow the use of variable structure symbols as
abbreviations of fixed expressions defining these structures with variable parameters, but
this way can only bind them on some restricted ranges depending on the chosen expressions
(more comments in 1.D).
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 (by any expressions
with any number of parameters) or as the full set of all such operations
(relating the given interpreted types), which exist... in the universe.
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.
A theory is called complete if it essentially determines its model. The exact
definition is that all models are isomorphic
to each other (3.3); but let us understand now that it both determines all properties of its model
(values of first-order statements) and excludes non-standard models.
Arithmetic (the theory describing the system ℕ of natural numbers with four symbols 0, 1, +, ⋅ )
can be formalized as a complete theory in second-order logic (axioms listed in 4.3 and 4.4).
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 (1.C) 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 defined
either for the same reason, since defining the exact infinite range of all possible
defining expressions, amounts to defining ℕ.
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:
- ∀x, x = x (reflexivity)
-
∀A,∀x,y, (x = y ∧ A(y)) ⇒ A(x).
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 the use with an A with parameters a,
b, by adapting a logically valid statement from 1.10 :
∀a,b, (∀x,y, R(a, b,
x,y)) ⇒ R(a, b, a,b)
Diverse definitions of A give diverse statements (assuming reflexivity):
Statement
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 |
Quality of =
Symmetric
Transitive
Left Euclidean
|
A(u) used
y = u
u = z
f(u) = f(y)
¬A(u)
z = u |
5. is a schema of statements with f ranging among functors between any two types.
6. can also be deduced from symmetry.
Remark. (1.∧7.) ⇒ 3., then 3. ⇒ (4. ⇔ 7) so that (1.∧7.) ⇔ (1.∧3.∧4.).
We shall abbreviate (x = y ∧ y = z) as x = y = z.
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.9 (equivalence
relations).
Defining new binders
A new free variable symbol x defined by a given term t can be introduced, either
declared as a separate line of proof (x = t) serving as axiom, or inside a line as
(x = t ∴ ...). This can be justified by the rules as
(∀x, x = x) ∴ t = t ∴ ∃x,
(x = t ∴ ...).
Binding one parameter, the definition of a functor symbol f
by a term here abbreviated t with variable x (which will justify this abbreviated notation
t like a functor symbol), is declared by the axiom
∀x, f(x) = t(x).
Similarly, operator symbols can be defined by binding multiple parameters, and classes and other
predicates can be defined in the same way replacing = by ⇔.
Finally, new binders B to be used in a first-order theory T (namely
in set theory formalized with its translation as a first-order theory) can be defined
by any expression here abbreviated as F(A) as it involves, beyond the language of T,
a symbol A of variable unary structure (whose argument will be bound by B).
Such a definition can be declared by this second-order axiom :
∀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 defining expression for A, the expression (Bx, A(x)) is defined like
a structure symbol, by the expression defining F(A), obtained by replacing A by
its defining expression inside the expression F. So its available free variables are the
parameters of F plus those of A.
Other languages:
FR : 1.11. Quantificateurs
du second ordre