3.6. Arithmetic with addition
Firstorder theories of arithmetic
Our first formalization of ℕ
was based on the framework of set theory, where it used the powerset to characterize ℕ in an
"essentially unique" way (specify its isomorphism class). It allowed recursion,
from which we could define addition and multiplication.
Let us now consider formalizations in the framework of firstorder logic, thus
called 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 without the set theoretical framework we used to express and justify the definiteness
of recursive definitions, the successor function no more suffices to define addition and
multiplication. 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, with addition, starts to be interesting, but still cannot define multiplication.
 Full arithmetic, with addition and multiplication, is finally
able to express all recursive definitions.
Presburger arithmetic
Presburger arithmetic has been proven by experts to be a decidable theory, i.e.
all its ground formulas are either provable or refutable from its axioms. Let us
present its shortest equivalent formalization, describing the set ℕ* of nonzero natural
numbers, with 2 primitive symbols: the constant 1 and the operation +. Axioms will be
∀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 let us regard our present
use of set theoretical notations as mere abusive abbreviations of works in firstorder logic,
as long as we only consider subsets of ℕ* defined by firstorder formulas in this arithmetical
language. In particular, (Min) will be meant as abbreviating a schema of axioms with 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}) by the above proposition.
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).
(Ind) ⇒ (Min) :
∀A⊂ℕ*, the set A_{0}= A∪{0}
satisfies 0∈A_{0} and
(1∈A ∧ (∀x,y∈A, x+y ∈A))
⇒ (S0∈A_{0} ∧ (∀x∈A, Sx=x+1
∈A⊂A_{0})) ⇒ A_{0}=ℕ∎
(As ∧ Min) ⇒ (Ind)
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∎
(F) ⇔ (∀x∈ℕ*, ∀y∈ℕ, x+y ≠ y)
because x+0 = x ≠ 0.
(Inj ∧ Ind ∧ A1) ⇒ (F) : ∀x∈ℕ*,
x+0 ≠ 0
∀y∈ℕ, x+y ≠ y ⇒ x+y+1
≠ y+1∎
For the converse, we need to use the order relation.
The order relation
From the operation of addition, let us define binary relations < and ≤ on ℕ and
show that they form an order and its strict order (even in first order arithmetic);
its equivalence with the definition of the order
between terms in set theory in the common particular case of ℕ with full
set theoretical induction, will be left here as an intuitive fact.x<y ⇔ ∃z∈ℕ*, y =
x+z
x≤y ⇔ ∃z∈ℕ, y = x+z
These are consequences of (Ind ∧ A1) :
 < is transitive
 x≤y ⇔ (x<y ∨ x=y)
 x<y ⇔ x+1≤y
 ∀A⊂ℕ, A≠∅ ⇒ ∃x∈A, ∀y∈A,
x≤y (this may also be interpreted either set theoretically or as a schema in first order logic)
 ∀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}
 y = x+n ⇒ y+z = x+z+n
∎
(for 5. it is also possible to more directly prove for A={x∈ℕ
∀y∈ℕ, x<y ∨ x=y ∨ y<x}
that 0∈A and ∀x∈A, x+1∈A)
Now, (F) means that < is irreflexive, thus a strict total order
thanks to 1. and 5.
Moreover it implies ∀x,y,z∈ℕ, (x<y
⇔ x+z < y+z) and (x =
y ⇔ x+z = y+z), which
gives (Inj) as a particular case.
Proof: the direct implications were shown above; the converses are deduced from there as
< is a strict total order : one of (x<y, x
= y, y<x) must be true while only one of
(x+z<y+z,
x+z=y+z, y+z<x+z)
can.∎
Finally, ≤ is a total order with strict order < and
every nonempty subset of ℕ has a smallest element, which is unique by antisymmetry.
Arithmetic with order
It is possible to express a firstorder arithmetic with language {0,S, ≤}, stronger than {0,S}
but weaker than Presburger arithmetic, in the sense that addition cannot be defined from ≤.
Namely, it can be based on the characteristion of the order by the property:
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 by induction on n; its uniqueness for a fixed n
is deduced by induction on x.
Back to homepage :
Set theory and foundations
of mathematics
1. First foundations of
mathematics
2. Set theory (continued)
3. Algebra 1
3.1. Morphisms
of relational systems and concrete categories
3.2. Special morphisms
3.3. Algebras
3.4. Algebraic terms and
term algebras
3.5. Integers and
recursion
3.6. Arithmetic with addition
4. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Infinity and the axiom of choice
4.4. Nonstandard models of Arithmetic
4.5. How theories develop
4.6. The Incompleteness Theorem