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:
  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 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):

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
Quality of =

Left Euclidean
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.

Remark. (1.∧7.) ⇒ 3., then 3. ⇒ (4. ⇔ 7) so that (1.∧7.) ⇔ (1.∧3.∧4.).
We shall abbreviate (x = yy = 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.

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
Truth undefinability
Introduction to incompleteness
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