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.

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.

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