1.11. Secondorder universal quantifiers
Firstorder 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 secondorder 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 secondorder quantifiers means working in some wider logical framework such as
some version of secondorder 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 secondorder logic for intuitive reasons, before formally interpreting
this as a convenient meta level tool to abbreviate a firstorder formalization, as follows.
Let T be
a firstorder theory, T' its extension by a structure symbol s
(without further axiom) and F a statement of T' (in firstorder logic)
also denoted F(s) when seen as a formula of T using the
variable structure symbol s in secondorder logic.
Secondorder Universal Introduction. If T'⊢F then T
entails the secondorder 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.
Secondorder Universal Elimination. Once a secondorder statement
(∀s, F(s)) is accepted in a theory T,
it is manifested in firstorder 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 secondorder universal elimination after secondorder universal introduction,
means deducing from T a schema of theorems, each one deducible
in firstorder logic by replacing s by its respective definition in the original proof.
Incompleteness of secondorder logic
The above rules of proof, which will suffice for our needs, are clearly sound,
but unlike firstorder logic, secondorder logic does not admit any sound and complete
proof theory. In the above, the only complete rule of proof is that secondorder 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 secondorder logic (axioms listed in 4.3 and 4.4) in the sense of
excluding nonstandard models, thus determining in principle the values of all its firstorder statements
as true or false. The only component of this formalization beyond firstorder 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 firstorder 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 firstorder theory T (namely
in set theory which we shall formalize with its translation as a firstorder theory) are expressible
in secondorder 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 secondorder universal elimination, this comes down to a schema of definitions in firstorder 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 firstorder 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 secondorder 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 reordering 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 ∀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 
Name
Symmetry Transitivity

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.
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
relations).
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 ∴ ...).
Other languages:
FR : 1.11. Quantificateurs
du second ordre