4. Arithmetic and firstorder foundations
4.1. Algebraic terms
Algebraic drafts
The concept of algebraic term with a purely algebraic language L
and a set V of variable symbols (no predicate, logical symbols nor
binders), which was first intuitively introduced in
1.5), is going to be formalized as systems
in a set theoretical framework. For convenience let us work with one type
(the generalization to many types is easy), and start with a wider class of
systems.
Let us call Ldraft
any L'system
(D,D) where D⊂ (^{L}D)×D, such that:
 The transpose ^{t}D of D is the
graph of a function Ψ_{D}: O_{D}
→ ^{L}D, with domain O_{D} = Im D = D\V
called the set of occurrences in D (which differs from our first intuitive
notion of occurrences), and its complement V_{D} = D∩V
is the set of used variables of D;
 〈V_{D}〉_{L}= D (wellfoundedness condition).
Let us denote ∀x∈O_{D},
Ψ_{D}(x) = (σ(x), l_{x})
∈ ^{L}D where σ∈L^{OD} and
l_{x}∈D^{nσ}^{(x)}.
Equivalent formulations of wellfoundedness are
∀A⊂O_{D}, (∀x∈O_{D},
Im l_{x} ⊂ A∪V ⇒ x∈A)
⇒ A=O_{D}
∀A⊂D, (V_{D}⊂A ∧
D_{*}(^{L}A) ⊂A) ⇒
A = D
∀A⊂D, V_{D}⊂A≠D
⇒ ∃x∈O_{D}\A, Im l_{x}⊂A
∀A⊂O_{D}, A≠∅ ⇒ ∃x∈A,
A∩ Im l_{x} = ∅
A ground draft is a draft with no variable, i.e. V_{D}=∅. Thus,
Ψ_{D}: D→ ^{L}D and Sub_{L}D
= {D}.
Variables in a draft may be reinterpreted as constants: extending Ψ_{D}
by Id_{VD} : V_{D} → V,
forms a ground (L∪V)draft.
Subdrafts and terms
Drafts do not have interesting stable subsets (by wellfoundedness), but
another stability concept: a subset A⊂D is a subdraft of
D (or a costable
subset of D) if, denoting O_{A} = A∩O_{D}
and Ψ_{A} = Ψ_{DOA},
we have (Im Ψ_{A}⊂ ^{L}A), i.e. ∀x∈O_{A},
Im l_{x}⊂A.
Indeed, it remains wellfounded, as can be seen on the last formulation of wellfoundedness.
Like with stable subsets, any intersection of subdrafts is a subdraft. Moreover,
any union of subdrafts is also a subdraft (unlike for subalgebras with an operation
with arity >1, which from arguments in different subalgebras may give a result escaping
their union).
The subdraft cogenerated by a subset of a draft, is the intersection of all subdrafts
that include it. A term is a draft cogenerated by a single element that is its root.
Each x in a draft D defines a term T_{x} with
root x, subdraft of D cogenerated by {x}.
Each draft D is ordered by x ≤ y ⇔ x∈T_{y}.
It is obviously a preorder.
Proof of antisymmetry (uniqueness of the root):
∀x∈O_{D}, V_{D} ⊂
A={y∈Dx∉T_{y}} which is a subdraft
by transitivity of ≤.
x∉A ∴ ∃z∈O_{D}\A,
Im l_{z}⊂A.
A∪{z} is a subdraft, thus T_{z}⊂A∪{z}
by definition of T_{z}.
z∈O_{D}\A ∴
x∈T_{z} ∴ x=z.
Thus x is determined by A. ∎
More properties of this order will be seen for natural numbers in 3.6, and in the
general case with wellfounded relations
in the study of Galois connections.
Categories of drafts
As particular relational systems, classes of Ldrafts form concrete categories.
Between two Ldrafts D,E,
f ∈Mor_{L}(D,E) ⇔
(f[O_{D}]⊂O_{E} ∧
Ψ_{E} ০ f_{OD}=
^{L}f০Ψ_{D})
where the equality condition can be split as
σ_{E}০f_{OD}
= σ_{D}
∀x∈O_{D},
l_{f(x)}=f০l_{x}
Another concrete category is that of drafts with variablespreserving morphisms, where V
is fixed and morphisms f from a draft D are subject to
f_{VD} = Id_{VD}.
This is equivalently expressed reinterpreting variables as constants, as the category of ground
(L∪V)drafts.
Intepretations of drafts in algebras
For any Ldraft D and any Lalgebra E, an interpretation of
D in E is a morphism f∈Mor_{L}(D,E),
i.e. f_{OD}=
φ_{E}০^{L}f০Ψ_{D},
also expressible as
∀x∈O_{D}, f(x) =
σ(x)_{E}(f০l_{x})
Any interpretation v∈E^{V} of variables in an algebra E
determines an interpretation of any draft D in E. To simplify formulations,
restricting v to V_{D} reduces the problem to the case
V_{D}=V.
Theorem. For any Ldraft D with V_{D}=V and
any Lalgebra E, any v∈E^{V}
is uniquely extensible to an interpretation of D:
∃!h∈Mor_{L}(D,E), h_{V}
= v, equivalently ∃!h∈E^{OD}, v∪h
∈ Mor_{L}(D,E).
Uniqueness is deduced from
wellfoundedness : ∀g,h∈Mor_{L}(D,E),
g_{V} = v = h_{V} ⇒
V⊂ {x∈Dg(x) = h(x)} ∈
Sub_{L}D ⇒ g=h.
Let us now prove existence (using conditional operator).
S = {A⊂D  V⊂A ∧ Im Ψ_{A}⊂
^{L}A}
v ∈ K = ⋃_{A∈}_{S}
{f∈Mor_{L}(A,E) 
f_{V} =v}
∀f,g ∈K, B = Dom f ∩ Dom g
⇒ (f_{B}∈K ∧
g_{B}∈K)
⇒ f_{B}=g_{B}
⋃_{f∈K} Gr f = Gr h
C= Dom h = ⋃_{f∈K} Dom f
∈ S
h ∈ K
(C∪D_{*}(^{L}C) ∋ x↦ (x∈C ?
h(x) :
φ_{E}(^{L}h(Ψ_{D}(x)))))
∈ K
D_{*}(^{L}C) ⊂ C
C=D ∎
Operations defined by terms
Any element t of an Ldraft D defines a Vary
operation symbol, interpreted in each Lalgebra E by
∀v∈E^{V}, t_{E}(v) = h(t)
for the unique h∈Mor_{L}(D,E)
such that h_{VD} =
v_{VD}.
This formalizes the operation
defined by a term, namely the Lterm with root t in D (which
can replace D here without modifying the interpretations of t).
This interpreted operation symbol being the structure defined by
(Id_{V},t), is preserved by all Lmorphisms, thus
can be added to L without changing the category of Lalgebras.
Symbols s∈L come back as the particular cases of the terms they form
themselves where Ψ(t) = (s, Id_{V}).
For the case of "small" (concretely written) terms, this preservation also has a
schema of one proof for each term: reexpressing
the term as a formula defining a relation (graph of the operation) using symbols ∃ and ∧,
we can use the preservation
of structures defined by such formulas.4.2. Term algebras
Condensed drafts
A draft D is condensed if, equivalently, D is functional,
i.e. Ψ_{D} is injective;
 D has an injective interpretation in some algebra;
 For any two distinct elements of D there is an algebra interpreting
them differently.
1.⇒2. if D≠∅ (otherwise replace D by a singleton),
∃φ∈D^{LD},
φ০Ψ_{D} = Id_{OD}, i.e.
Id_{D} interprets D in (D,φ).
2.⇒3.
3.⇒1. ∀x,y∈O_{D}, if Ψ_{D}(x) =
Ψ_{D}(y) then x,y have the same interpretation
in every algebra.
Any draft D can be reduced to a condensed draft as follows.
Give
℘(D) the Lalgebra structure (s,u) ↦
{x∈O_{D}  σ(x)=s ∧ l_{x}∈∏u}.
Then the interpretation of D in ℘(D) which sends any variable x to {x},
is the curried form of the only equivalence relation on D which quotients it
into a condensed draft.
Let us call condensation of D this projection of D
to a condensed draft. This is the (not typographically convenient) way to confuse
the repeated subterms of a given term (or draft), which will have the same meaning
in all algebras.
This equivalence relation is included in that of any interpretation
of D in any algebra, thus quotienting interpretations of D.
We can also compare separately given terms by reducing them
to this case as any disjoint union
of drafts (only keeping variables in common) is a draft.
If L only has symbols with arity 0 or 1 then every Lterm is condensed.
Term algebras
An Lalgebra (E,φ_{E}) is called a term algebra
if it is injective and 〈E\Im φ_{E}〉_{L}
= E. Thus it is also a condensed Ldraft with Ψ_{E}
= φ_{E}^{1}. Another usual assumption is that
V=V_{D}=E\Im φ_{E}, i.e.
used variables of a term algebra are usually not regarded as a
subset of any larger set of available variables. This term algebra is ground if
V=∅, i.e. E=Im φ_{E}. So, a ground term
Lalgebra is an algebra both minimal and injective, and thus also bijective.
If L has no constant then ∅ is a ground term Lalgebra.
If L only has constants, then ground term Lalgebras are the
copies of L.
From any injective Lalgebra (E,φ_{E}) and
V ⊂ E \ Im φ_{E} one can form the term algebra
〈V〉_{L}. In particular the existence of an injective
algebra implies that of a ground term algebra.
Whenever present as object, any ground term Lalgebra is an
initial object in
any category of Lalgebras, and a final object in any category of ground
Ldrafts. It is thus essentially unique for the given L.
Conversely any initial Lalgebra (E,φ_{E})
is a ground term algebra:
 minimal : ∃f∈Mor_{L}(E,Min_{L}E),
f∈Mor_{L}(E,E)∴ f=Id_{E} ∴
Min_{L}E=E
 injective : (F = ^{L}E ∧ φ_{F} =
^{L}φ_{E}) ⇒
φ_{E}∈Mor_{L}(F,E) ∴
∃f∈Mor_{L}(E,F),
φ_{E}০f = Id_{E}
∴ f০φ_{E} =
φ_{F}০^{L}f =
^{L}(φ_{E}০f) = Id_{F}.
Similarly, term Lalgebras (E,φ_{E}) with
E\Im φ_{E}=V are the final objects in any
variablespreserving category of Ldrafts for a given V (this is
deducible from the above by replacing variables by constants).
Proposition. For any ground term Lalgebra K
and any injective Lalgebra M, the unique
f∈Mor_{L}(K,M) is injective.
Proof 1. By the injectivity lemma,
{x∈K  ∀y∈K,
f(x) = f(y) ⇒ x=y}
∈ Sub_{L}K, thus = K.
Proof 2. Im f ∈ Sub_{L}M is both injective and
minimal,
thus a ground term Lalgebra, so the morphism f between initial Lalgebras
K and Im f is an isomorphism.
Role of term algebras as sets of all terms
As any draft can be seen as a family of terms, any term algebra (final draft)
F precisely plays the more role of the "set of all terms" (with the given list
V of variable symbols), as it contains exactly one representative image
of each term (operation symbol defined by a term), i.e. any two "equivalent terms"
(defining the same operation) have the same image. Namely, any
Lterm T with root t and V_{T}⊂V, is
represented in F by the image of the f∈Mor(T,F) such that
f_{VT} = Id_{VT},
with root f(t).
This f plays the role of condensation (so is injective if and only if
T is condensed), respecting the interpretation in any Lalgebra
E extending any v∈E^{V}, as the unique
g∈Mor_{L}(F,E) and
h∈Mor_{L}(T,E) extending v, are related by
h=g০f, thus
h(t)=g(f(t)).
For any subset A of an Lalgebra E and any term algebra
whose set of variables is a copy of A, the image of its interpretation
in E is 〈A〉_{L}.
Free monoids
If it exists, any unary term Lalgebra M (essentially determined by L),
is a monoid acting on all Lalgebras, whose actions are preserved by all
Lmorphisms (Mor_{L} ⊂ Mor_{M} as they form a category of acts). It serves as
set of all (function symbols defined by) unary Lterms. The set of function
symbols from L is canonically injected there by j(s) =
s_{M}(e) so that in any Lalgebra E, ∀x∈E,
j(s)⋅x = s_{E}(x).
Conversely if L is made of function symbols then essentially
L ⊂ M, thus Mor_{L} = Mor_{M}.
The monoid structure of M was defined from its Lstructure; now let us
take the monoid structure as primitive and review alternative descriptions from it, of the
situation when L was made of function symbols. These function symbols
can be replaced by (reinterpreted as) constant symbols, as these 2 interpretations
can be defined from each other by terms using the monoid structure: the function defines
the constant as s = s(e), while the constant defines the function as
∀x∈M, s(x) = s•x.
For any set X, let us call Xmonoid any (X∪{e,•})algebra M
seeing X as a set of constant symbols by some j:X→M, such that
(e,•) is a monoid structure on M.
Denoting X_{1} the copy of X seen a set of function
symbols, the following statements on M are equivalent; such an M is
called a free monoid on X.
 M is a unary term X_{1}algebra with variable e,
interpreting the copy x'∈X_{1} of each x∈X
as ∀y∈M, x'_{M}(y) = j(x)•y
 For any X_{1}algebra E there is a unique left action
⋅ of M on E such that ∀x∈X, ∀y∈E,
j(x)⋅y = x_{E}(y)
 M is an initial object in the category of Xmonoids.
(The proof of this equivalence remains to be completed, using the property of trajectories
and the representation theorem)
1. is equivalent to: for any X_{1}algebra E and any x ∈ E
there is a unique h_{x} ∈
Mor_{X1}(M,E) such that
h_{x}(e)=x.
That is the curried form of the action ⋅ : M×E → E.
The uniqueness of the morphism to other Xmonoids is expressed by
〈X〉_{{e,•}} = M.
When writing terms with multiple uses of an associative operation symbol, all parenthesis
may be removed. For monoids, this removal of parenthesis and also of occurrences of e
seen as the empty chain of symbols, is operated by the interpretation of any
Vary {e,•}term in the free monoid on V.
The image of M by any morphism of monoid is the submonoid generated by the image of L.
Examples of varieties
The above gives two examples of varieties
 That of all Lalgebras for any given algebraic language L; its clone is the sequence of term algebras
with each finite arity.
 That of all monoids; its clone is made of free monoids.
4.3. Integers and recursion
The set ℕ
An arithmetic is any theory describing the system ℕ of natural numbers.
There are diverse such theories, depending on the choice of a logical framework,
then of a language and axioms. First is the set theoretical one,
which is the most precise as it determines the isomorphism class of ℕ in
the given universe :
Definition. ℕ is a ground
term algebra with two symbols: a constant
symbol 0 called zero, and a unary symbol S called the successor.
The essential uniqueness of such systems removes any uncertainty attached
to fixing a choice of ℕ among them, at least once any irrelevant questions are made
inexpressible by seeing ℕ as a set of pure elements.
The existence of a ground term {0,S}algebra is our first expression of the
axiom of infinity, which
completes the set theory we progressively introduced from the beginning to the powerset (with optionally the
axiom of choice), to form what is
essentially the standard foundation of mathematics as practiced by most mathematicians.
It will imply the existence
of term algebras with any language.
The above use of algebraic concepts in the definition of ℕ may make it look circular, as
our study of algebras used natural
numbers as arities of operation symbols. But these definitions may also be written
without reference to numbers when used symbols have small arities only
(for arithmetic, arities are first just 0 and 1, then later 2).
Namely, the most convenient expression of the axiom of infinity consists in inserting arithmetic into
set theory, by first inserting the language of {0,S}algebra in the form of 3
constant symbols: ℕ (as a set) and the images of both algebraic symbols 0 and S,
with axioms 0∈ℕ and S:ℕ→ℕ; then making this a ground term algebra by the
following 3 axioms :
(H0) 
∀n∈ℕ, Sn ≠ 0

: 0 ∉ Im S 
(Inj) 
∀n,p∈ℕ, Sn =
Sp ⇒ n = p 
: S is injective 
(Ind) 
∀A⊂ℕ, (0∈A ∧ ∀n∈A,Sn∈A)
⇒ A=ℕ 
(induction) : ℕ is minimal. 
More constant symbols can be defined from there:
1=S0, 2=S1=SS0, 3=S2=SSS0, ...
Recursively defined sequences
A sequence of elements of a set E, is a function from ℕ to E
(a family of elements of E indexed by ℕ).
In particular, a recursive sequence in E is a sequence defined as the
only u∈E^{ℕ} such that u ∈ Mor(ℕ,(E,a,f)),
where (E,a,f) is the {0,S}algebra E
interpreting 0 as a∈E and S as f∈E^{E} :
u_{0}=a
∀n∈ℕ, u_{Sn} = f(u_{n}).
As u_{n} also depends on a and f, let us write it as
f^{ n}(a). This notation is motivated as follows.
As an element of a ground term {0,S}algebra, each number n represents a
term with symbols 0 and S respectively interpreted as a and f in E.
So, f^{ n}(a) abbreviates
the term with shape n using symbols a and f:
f^{ 0}(a) = a
f^{ 1}(a) = f(a)
f^{ 2}(a) = f(f(a)) 
Reinterpreting the constant 0 as a variable, makes ℕ a unary term
{S}algebra, where each number n is a unary term S^{n} with n
occurrences of S, interpreted in each {S}algebra (E,f)
as the function f^{ n}∈ E^{E}, recursively defined by
f^{ 0} = Id_{E}
∀n∈ℕ, f^{ Sn} = f০f^{ n}
In particular, f^{ 1}=f and f^{ 2} = f০f.
Generally for any f∈E^{E},
g∈E^{X}, the sequence (h_{n})_{n∈ℕ} in
E^{X} recursively defined by (h_{0}=g) and
(∀n∈ℕ, h_{Sn} = f০h_{n})
is h_{n}=f^{ n}০g.
Addition
Like any unary term algebra, ℕ forms a monoid (ℕ, 0, +),
whose actions are the sequences (f^{ n}) for any transformation f.
It is commutative as it is generated by a singleton, {1} (which commutes with itself). Thus the side won't
matter, but conventions basically present it as acting on the right, defining addition as
n+p = S^{p}(n), or recursively as
n + 0 = n
∀p∈ℕ, n+S(p) = S(n+p).
Thus, n+1 = S(n+0) = Sn.
Like in the general case, the action formula ∀n,p∈ℕ, f^{ n+p} = f^{
p}০f^{ n} is deduced from
(f^{n+0}=f^{n} ∧ ∀p∈ℕ,
f^{n+Sp} = f^{S(n+p)
} = f০f^{n+p})
∴
∀a∈E, ∀f∈ E^{E}, (p↦f^{
n+p}(a))∈Mor(ℕ,(E,f^{n}(a),f)),
In this view, associativity appears as (a+b)+n =
S^{n}(S^{b}(a)) =
S^{b}^{+}^{n}(a) =
a+(b+n). From now on, use of associativity will be implicit, omitting parenthesis.
Multiplication
By the concept of cardinals of finite
sets (counting their elements)
that will be defined in 4.1., multiplication in ℕ
may be defined as the cardinal of a product, making obvious its
basic properties, including commutativity.
Without this, multiplication can be defined by the following recursion,
which needs to treat sides differently until commutativity is deduced.
Let us choose the side that fits common language, though it is opposite
(transpose) to the usual one from the literature on the axioms of arithmetic:
∀x∈ℕ, 0⋅x = 0
∀x,y∈ℕ, (Sx)⋅y = (x⋅y)+y
which can be summed up as x⋅y =
(S^{y})^{x}(0). Then generally, ∀f∈E^{E}, f^{ x⋅y}
= (f^{ y})^{x}.
∀x∈ℕ, x⋅0 = 0 is deduced by induction.
Right distributivity ∀x,y,z∈ℕ, (x+y)⋅z =
x⋅z + y⋅z comes by induction on y, or as
(S^{z})^{x+y} =
(S^{z})^{y}০(S^{z})^{x}.
Left distributivity ∀x,y,z∈ℕ, x⋅(y+z) =
x⋅y + x⋅z comes by induction on x using commutativity of +. In particular this gives ∀x,y∈ℕ, x⋅Sy = (x⋅y)+x, so that the transpose of multiplication, satisfying the same recursive definition, coincides with it : multiplication is commutative.
Inversed recursion and relative integers
By induction using commutativity (n+1 = 1+n), ∀f,g∈
E^{E}, g০f = Id_{E}
⇒ ∀n∈ℕ, g^{n}০f^{ n} = Id_{E}.
Thus if f is a permutation then f^{ n} is also a permutation, with inverse
(f^{ n})^{1} = (f^{ 1})^{n}.
Commutativity was just here to show that composing n times is insensitive to sides reversal,
as (f^{ n})^{1} has the more direct recursive definition
(f^{ Sn})^{1} =
(f^{n})^{1}০f.
The system of (relative) integers ℤ is defined as the {0,S}algebra where
 the set ℤ is defined as ℕ ∪ ℕ, where elements of ℕ (natural numbers) are
called positive, and ℕ= {nn∈ℕ} is a copy of ℕ
called the set of negative integers (where n is the opposite of n),
only intersecting ℕ at 0 = 0.
 S_{ℤ} is the permutation extending S_{ℕ} by
∀n∈ℕ, S(Sn)= n, thus letting Gr S_{ℤ} be
the union of Gr S_{ℕ} with its transposed copy in ℕ.
Proposition. ℤ is a commutative group, and for any permutation f of a set E,
there exists a unique (f^{ n})_{n∈ℤ} which is,
equivalently, a {0,S}morphism from ℤ to (E^{E}, Id_{E},
f), or an action of ℤ on E interpreting 1 as f.
Proof: the {0,S}morphism condition requires on ℕ the same n ↦
f^{ n} as above; on ℕ, it recursively defines f^{ n} =
(f^{ 1})^{n}, namely
 f^{ 0} = Id_{E} = f^{ 0}
 ∀n∈ℕ, f^{ n} = f০f^{ Sn},
equivalently f^{ 1}০f^{ n} = f^{ Sn}
This makes (ℤ,0,S) an initial object in the category of {0,S}algebras
(E,a,f) where f is a permutation. This category is derived as described for eggs from that of
{S}algebras (E,f) where f is a permutation.
Therefore, ℤ is a monoid acting by (f^{ n})_{n∈ℤ} on every set E
with a permutation f.
This monoid is a commutative group because it is generated by {1, 1}, which commute and are the
inverse of each other : (1)+1=0=1+(1).
The formula of its inverse, (n)+n = 0 = n+(n) can be deduced either
from symmetry ((n)+n∈ℕ ⇔ n+(n)∈ℕ) and commutativity, or from the
above result.
4.4. Presburger Arithmetic
Firstorder theories of arithmetic
Our first formalization of ℕ
was based on the framework of set theory, using the powerset to determine the isomorphism class of ℕ.
This allowed recursion, from which addition and multiplication could be defined.
Let us now review firstorder theories describing ℕ as their only type, called theories
of firstorder arithmetic. As firstorder logic cannot fully express the powerset,
the (∀A⊂ℕ) in the induction axiom must be replaced by a weaker version :
it can only be expressed with A ranging over all classes of the theory, that is, the
only subsets of ℕ defined by firstorder formulas in the given language, with bound
variables and parameters in ℕ. For this, it must take the form of a schema of axioms,
one for each formula that can define a class.
But as the set theoretical
framework was involved to justify recursive definitions, the successor function no
more suffices to define addition and multiplication in firstorder logic.
This leaves us with several nonequivalent versions of firstorder arithmetic depending
on the choice of the primitive language, thus nonequivalent versions of the axiom
schema of induction whose range of expressible classes depends on this language:

Bare arithmetic, with the mere symbols 0 and S, is very poor.
 Presburger arithmetic is arithmetic with addition. It still
cannot define multiplication.
 Full arithmetic, named Z_{1},
admits symbols 0,S, + and ⋅ , and
all axioms of their definitions. It
can express any other recursion.
Presburger arithmetic
A minimal formalization describes the set ℕ* of nonzero natural
numbers, with symbols 1 (constant) and + (binary operation), and axioms :
∀x,y∈ℕ*, x + (y+1)
= (x+y)+1 
(A1) : + is associative on 1 
∀A⊂ℕ*,(1∈A ∧ ∀x,y∈A,
x+y∈A) ⇒A=ℕ* 
(Min) 
∀x,y∈ℕ*, x + y
≠ y 
(F) 
In set theory, (Min) would make ℕ* a minimal {1,+}algebra. But we shall use set
theoretical notations in such ways that they can be read as abbreviations of works in
firstorder logic: as long as we only consider subsets of ℕ* defined by firstorder formulas
in this arithmetical language, (Ind)
and (Min) can be read as abbreviations of schemas of statements, A ranging
over all classes in this theory.
(A1) is a particular case of
∀x,y,z∈ℕ*, x + (y+z)
= (x+y)+z 
(As) : + is associative 
Conversely, (A1 ∧ Min) ⇒ (As) :
Let A={a∈ℕ* ∀x,y ∈ℕ*,
x+(y+a) = (x+y)+a}. ∀a,b∈A,
∀x,y ∈ℕ*, x + (y+(a+b))
= x + ((y+a)+b) = (x + (y+a))+b
= ((x + y)+a)+b = (x+y)+(a+b)
∴ a+b ∈ A.
(A1) ⇔ 1∈A.
(A1 ∧ Min) ⇒ A=ℕ* ∎
(As ∧ Min) ⇒ (+ is commutative), as deduced from 1∈C({1}).
Now take ℕ = ℕ*∪{0} where 0∉ℕ*, to which + is extended as ∀n∈ℕ,
0+n = n+0 = n. This extension preserves its properties
of commutativity and associativity.
Define S as ℕ∋x↦ x+1.
These definitions directly imply (H0).
Let (Ind_{1}) be the statement ∀A⊂ℕ*,
(1∈A ∧ (∀x∈A, x+1 ∈A)) ⇒ A=ℕ*.
(Ind_{1}) ⇒ (Ind) ; (Ind) ⇒ (Ind_{1}) using A∪{0}.
One may instead use {x∈ℕx+1∈A} once noted that (Ind) ⇒ Im S = ℕ*.
(Ind_{1}) ⇒ (Min)
(As ∧ Min) ⇒ (Ind) in set theory (ignoring our previous definition of ℕ):
Let M = Min_{{0,S}}ℕ.
∀x∈M, M ∈ Sub(ℕ,x,S) ∧ f_{x} =
(M∋y↦x+y) ∈ Mor_{{S}}(M,ℕ).
Im f_{x} = f_{x} [〈0〉_{{S}}] =
〈x〉_{{S}} ⊂ M.
As M is stable by + and contains 1, it equals ℕ.∎
(As ∧ Min) ⇒ (Ind) as directly convertible to firstorder logic:
Let A∈Sub_{{0,S}}ℕ, and B
= {y∈ℕ* ∀x∈A, x+y∈A}.
∀y,z∈B, (∀x∈A, x+y∈A ∴
x+y+z∈A) ∴ y+z ∈B.
(∀x∈A, x+1 ∈A) ⇔ 1∈B ⇒ ((Min)⇒
B=ℕ*).
0∈A ⇒ (∀y∈B, 0+y∈A) ⇒ B⊂A.∎
So, all possible axiom pairs are equivalent:
(A1 ∧ Min) ⇔ (As ∧ Min) ⇔ (As ∧ Ind) ⇔ (A1 ∧ Ind), and imply commutativity.
Parity
A number n∈ℕ is even if ∃x∈ℕ, n=x+x; it is odd
if ∃x∈ℕ, n=x+x+1.
Obviously, if n is even then n+1 is odd; if n is odd then n+1 is even thanks to commutativity. Thus by induction, any number is either even or odd.
But to show that it cannot be both and that this x is unique, also requires the use of
(Inj). These are left as a possible exercise. But instead of (Inj) we proposed axiom (F).
This raises the question of their equivalence.
(F) ⇔ (∀x∈ℕ*, ∀y∈ℕ, x+y ≠ y)
because x+0 = x ≠ 0.
(Inj ∧ Ind ∧ A1) ⇒ (F) because ∀x∈ℕ*,
{y∈ℕ  x+y ≠ y} ∈ Sub_{{0,S}}ℕ .
For the converse, we need to use the order relation.
The order relation
In any model of Presburger arithmetic,
let us define binary relations ≤ and < as x<y ⇔ ∃z∈ℕ*, y =
x+z
x≤y ⇔ ∃z∈ℕ, y = x+z
(A1 ∧ Ind) implies that
 < is transitive
 x≤y ⇔ (x<y ∨ x=y)
 x<y ⇔ x+1≤y
 ∀A⊂ℕ, A≠∅ ⇒ ∃x∈A, ∀y∈A,
x≤y (meaning a schema of formulas in Presburger arithmetic)
 ∀x,y∈ℕ, x≤y ∨ y≤x
 x<y ⇒ x+z < y+z
Proofs :
 using (As), x < y < z
⇒ (∃n,p∈ℕ*, z = y+p = x+n+p)
⇒ x < z.
 obvious from definitions;
 thanks to (Ind), ℕ is a bijective
{0,S}algebra;
 x≤y ⇒ (x+1≤y ∨ x=y)
0∈{x∈ℕ ∀y∈A, x≤y}=B
∀x∈B, x+1∈B ∨ x∈A
A⋂B=∅ ⇒ (B=ℕ ∴ A=∅)
 from 4. with A={x,y}. Or using 3, A={x∈ℕ
∀y∈ℕ, x<y ∨ x=y ∨ y<x}
⇒ (0∈A ∧ ∀x∈A, x+1∈A)
 y = x+n ⇒ y+z = x+z+n
∎
Now the full system (A1 ∧ Ind ∧ F) implies that  < is a strict total order, associated
with the total order ≤
 ∀x,y,z∈ℕ, x<y ⇔ x+z
< y+z
 + is cancellative (which gives (Inj) as a particular case).
Proof. (F) means that < is irreflexive, which with transitivity (1.) implies
that it is a strict order, which is total by 5.
There must be one true formula among (x<y),
(x
= y), (y<x), which by 6. respectively imply
(x+z<y+z),
(x+z = y+z), (y+z<x+z).
But only one of the latter can be true, thus each implication must be an equivalence.
Cancellativity on one side extends to the other side by commutativity.
∎
Finally, by 4., every nonempty subset A of ℕ has a smallest element
(unique by antisymmetry), written min A.
This order coincides with the order
between terms in the common particular case of the set theoretical ℕ, as will
be clear from the properties of generated preorders.
Arithmetic with order
It is possible to express a firstorder arithmetic with language {0,S, ≤}, more
expressive than {0,S} but less than Presburger arithmetic, in the sense that
addition cannot be defined from ≤.
There, ≤ is related to S by the following property (which determines it in set theory,
but no more in bare arithmetic due to the poverty of its
interpretation of induction by an axiom schema):
For all n ∈ℕ, the set {x∈ℕ  n ≤ x} is the unique A⊂ℕ
such that
∀x∈ℕ, x∈A ⇔ (x = n
∨ ∃y∈A, Sy=x).
Its existence in ℘(ℕ) can be deduced in set theory (not firstorder arithmetic) by induction
on n; its uniqueness for a fixed n is deduced by induction on x.
Trajectories of recursive sequences
For any recursive sequence u∈Mor(ℕ,(E,a,f)), the trajectory
K = Im u = {f^{ n}(a)  n∈ℕ} of an
action of ℕ on E is generated by a, which is a free element for the image of
ℕ as a transformation monoid of K thanks to the commutativity of +.
Therefore K can be seen as a commutative monoid, whose description
coincides with the above arithmetic without axiom (F), where the roles of the neutral element 0
and the generator 1 are respectively played by a and f(a). However for convenience, let us focus on the set theoretical viewpoint on the remaining case, when
u is not injective so that K is not a copy of ℕ. Then K must be a
noninjective {0,S}algebra: there must be a pair in {0,S}⋆K
mapped to a singleton, but we shall see that such a pair is unique.
Let y the minimal number such that ∃x<y, u_{x} =
u_{y}. This x is unique because y is minimal.
{u_{n}  n<y} ∈ Sub_{{0,S}}K,
thus =K.
As Inj f_{K} ⇔ x=0 ⇔ a∈ Im
f_{K} ⇔ f^{y}(a)=a
⇔ (f_{K})^{y} = Id_{K},
a trajectory K where these are true is called a cycle of f with period
y; the restriction of f to K is then a permutation of K. Then replacing
a by another element of K would leave both K and
y unaffected.
Now if f is a permutation then every cycle of f is also a cycle of f^{ 1}
with the same period.
4.5. Finiteness and countability
To review equivalent forms of the axiom
of infinity, we need to work without assuming it.
Let us start with a technical result.
Covering of stable subsets by terms
For any L'system (E,E), any X⊂E and any
x∈〈X〉_{L} in E there exists a draft
(D,D) where x∈D⊂E, D⊂E and
V_{D}⊂X.
It makes no difference to fix V_{D}=X, or X=∅
by adding it as a set of constants to the language.
Proof, fixing X=∅ to simplify.
Let us show the stability of the union B
of the D such that there exists a ground draft (D,D) with
D⊂E.
Let (s,x,y)∈E such that Im x ⊂B. By finite choice
there exists a tuple of ground drafts
(D_{i},D_{i})_{i<ns}
such that ∀i<n_{s},
x_{i}∈D_{i} ∧ D_{i}⊂E.
Let D = ⋃_{i<ns} D_{i}.
Let us check that Ψ = (D ∋ z ↦ Ψ_{i}(z) for the smallest
i such that z∈D_{i}), defines a ground draft.
For any nonempty A⊂D, take the smallest i
such that A∩D_{i} ≠ ∅.
∃z∈A∩D_{i},
∅ = A∩D_{i}∩ Im l_{i,z} =
A ∩ Im l_{i,z} because
Im l_{i,z} ⊂ D_{i}.
Ψ(z) = Ψ_{i}(z) because i
is also smallest such that z∈D_{i},
thus l_{z} = l_{i,z}.
We conclude ∃z∈A, A ∩ Im l_{z} = ∅,
thus Ψ defines a ground draft on D.
Then either y∈D, or adding it there with
(s,x,y) gives a ground draft that fits.∎
Thus independently of the axiom of infinity (existence of term algebras)
anyway all elements of a minimal algebra are values of ground terms.
Finiteness
Let K={0,S}.
For any set E, let us give its powerset P=℘(E)
the K'structure defined by 0_{P} = {∅} and
S_{P} = {(A,B)∈P^{2}
∃x∈B, A=B\{x}}.
We define the set of finite subsets of E as Min_{K}℘(E).
A set is finite if it is a finite subset of itself (otherwise it is infinite).
For any sets E⊂F, (E is finite) ⇔ (E is a finite subset of F). Proof :
 ⇒ : Id_{℘(E)} = Mor_{K'}(℘(E), ℘(F)).
 ⇐ : ∀A∈Sub_{K}℘(E),
A∪(℘(F)\℘(E)) ∈ Sub_{K}℘(F).
Equivalently, a set E is finite if it has a bijection to the graph of S in
a ground Kterm n (which can be seen as a unary {S}term). This may
as well be seen as a bijection to its domain {0,...,n1} or to its image {1,...,n}.
Proof. From a finite set E, the above theorem gives a term with root E included in ℘(E)...
Countable sets
It is easy to check that any condensed ground
Kdraft is either ∅ or a ground Kterm or a ground term
Kalgebra (only two other languages have this property, apart from those with no constant).
A set is called countable if, equivalently,
 It has an injection to a condensed ground Kdraft
 It has a bijection with a condensed ground Kdraft
 A condensed ground Kdraft has a surjection to it
1.⇒2. by restricting the order, once condensed ground {0,S}drafts are described
from their order structure; another method is given below.
2.⇒(1.∧ 3.) ; 3.⇒1. without AC, by picking the smallest element of each preimage.
So, countable sets are either finite or in bijection with ℕ. The latter, on which there exists a
possible structure of ground term {0,S}algebra, will be called countably infinite.
However we still need to prove that they are indeed infinite.
Finite cardinalities
Let ≈ be the equivalence relation of equinumerosity on P, defined as
existence of a bijection: A≈B ⇔ ∃f : A ↔ B.
The quotient
structure on Q=P/≈, seen as a graph
G⊂(^{{0,S}}Q)×Q is functional both ways (both it and
its transpose are functional), and Im G = Q.
Indeed:
 ∀(A,B),(A',B') ∈S_{P},
A≈A' ⇔ B≈B'. The converse for x∈B\A,
x'∈B'\A' and f : B ↔ B' is by A ∋
y ↦ (f(y)=x' ? f(x):f(y)) ∈A'.
 ∀A∈P, A≈∅ ⇔ A=∅ ⇔ A ∉ Im S_{P}.
Axiom of infinity
In set theory with the powerset, the
following statements are equivalent expressions of the axiom of infinity:
 There exists an injective algebra whose language has at least a constant and a
nonconstant.
 There exists a nonsurjective injection of a set to itself; equivalently an
injective {0,S}algebra, or a set ℕ.
 There exists an infinite set.
 For any countable algebraic language there is a (countable)
injective algebra
 Any consistent firstorder theory with a countable language
has a (countable) model
4. ⇒ 2. ⇒ 1.; for 1. ⇒ 2. : from a nonconstant operation s there,
x↦s(k↦x)
is an injective, nonsurjective transformation.
We shall prove 2. ⇔ 3. below (finite cardinalities), and 2. ⇒ 4. ⇒ 5. in the section on the
completeness theorem.
We may regard 5. ⇒ 4. as relative to the natural assumption that the concept of injective
algebra forms a consistent theory. This theory is essentially the part of set theory which describes
tuples. So, if a language L is
included in a model of that simple part of set theory, then there
exists an injective Lalgebra. If such a model U is standard, this takes the form
^{L}U ⊂ U, making (U, Id_{LU})
an injective Lalgebra. ∎
The infinity of ℕ easily implies the uniqueness of the
number of elements of a finite set, as its nonuniqueness would give that set a strict injection
into itself, and thus an injection of ℕ into it.
2. ⇒ 3. will come from the infinity of ℕ.
For 3. ⇒ 2. we shall pick a different set, as the existence of an injective
{0,S}algebra structure on any infinite set would need the axiom of choice.
Finite cardinalities
Now denoting e the image of E∈P in Q, these definitions
allow to "measure the size" of E (finding whether it is finite or infinite,
and what is its number of elements if it is finite), by making it easy (but still nontrivial),
through the fact that (Dom K)∪{(S,e)} = (^{{0,S}}Q)
to prove that things fall into either case:
 If E is finite, e∈ Min Q, and Q is a ground term with
root e representing the number of elements of E ;
 If E is infinite, e∉ Min Q, and Min Q is a ground term algebra
(thus a model of arithmetic), whose preimage is the set of all finite subsets of E.
Assuming the axiom of infinity, the finiteness of a set E is equivalent to the existence of a
number n∈ℕ and a bijection from
V_{n} = {x∈ℕ  x<n} to
E; or a surjection from V_{n} to
E, which is then bijective precisely when n takes its smallest value
(the number of elements of E).
Without ℕ, either ℘(℘(E)) or (with more
work) E^{E} can be used to express the
finiteness of a set E, and to rebuild ℕ from E
if E is infinite.
Any left cancellative element of a finite monoid is invertible.
Thus any finite cancellative monoid is a group.
Proof: it acts as an injective transformation of
a finite set, thus a permutation, by which the preimage of e is a right inverse, thus an inverse.
Countability of ℕ×ℕ
y\x

0

1

2

3

4

0

0

1

4

9

16

1

2

3

5

10

17

2

6

7

8

11

18

3

12

13

14

15

19

A natural bijection between ℕ×ℕ and ℕ is defined by
(x,y) ↦ (y < x ? x⋅x + y : y⋅y +
x + y).
y\x

0

1

2

3
 4

0

0

1

3

6
 10

1

2

4

7
 11

2

5

8
 12

3

9
 13

Another bijection
b_{2} :
ℕ×ℕ → ℕ
is defined as
b_{2}(
x,
y) =
T_{x+y}+
y
from the sequence (
T_{n}) of
triangular numbers
defined by
2⋅T_{n} = n⋅(n+1) (see
properties of parity) or equivalently by
T_{0}=0 ∧ ∀
n∈ℕ,
T_{n+1}=
T_{n}+
n+1.
This makes ℕ×ℕ a ground term (0,
S)algebra where
0=(0,0)
S(0,y)=(y+1,0)
S(x+1,y)=(x,y+1)
which recursively defines b_{2}^{1}(z), where
x+y is the only n such that
T_{n}≤z<T_{n+1}.
Countability of finite sequences of integers
If there is a surjection f from ℕ to a set E then E is countable, as an inverse
injection can be defined by associating to each x∈E its smallest preimage by f.
Fixing a bijection b_{2} from ℕ^{2} to ℕ,
for any integer n>0 we can recursively define a
bijection b_{n}:ℕ^{n}→ℕ, for
example:
b_{1}=Id_{ℕ}
∀n>0,∀u∈ℕ^{n},
b_{Sn}(u) =
b_{2}(b_{n}(u),u_{n})
(which gives back b_{2} as the particular case of
b_{n} for n=2).
Also the set ℕ^{(ℕ)} = {u∈ ℕ^{ℕ} 
∃k∈ ℕ, ∀n>k, u_{n}=0} is countable.
There are different ways to see it:
 A sequence of bijections h_{n} : ℕ↔
E_{n}, gives a surjection ∐_{n∈ℕ}
E_{i} ≈ ℕ×ℕ →
U=⋃_{n∈ℕ} E_{n}
so that taking E_{n}=ℕ^{n} we find that
U=ℕ^{(ℕ)} is countable.
 With the decomposition in prime numbers
 As the binary representation maps ℕ to the set 2^{(ℕ)} of finite
subsets of ℕ, it also maps ℕ^{(ℕ)}
to the set 2^{(ℕ×ℕ)} of finite subsets of ℕ×ℕ.
But this construction of ℕ^{(ℕ)}) and similarly simple candidate
expressions of H as a countable set, assumes recursion, thus cannot be
used to define recursion by the above method. To actually provide a definition of
recursion that does not assume it, requires a different expression of an enumerated
H. The representation of sequences which was used by Godel
as a basis to define recursion, actually forms a different set.
4.6. The Completeness Theorem
Existence of countable term algebras
For any countable algebraic language L with at least a constant and a
nonconstant, finding a countable ground term Lalgebra (necessarily infinite)
amonts to defining a ground term Lalgebra structure on
ℕ, which is a bijection from ^{L}ℕ to ℕ.
Splitting L as C∪D where C is the set of
constants, and D is the rest of symbols, we have ^{L}ℕ
= C∪(^{D}ℕ). But C and D
are countable (either finite or infinite), and ^{D}ℕ is a union
over D of disjoint sets with explicitly definable bijections with ℕ
(such as the b_{ns} we saw).
In any case, a bijection between C∪(^{D}ℕ)
and ℕ can be found without problem.
In practice, such bijections from ^{L}ℕ to ℕ
happen to be ground term Lalgebra structures because
∀(s,x)∈^{D}ℕ,
∀i<n_{s},
x_{i}<s(x) which would be contradicted
by the smallest element outside Min_{L} ℕ.
∎
Interpretation of firstorder formulas
Trying to extend the formal construction of
the interpretation of terms in algebras, to the case
of formulas interpreted in systems, the difficulty is to cope with the
interpretation of quantifiers (or generally binders, if we wish to still generalize).
A possibility, is to switch to a view over all variables as bound throughout the formula:
from the concept of interpretation h_{v}∈E^{T} of a term T
in an algebra E for every interpretation v of its set V of variables, the
family (h_{v})_{v∈EV}
is recurried into a function from T to E^{EV}.
So, a firstorder formula interpreted in a system E can be understood as a term
interpreted in an algebra with maybe two base types : the sets Op_{E} and
Rel_{E } of all operations and all relations in E; or split as two sequences
of types, Op_{E}^{(n)} and Rel_{E}^{(n)}.
We might not need the full sets of these, but at least, an algebra of these (a subset stable
by all needed logical operations).
We took unions over ℕ for the case we would need to see "all possible formulas" as terms
interpreted in one same algebra.
The Completeness Theorem
Any good formal proving system (a theory describing proof syntax, verifiable by an algorithm)
needs of course to be sound, which means only
"proving" what is always true (the provability of a formula implies its truth in every model).
More remarkable is the converse property, that is completeness :
Theorem. Firstorder logic has a proving system both sound and complete
in the following equivalent senses
 Any consistent
firstorder theory T with countable language
has a countable model.
 Any formula true in all models of such a theory is
deducible from its axioms.
This quality of perfection, established for a certain formal proving system for
firstorder logic, ensures that any other formal proving system with the same quality
will be necessarily equivalent : any formal proof according to one is automatically
convertible into a proof according to any other.
Sketch of proof of the first statement (implicitly suggesting how such a proving
system can be made; not using
the axiom of choice, anyway out of topic):
Express axioms in prenex
form, that is chains of
quantifiers applied to quantifierfree formulas (using equivalences
from 2.1 and 2.3 simplified for a nonempty model).
Interpret the symbol = in axioms as an ordinary predicate
symbol, with the axioms of
equality [1.6].
Replace each occurrence of ∃ in an axiom by the use of an additional
operator symbol K, for example
(∀x,x', ∃y, ∀z,
A(x,x',y,z))
⇢ (∀x,x',∀z,
A(x,x',K(x,x'), z)).
Let M be the ground term algebra over the language of
operator symbols enriched as just described. Reinterpreting all ∀
in axioms as the use of axiom schemas (one axiom for each replacement of variables by a
tuple of elements of M), gives a propositional
theory T' (its axioms are composed of logical
connectives over Boolean variables), whose set of Boolean
variables is ^{P}M where P is the set of
predicate symbols in the theory plus the "equality" symbol.
Observe that T' is still consistent, as any contradiction
in T' (= finite set of axioms not satisfied by any tuple
of Boolean values of their variables) would provide a
contradiction in T, as follows:
From all subterms occurring in used axioms of T', list without repetition all those
whose root is a symbol S which was added to the
language when converting some axiom
∀x,∃y,∀z,∃u,
A(x,y,z,u)
of T, into the axiom ∀x,z, A(x,K(x),z,
S(x,z)) in T'. Successively replace them all by variables
in T: for terms
S(t_{0},t_{1})
and S(t_{0},t_{2})
(where t_{0}, t_{1}, t_{2}
∈ M), the reasoning in T will say
"Let y such that ∀z,∃u,
A(t_{0},y,z,u);
let u_{1} such that
A(t_{0},y,t_{1},u_{1});
let u_{2} such that
A(t_{0},y,t_{2},u_{2});"
and use the contradiction in T' where y replaces
K(t_{0}), u_{1} replaces
S(t_{0},t_{1}) and u_{2}
replaces S(t_{0},t_{2}).

Recursively by a chosen enumeration of ^{P}M as a countable set,
add one by one to the axioms, each of these Boolean variables
if it is consistent with previously accepted axioms, so that all
get values without contradiction.
Then the quotient
of M by the equivalence relation of "equality", forms a model (with the "true
equality"). ∎
As this construction depends on an arbitrary order between formulas, different
choices give different models, which may be nonisomorphic and even have different
properties reflecting the undecidability of the theory's formulas.
Deduction of the second statement from the first :
T⊢ A
⇔ T ∪ {¬A} is inconsistent
⇔ T ∪ {¬A} has no model
⇔ A is true in all models of T. ∎
So, the provability function giving the set of theorems from each set of axioms,
is the closure of the Galois
connection defined by the truth relation R ⊂ X×Y between
 the set X of ground formulas using some language L
 the
set Y of Lstructures on ℕ or a subset of it (sufficient representatives of
the class of all Lsystems).
However, as already announced in truth in mathematics and will be shown
by the incompleteness
theorem, unclarities remain about provability and existence of models:
 The proven equivalence between consistency and existence of a model, does not inform
whether these are both true, or both false:
 Provability, if true, can stay
practically unknowable: if a proof exists, nothing says how to find it; it may be
too big to be ever given.
 The consistency of a theory may be true but unprovable: completeness only ensures
that, in this case (and it may be undecidable whether it is the case or not), there also exists
universes in which, equivalently, this theory is inconsistent and it has no models.
 Such constructions of models as provided by the above proof, are
not really effective, as they are not algorithmic:
they require an infinity of steps, each of which involves an infinite
knowledge (knowing if a formula remains
consistent with previously accepted ones, which is the answer
to a halting
problem of search for contradiction). Actually, most
foundational theories such as set theories, do not have any
algorithmically definable model.
Skolem's Paradox
Comparing the results of the completeness theorem with Cantor's theorem gives this paradox :
If set theory is consistent then it has countable models, though
it sees some sets there, such as ℘(ℕ), as uncountable.
 A countable model U interprets the powerset "℘(E)" of an
infinite "set" E∈U as the "set" P of all objects in U which play
the role of subsets of E (but may differ from these when U is nonstandard); as P
is metacountable, it cannot exhaust the uncountable metapowerset of "all" subsets of
E.
 As P is metacountable, it externally has a bijection with ℕ or U;
but such bijections "do not exist" (have no representatives) as objects in U.
Rigorously speaking, when the powerset
axiom says that the class of subsets of E is a set written ℘(E), it
can only determine the interpretation of the functor ℘
relatively to (depending on) the universe where its open quantifiers are
interpreted: «all subsets
of E existing in this universe are in ℘(E)».
In the other interpretation
of what it means for a class to be a set, this would mean that the universe
already contains "really all" subsets of E, forming the supposedly
"true" set ℘(E) which will stay fixed in any further expansion
of the universe. However, for the powerset of an infinite set, this wish
cannot be expressed in firstorder logic nor any other conceivable
mathematical formalism:
there is no way to talk about metasets that "cannot be found" in this universe
but would «exist elsewhere» (in any mysterious bigger universe) to exclude them
from there.
(Only one aspect of this idea can be formalized as the axiom schema
of specification).
4.7. Nonstandard models of Arithmetic
Standard and nonstandard numbers
Since the induction axiom
needed to determine the isomorphism class of ℕ depends on
℘(ℕ), the relativity of ℘ allows a diversity of nonisomorphic
models of arithmetic respectively defined by the diverse models of any consistent
firstorder theory T which contains arithmetic. Many theories may be
picked in the role of T, such as a set theory seen as a firstorder theory, thus
involving other notions than numbers (to define more sets of numbers than
arithmetically defined classes). All we shall assume here is that it has a notion N
of "natural number" with a constant 0, a function symbol S, and axioms
making N a model of bare
arithmetic (in any model of T), thus a bijective {0,S}algebra.
A number in N is called standard if it belongs to the
minimal
subalgebra N_{0} = Min_{{0,S}}N,
isomorphic to ℕ by the unique {0,S}morphism
(embedding,
n↦S_{N}^{n}(0_{N}))
from ℕ to N. So, it represents an element of ℕ,
which may be called a metanumber.
A model N of arithmetic is called standard if it
is a minimal {0,S}algebra, which can be equivalently written in 3 ways:
 It satisfies the full induction axiom (in terms of powerset);
 It is isomorphic to ℕ (also called the standard
model of arithmetic);
 All its elements are standard.
We shall abbreviate some works of
firstorder logic by set theoretical notations as follows :
 Each metanumber n∈ℕ will be confused with the ground term
"S^{n}(0)" and its value as a standard number;
 The quantifier "∀n∈ℕ" at the root of a formula, means to declare a schema of one formula per value of
n in ℕ;
 For each n∈ℕ, the quantifier ∀x<n (resp.
∃x<n) can equivalently be read using x as an object (∀x,
x<n ⇒), or as a string of conjunctions (resp. disjunctions)
of n copies of the subformula with each value of x as a
metanumber lower than n.
Existence of nonstandard models
The nonstandardness of N is expressible by axioms on an additional
structure, forming an extended theory T'. One way is to add 
A constant symbol k with range N (which may need the
axiom k∈N);
 The schema of axioms n ≠ k for each
n∈ℕ, making the number k nonstandard.
If T is consistent then T' is also consistent (and cannot prove more),
as any finite list of axioms of T' can be satisfied in any model of T
(by interpreting k as a different number). Thus,
T' also has
a model, which is a model of T where N is nonstandard.
This means that no consistent extension of arithmetic can ever force its
model of arithmetic to be standard, i.e. require induction to apply to the full
powerset of N, which it cannot ensure to exhaust by its classes.
Candidate "standardness" predicates may be introduced but still cannot be
forced to coincide with the true standardness (N_{0}),
which may stay a metaset beyond all classes.
Any model of arithmetic obtained as described in the proof of the completeness
theorem from any consistent extension of arithmetic, will necessarily be nonstandard,
as it cannot even be elementarily
equivalent to ℕ according to the truth undefinability theorem.
Skolem's paradox
still holds in two ways:
 the metacountable set P interpreting "℘(ℕ)", whose elements serve as
subsets of N, still cannot exhaust ℘(N) which is also metauncountable
(on the meta level, bijections between sets N and ℕ induce bijections
between their powersets, which preserve uncountability);
 the image of P projected to ℘(ℕ) by taking preimages by the embedding
from ℕ to N,
does not fill ℘(ℕ) either.
Nonstandard models behave much like standard ones, as they satisfy
all consequences of induction. Their precise range of diversity depends on
the chosen theory of arithmetic.
Nonstandard models of bare arithmetic
The only "addition" definable from S, is the metaoperation adding any
n∈ℕ to any x∈N as
x + n = S^{n}(x), that is the metasequence of functions
(S^{n})_{n∈ℕ}
each defined in the theory by a unary Sterm n.
The consequences of the induction schema in bare arithmetic can be summed up as
 The bijectivity of N as a {0,S}algebra, which
implies the bijectivity of S on the set of nonstandard numbers
 The schema of formulas
∀n∈ℕ*, ∀x∈N,
x + n ≠ x which is a weak version of (F).
As the restriction of S to the metaset N\N_{0}
of nonstandard numbers of any model is a permutation, N\N_{0}
is a ℤset.
The last formula obliges this ℤset to be free. Conversely, the disjoint
union of ℕ with any free ℤset, forms a model of bare arithmetic.
Applying both ways the definition of the order from the partial metaoperation
of addition, gives two ordering results with nonstandard numbers:
 Each ℤorbit of nonstandard numbers has its own total order.
 Each nonstandard number is greater than each standard number, thus
may be called «infinitely big».
Models of arithmetic
with order, are formed as models of bare arithmetic with any
choice of a total order on the partition of nonstandard numbers in ℤorbits.
Thus, bare arithmetic cannot suffice to define the order. But arithmetic with
order cannot suffice to define addition either, as its nonstandard models
may either admit no or many corresponding interpretations of addition.
Nonstandard models of Presburger Arithmetic
Such models satisfy all theorems
of Presburger Arithmetic. In particular they have a welldefined total order, by
which any nonstandard number is greater than any standard number,
and any nonempty class of numbers has a smallest element
(which the metaset of nonstandard numbers hasn't).
Here are some more details only for the sake
of illustration, which may be skipped.
There is also a metaoperation (sequence of functions) of multiplication of an
x∈N by a standard number n∈ℕ : n⋅x =
x+...+x (with n occurrences of x)
Beyond commutativity, associativity and the seen properties of the order, the last independent
consequence of the axiom schema of induction constraining
nonstandard models, is the possibility of Euclidean division by any nonzero standard number
(generalizing the results on parity) :
∀d∈ℕ*, ∀x∈N, ∃q∈N,
∃r<d,
x = d⋅q + r
thanks to ∀d∈ℕ*, ∀q∈N, d⋅(q+1) =
d⋅q+d which is a schema of theorems in Presburger arithmetic.
Moreover this (q,r) is unique; q = x:d∈N
is called the quotient and r is called the rest of the division of an
x∈N by a d∈ℕ*, so that
∀q∈N,
q=x:d ⇔ d⋅q ≤ x< d⋅(q+1) ⇔ ∃
r<d, x = d⋅q + r.
The concept of model of Preburger arithmetic generated by a set
(of nonstandard numbers, since standard ones have no generating effect), is defined as
that of subalgebra generated by a subset
for the "algebra" (not exactly an algebra, but...) with language completed, like in the proof of
the completeness theorem, by additional operation symbols reflecting all existence properties
deduced from the axiom schema of induction:
 The subtraction of a number by a lower number (or the absolute value of subtraction),
which was implicit in the definition of the order and
the proof that it is total;
 The sequence of functions (x↦ x:d) of Euclidean division
by each d∈ℕ*.
They can be conceived either in the abstract (by evaluating relations arbitrarily,
like in the proof of the completeness theorem) or as a subset of a given model
(interpreting expressions there).
In particular, in any model of Preburger arithmetic generated by a single element
(nonstandard k∈N), the set of nonstandard elements is the set of
all values of expressions of the form (a⋅k):d +b
where a,d ∈ℕ* and b∈ℤ (the cases where a,d
are relative primes suffice).
The predicate of divisibility of x∈N by a d∈ℕ*, is defined as the
case when the rest cancels:
dx ⇔ (∃q∈N, x = d⋅q)
The possible shapes of these models with respect to k (classes of isomorphisms
preserving k, described using it), are classified by the sequence
(r_{d})_{d∈ℕ*} of rests of the division of k by all
standard numbers d. The possible sequences are those which satisfy not only
r_{d}<d but also the compatibility formulas :
∀n,d ∈ℕ*, ∃h,
r_{d⋅n} = d⋅h + r_{d}
(where in fact h<n). The simplest one is where all r_{d}
are 0, i.e. where k is divisible by every standard number (but the distinguishing property
of this isomorphism class of models with 1 generator, "there exists a number divisible by
every standard number", is inexpressible in Presburger arithmetic).
The nonstandard models generated by 2 nonstandard numbers
k,k' can be split into the following classification depending
on what may be intuitively described as the (standard) real number which
k/k' is infinitely close to:
 k/k' may be infinitely large or infinitely small;
 It may be close to an irrational number
 But the cases when it is close to a rational number
a/b for standard numbers a, b, are reducible to other cases:
 If the difference between b⋅k and a⋅k'
is standard then the model is actually generated by only one element
(any nonstandard element is a generator).
 If this difference is nonstandard then, replacing one generator
by this difference, reduces this model to the first case.
4.8. Developing theories : definitions
Given a theory
T (with types, structures and axioms), a development
of T is a extended theory T' = T∪(pack of
extra components) which remains «equivalent» to T.
This concept has 3 aspects:
 In which sense is T' «equivalent» to T :
 For any extension T' of T, any model of T'
defines by restriction a unique model of T ;
 Such a T' is qualified a development of T if
conversely, any model of T has a «unique extension» as a model
of T', in a sense we need to specify.
 A list of developments schemes, where each is the data of a pair
(X,Y) of theoretical components (a subtheory X of a theory
Y) so that any morphism from X to a theory T allows to add to
T a copy of the rest of Y beyond its subtheory X
identified as its image in T. A list of developments schemes
is sufficient when any legitimate development is producible by a succession
of steps each described by one of these schemes.
 On the formal side: how, for each such scheme, the use of extra components in
works (expressions, proofs...) with T' can be translated
into (usually longer) works with T, and thus be seen as
abbreviations of them.
There are 3 levels of development with their respective schemes:
 A proof only adds one ground formula to the axioms, as this
formula is shown to be a theorem (deduced from some of the previous axioms).
 A definition adds both a new structure symbol and a
new axiom.
 A construction adds altogether a new type, new
structure symbol(s) and new axiom(s).
The use of a theorem as an available axiom for the proofs of the
next theorems, abbreviates a repetition of its proof as a part of
the next proofs (with possible substitutions of variables by terms
to which the theorem is applied).
When inserting theories in the set theoretical framework,
constructions become set theoretical definitions, which is why the
distinction between definitions and constructions is not usually
clarified in the literature.
The Galois connection (Mod,Tru)
For any language L, the truth relation between ground formulas and systems defines
a Galois connection (Mod,Tru), where Mod gives the class of models of any set A
of ground formulas taken as axioms, while Tru gives the set of true formulas which all given
systems have in common. Replacing
the class of all systems by the set of all Lstructures on ℕ, leaves unchanged and
thus gives definite sense to the closure Tru০Mod. All theorems of a theory belong to the
closure Tru০Mod(A) of axioms, which is the condition for a formula to leave
unchanged Mod A when it is added to A.
Schemes of definitions
We have 3 schemes of definitions:
 A formula φ defines a new relation symbol R with
arguments the free variables of φ, with the new axiom
∀(variables), R(variables)⇔φ(variables).
The use of R can be replaced by the use of φ as a
subformula of other formulas (replacing the free variables of φ by
the terms used as arguments of R).
 A term t defines an operation symbol S,
with the axiom ∀(variables), S(variables)=t(variables).
This S abbreviates, and can be replaced by, its defining term t.
 Given a formula φ(variables, x), if we have
(∀(variables),∃!x, φ(variables, x)) then it defines
a new operation symbol S, with the new axiom
∀(variables), φ(variables, S(variables)). This
scheme may be split in 2 steps : the definition of a
relation symbol R by φ (by the first scheme); then a reduced
version of the last scheme directly using R instead of a
formula φ. This case was discussed with the uniqueness
quantifiers (2.4).
Extending models by undefined structures
Thanks to the completeness
theorem, if every model of T can be extended as a model of a T' =
(T∪{R,A}) where R is a new symbol
and A is a new (set of) axiom(s), then every ground formula of T
provable in T', is also provable in T.
The converse may be wrong: a theory T may be extensible to a theory T'
unable to prove more of its formulas, but to which not all its models are extensible.
Here are some examples from nonstandard
models of arithmetic :
 T is any arithmetic and T' expresses nonstandardness by letting
R be a constant (number), and A the axiom schema making it nonstandard.
 The other expression of nonstandardness by a unary predicate symbol R which may mean the standardness predicate in a nonstandard model, as A says the
the induction axiom fails on R: R(0) ∧ (∀x, R(x)
⇒ R(S(x))) ∧ (∃x, ¬R(x))
 T = bare arithmetic; T' = Presburger arithmetic
 T = Presburger arithmetic; T' = full arithmetic (with addition and multiplication)
Definitions extend models
For any theory T with a model E, extensions T' of T
by an additional axiom and/or structure symbol may have different effects:
 If T' only has a new axiom A then E may stay or
not as a model of T', depending whether A is true or false in E;
it always does if A is provable from previous axioms;
 If T' only has a new symbol then E may have several extensions as
models of T' by giving this symbol arbitrary interpretations, except for special cases
 Definitions precisely combine a new symbol R and a new axiom A,
so that any model of T has a unique extension to an interpretation of R
that satisfies A, forming a model of the extended theory
(T∪{R,A}).
The uniqueness of the extension for every E, means that in the doubly extended theory
(T∪{R,A,R_{1},A_{1}})
where (R_{1},A_{1}) is a copy of (R,A),
one can prove
∀(variables), R⇔R_{1}
Definitions preserve sets of isomorphisms
For any isomorphism f between models E
and F of T, with respective extensions as models E'
and F' of a theory T' extending T by further structures and axioms,
f may stay or not as an isomorphism between E'
and F', i.e. preserve the interpretation of the new structure(s). It will be an
isomorphism whenever the additional axiom(s) form a definition, determining the new
structure(s) and thus making it invariant by isomorphisms. Thus, adding a defined structure to a theory
preserves the sets of isomorphisms between its models.
In particular, any relation defined by an expression with language L⊂R without parameters
is invariant by automorphisms, so is in its closure
Inv(Aut_{L} E).
This means that adding it to L preserves Aut_{L} E.
As we saw how the switch from models to isomorphisms provides similarities between development levels
from proofs to definitions, we shall now see it also providing similarities from definitions to constructions,
making sense to how constructions also essentially preserve theories.
4.9. Constructions
Diverse construction schemes let new types play the roles of sets defined in set
theory by operations between sets named by previous types:
Each of the following schemes suffices to produce both others through the use of previous ones:
 From a type E, a binary relation R on E and the theorem
making R an equivalence relation (∀_{E }x,y, xRy
⇔ (∀_{E }z,xRz⇔yRz)), we can construct a
type Q in the role of the quotient E/R
with a function symbol q:E→Q, and axioms
 ∀_{E }x,y, q(x)=q(y)
⇔ xRy
 ∀_{Q }x, ∃_{E }y, q(y)=x
Any structure S(u,v,...,k) with an argument k of type Q,
abbreviates a structure S'(u,v,...,x),
where x is of type E, with the axiom
∀u,v,...∀_{E }x,y, xRy ⇒
S'(u,v,...,x)=S'(u,v,...,y)
(thanks to properties of equivalence
relations and quotient)
 A type of unary relations: from 2 types E,F
and a relation R between them, we construct the image Q
of E in ℘(F) by the curried R, by 2 new
structures
 a function q:E→Q
 a relation R' between Q and F,
and axioms
 ∀_{Q }x,∃_{E }y, q(y)=x
 ∀_{E }x,∀_{F }y, q(x)R'
y ⇔xRy
 ∀_{Q }x,y, (∀_{F }z, xR' z ⇔
yR' z) ⇒ x=y.
Or equivalently,∀_{E }x,y,(∀z∈F,
xRz ⇔ yRz)⇒ q(x)=q(y)
The last 2 axioms are together equivalent to
 ∀_{E }x,∀_{Q }y,
(∀_{F }z,
yR' z ⇔xRz) ⇔ q(x) =y.
 A type of structures K of any kind defined by a
fixed expression with parameters, meaning all structures
defined by this expression with all values of parameters. Its structures are:
 A quotient operation, from parameters to K
 An evaluator, interpreting K as a set of structures.
The last one can be obtained by composing constructions of products
(to collapse bound variables as one, and the same for parameters),
a definition and a type of unary relations or functions
(either as particular relations, or by adapting the form of axioms, replacing ⇔ by = ).
A development scheme at each level looks like a component at the
next level
Despite their differences of nature, the 3 levels of development
have remarkable similarities:
 A construction of a type of structures is given by a variable structure,
that is a structure symbol with a selection of variables to play
the role of parameters. Structures in the language are invariant, i.e.
without parameter.
This construction is worthless if the chosen symbol is without parameter
(or behaving as such: independent of parameters) which would give singleton; or
without other variable, as it would give the Boolean type.
 Definitions look like axioms: a definition of a predicate is given by a formula
with free variables; axioms are chosen from ground formulas. Any formula
merely defining a Boolean constant, i.e. with value depending only
on the model and not on variables, such as ground formulas or provable formulas
(in the sense that any free variables are implicitly
bound by ∀), do not play any effective role of structures of the
described system (giving roles to objects). Predicates defined without using the language,
are not structuring either.
 As systems using axioms, proofs are similar to contradictions. A
contradiction
is a kind of proof with no theorem but 0 (False),
which would be a very bad axiom. We might regard contradictions
as a 4th kind of component of theories after types, symbols and axioms; not
only the list of given contradictions should be empty for a theory to be of interest,
but the set of possible contradictions should be empty as well.
How constructions preserve isomorphisms
From any theory T, consider any extension T' =
T∪X∪R∪A
where X is a type, R is a pack of structures and A
is a pack of axioms. The existence of an extension of
a given model of T as a model of T', is
a matter of A being small enough for these X and R.
Its uniquess would not make direct sense as any identical copy would also fit.
But extensions may still be qualified as
«essentially unique»
(being all copies of each other) giving sense to how
constructions preserve models, depending on the set of isomorphisms
between them. For any models E'
and F' of T' respective extensions of models E
and F of T, and any isomorphism f : E
→ F,
 An extension of f as an isomorphism from E' to F' will have
to exist if A suffices to "determine" (make essentially unique) the
extension of the model (interpretation of X and R) in the following
sense: any two extensions are isomorphic (making unique the isomorphism class
of extended models E'), by some isomorphism whose restriction to old types is
the identity.
Therefore in this case, any formulas in T' without free variable in the new type
are provably equivalent to formulas expressed in T, may they be ground formulas
(as they describe the extended model) or with some free variables in old types
(as they may define structures on previous types, which the isomorphisms must preserve).
 The uniqueness of the extension of f is a matter of T' having enough
structures to prevent E' from having any more symmetry (nontrivial
automorphism) than E.
For example if R is empty, if the interpretations X and X' in E' and
F' are equinumerous then any bijection between them extends f
as an isomorphism between E'
and F'; this is nonunique when X has at least 2 elements.
 The extension T' of T is a
construction of X in T, when it ensures both the existence
and uniqueness of an extension of f to X as an isomorphism
from E' to F'. This can be formally verified in the doubly extended
theory T''=
(T∪X∪R∪A∪X'∪R'∪A'),
by defining without parameter, a function from X to X',
and proving that it is a bijection extending Id_{E} as
an isomorphism j
between both models E' , E'' of T'
obtained by restricting a model of T'' to copies
(T∪X∪R∪A)
and (T∪X'∪R'∪A') of T'.
Indeed in this case, any 2 isomorphisms g,h from E' to F'
with the same restriction to E, will be equal because
The automorphism h^{−1}০g of E'
extended by Id_{X'} forms an automorphism of the model
(E'∪E'') of T''. As j is invariant, it stays equal
to its image j০(h^{−1}০g)^{−1}
by this automorphism. Therefore h^{−1}০g
= Id_{E'}
, i.e. g=h.
What we can see here strictly preserved by constructions, is the class of isomorphisms as an
abstract category. In particular, constructions
leave unchanged the automorphism groups seen as abstract groups, providing more types on which they act.