1.11. Second-order universal quantifiers

First-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:
  1. x, x = x (reflexivity)
  2. A,∀x,∀y, (x = yA(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 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 = yy = x
4. ∀x, ∀y, ∀z, (x = yy = z) ⇒ x = z
5. ∀f, ∀x, ∀y, x = yf(x) = f(y)
6. ∀A, ∀x, ∀y, x = y ⇒ (A(x) ⇔ A(y))
7. ∀x, ∀y, ∀z, (x = yz = 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 = yy = 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 ∴ ...).

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions,..., meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Axioms and proofs
1.10. Quantifiers
1.11. Second-order quantifiers
Philosophical aspects
Time in model theory
Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations

Other languages:
FR : 1.11. Quantificateurs du second ordre