Now let us call

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
**Second-order Universal Introduction.** If *T'*⊢*F* then *T*
entails the second-order statement (∀*s*, *F*(*s*)).

**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.

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 (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 ℕ.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

- ∀
*x*,*x*=*x*(reflexivity) -
∀
*A*,∀*x*,∀*y*, (*x*=*y*∧*A*(*y*)) ⇒*A*(*x*).

∀*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 = uu = zf(u) = f(y)
¬ A(u)z = u |

5. is a schema of statements with

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*.

(∀*x*, *x* = *x*) ∴ *t* = *t* ∴
∃*x*, (*x* = *t* ∴ ...).

∀*x*, *f*(*x*) = *t*(*x*).

Finally, new binders

∀*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*.

Other languages:

FR : 1.11. Quantificateurs du second ordre