4.4. 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. Somehow, the main framework for arithmetic is second-order logic, but this leads to other versions depending on how second-order logic itself comes down to other frameworks.
Let us start with the set theoretical arithmetic, most precise arithmetic expressible in a strong enough set theory, interpreting second-order quantifiers by the powerset symbol. Namely, that is the set theoretical definition of "the standard ℕ", or rather of its isomorphism class, relative to the given universe (it amounts to defining the class of "finite sets", which are measurable by their number of elements, as we shall define in 4.5).

Definition. The set ℕ of natural numbers is a unary term {S}-algebra where S is a function symbol called the successor ; also expressible as a ground term {0,S}-algebra where 0 (zero) is a constant symbol.

The existence of such a system is our first expression of the axiom of infinity. Let us formalize it by inserting arithmetic into set theory, in the form of 3 constant symbols ℕ, 0, S with the following axioms :

0 ∈ ℕ ∧ S : ℕ → ℕ : ℕ is a {0,S}-algebra
(H0) n∈ℕ, Sn ≠ 0 : 0 ∉ Im S
(Inj) n,p∈ℕ, Sn = Sp n = p : S is injective
(Ind) A⊂ℕ, (0∈A ∧ ∀nA, SnA) ⇒ A=ℕ : 0 generates ℕ (induction axiom).

More constant symbols can be defined from there:
1 = S0
2 = S1 = SS0
and so on.

This completes our axioms of set theory up to the strength of Mc Lane set theory, which essentially forms (with the axiom of choice) the most commonly used foundational theory for mathematics. It will imply the existence of term algebras with any language.
This definition of ℕ may be criticized as circular, for involving concepts of algebra we initially introduced using ℕ as set of possible arities of symbols. But these concepts may be re-written up to this point without this use, by restriction to the use of symbols with small arities (0, 1, 2).

Recursively defined sequences

Each n∈ℕ represents a function symbol Sn defined by a unary S-term and interpreted in each S-algebra (E,f) as a function f nEE.

A sequence of elements of a set E, is a family u : ℕ → E. It is called recursive when it is a morphism for a given S-algebra structure on E, i.e. defined by choices of aE and fEE :

u ∈ Mor{0,S}(ℕ, (E,(a,f))) ⇔ (∀n∈ℕ, un = f n(a))
⇔ (u0 = a ∧ ∀n∈ℕ, uSn = f(un)).

Intuitively, each f n(a) abbreviates the term with n occurrences of the function symbol f, and variable a :
f 0(a) = a
f 1(a) = f(a)
f 2(a) = f(f(a))

The sequence (f n) is itself recursively defined by f 0 = IdE ∧ ∀n∈ℕ, f Sn = ff n.
In particular, f 1 = f and f 2 = ff.
Generally for any fEE, gEX, the recursive sequence h : ℕ → EX defined by h0 = g ∧ ∀n∈ℕ, hSn = fhn, is hn = f ng.

Addition

The basic properties of addition and multiplication in ℕ become obvious when seeing natural numbers as measures ("cardinals") of finite sets, as will be defined in 4.6. But let us take here as an exercise to prove them independently.
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 the 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 = Sp(n), or recursively as

n + 0 = n
p∈ℕ, n+S(p) = S(n+p)
n+1 = S(n+0) = Sn

The action axiom ∀fEE, ∀n,p∈ℕ, f n+p = f pf n is deducible like for any term algebra:
(f n+0=f n ∧ ∀p∈ℕ, f n+Sp = f S(n+p) = ff n+p) ∴ ∀aE, (pf n+p(a))∈Mor(ℕ,(E,f n(a),f)).
It gives associativity : (a+b)+n = Sn(Sb(a)) = Sb+n(a) = a+(b+n), which will be used implicitly, omitting parenthesis.

Multiplication

Let us define multiplication in ℕ as yx = (Sx)y(0) (this choice of sides fits common language, unlike the usual one from the literature, until the distinction disappears by the proof of commutativity). In recursive formulation, the latter coming as (Sx)Sy(0) = Sx((Sx)y(0)).
Then generally, ∀fEE, f xy = (f y)x.
x∈ℕ, x⋅0 = 0 is deduced by induction.
Right distributivity ∀x,y,z∈ℕ, (x+y)⋅z = xz + yz comes by induction on y, or as (Sz)x+y = (Sz)y⚬(Sz)x.
Left distributivity ∀x,y,z∈ℕ, x⋅(y+z) = xy + xz comes by induction on x using commutativity of +. In particular this gives ∀x,y∈ℕ, xSy = (xy)+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,gEE, gf = IdE ⇒ ∀n∈ℕ, gnf n = IdE.

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 = (fn)-1f.

The system of (relative) integers ℤ is defined as the {0,S}-algebra where 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 (EE, IdE, f), or an action of ℤ on E interpreting 1 as f.

Proof: the {0,S}-morphism condition requires on ℕ the same nf n as above; on -ℕ, it recursively defines f -n = (f -1)n, namely 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.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Arithmetic and first-order foundations
4.1. Algebraic terms
4.2. Quotient systems
4.3. Term algebras
4.4. Integers and recursion
4.5. Presburger Arithmetic
4.6. Finiteness and countability (draft)
4.7. The Completeness Theorem
4.8. More recursion tools
4.9. Non-standard models of Arithmetic
4.10. Developing theories : definitions
4.11. Constructions
4.A. The Berry paradox
5. Second-order foundations
6. Foundations of Geometry