3.8. Integers and recursion

The set ℕ

Any theory that aims to describe the system ℕ of natural numbers is called an Arithmetic. In details, there are several such formal theories, depending on the language (list of basic structures), and the logical framework (affecting the expressibility of axioms).

Our first "definition" of ℕ will characterize it in a set theoretical framework. This way of starting to formalize ℕ now may look circular, as we already used natural numbers as arities of operation symbols of algebras, of which arithmetic is a particular case. But this case only uses operation symbols with arity 0, 1 or 2, for which previous definitions might as well be specially rewritten without any general reference to integers.

Definition. The set ℕ of natural numbers is a ground term algebra with a language of two symbols: one constant symbol 0 ("zero"), and one unary symbol S.

The interpretation of S there is called the successor, understood as adding one unit (Sn=n+1).

This concept of ground term algebra can be expanded as the following 3 axioms on this {0,S}-algebra :
n∈ℕ, Sn ≠ 0
(H0), i.e. 0 ∉ Im S
n,p∈ℕ, Sn = Sp n = p (Inj), i.e. S is injective
A⊂ℕ, (0∈A ∧ ∀nA,SnA) ⇒ A=ℕ (Ind) : induction axiom (ℕ is a minimal (0,S)-algebra).

We can define 1=S0, 2=SS0...

This insertion of arithmetic into set theory, adding to set theory the constant symbol ℕ with some basic structure symbols interpreted in this ℕ, is the natural way to complete set theory (as we progressively introduced from the beginning to 2.5, + eventually the axiom of choice), to form the standard foundation of mathematics as practiced by most mathematicians. There is no uncertainty in choosing ℕ in the class of ground term {0,S}-algebras, since, as an initial {0,S}-algebra, it is essentially unique. The existence of ℕ is a form of the axiom of infinity, which implies the existence of term algebras of any language, as will be explained later.

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 uE such that u ∈ Mor(ℕ,(E,a,f)), where (E,a,f) is the {0,S}-algebra E interpreting 0 as aE and S as fEE :

n∈ℕ, uSn = f(un).

As un 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 integer n represents a term with symbols 0 and S respectively interpreted in E as a and f. 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))
In another curried view of this map from E×EE×ℕ to E we can re-interpret 0 as a variable instead of a constant symbol. Then each integer n becomes a term Sn with n occurrences of the function symbol S and one variable, interpreted in each {S}-algebra (E,f) as the function f nEE recursively defined by
f 0 = IdE
n∈ℕ, f Sn = ff n
In particular, f1=f.
More generally, for any functions fEE, gEX, the sequence of functions recursively defined by
n∈ℕ, hSn = fhn
is hn=f ng.


The operation of addition in ℕ can be defined as n+p = Sp(n), i.e. by the recursive definition
n + 0 = n
p∈ℕ, n+S(p) = S(n+p).
n+1 = n+S0 = S(n+0) = Sn
As ∀aE ,∀fEE, (pf n+p(a))∈Mor(ℕ,(E,fn(a),f)), i.e. fn+0=fn and ∀p∈ℕ, fn+Sp = fS(n+p) = ffn+p we have
n,p∈ℕ , f n+p = f pf n.
Addition is associative: (a+b)+n = Sn(Sb(a)) = Sb+n(a) = a+(b+n).
Recursive sequences are actions of this monoid of natural numbers (ℕ, 0 +), particular case of monoid of unary terms.


Multiplication in ℕ can be defined as xy = (Sx)y(0), so that

x∈ℕ, x⋅0 = 0
x,y∈ℕ, x⋅(Sy) = (xy)+x

More generally, for any aE and fEE, we have fxy(a) = (fx)y(a).

A more general form of recursion

Some useful sequences need recursive definitions where the term defining uSn uses not only un but also n itself. Somehow it would work all the same, but trying to directly adapt to this case the proof we gave would require to define some special generalizations of previous concepts, and specify their resulting properties. To simplify, let us proceed another way, similar to the argument in Halmos's Naive Set Theory, but generalized.
For any algebraic language L, let us introduce a general concept of "recursive condition" for functions u : EF, where, instead of a draft, E is first assumed to be an L-algebra (then a ground term algebra to conclude).
The version we saw was formalized by giving the term in the recursive definition as an L-algebra structure on F, φF: LFF, then expressing the request for u to satisfy this condition as u∈Mor(E,F), namely

∀(s,x)∈LE, u(sE(x)) = φF(s,ux).

Let us generalize this as u(sE(x)) = φ(s,x,ux) which by the canonical bijection Dom φ ≡ ∐sL Ens ×Fns ≡ ∐sL (E×F)ns = L⋆(E×F) can be written using h : L⋆(E×F) → F such that ∀(s,x,y)∈ Dom φ, φ(s,x,y) = h(s,x×y), as

u(sE(x)) = h(s,x×(ux)).

As ∀uFE, x×(ux) = (IdE×u)০x, this becomes the second component of the formula IdE×u ∈ Mor(E, E×F) when giving E×F the structure φE×F = (φE০πLh.
The first component (φE০πL) we give to φE×F, makes π∈ Mor(E×F, E) and makes tautological the first component of the formula IdE×u ∈ Mor(E, E×F), namely
IdE(sE(x)) = φE(s,x) = (φE০πL)(s,x×(ux)).
It is then possible to conclude by re-using the previous result of existence of interpretations:
If E is a closed term L-algebra then ∃!f ∈ Mor(E, E×F), which is of the form IdE×u because π০f ∈ Mor(E, E) ∴ π০f = IdE.
But one can do without it, based on the following property of this L-algebra E×F:

uFE, IdE×u ∈ MorL(E, E×F) ⇔ Gr u ∈ SubL(E×F)

The ⇒ is a case of image of an algebra by a morphism, Gr u = Im (IdE×u).
For the converse, the inverse of the bijective morphism π|Gr u ∈ MorL(Gr u, E) is a morphism IdE×u ∈ MorL(E, Gr u) ⊂ MorL(E, E×F).
This reduces the issue to the search of subalgebras of E×F which are graphs of functions from E to F.
Now if E is a ground term L-algebra then M = MinL(E×F) is one of them because π|M∈ MorL(M, E) from a surjective algebra to a ground term algebra must be bijective.
Any other subalgebra of E×F must include M, thus to stay functional it must equal M. ∎

Interpretation of first-order formulas

Trying to extend the formal definitions of terms interpreted in algebras, to formalize the general concept of formula interpreted in systems, the difficulty is to cope with the interpretation of quantifiers (or generally binders, if we wish to still generalize). A possible solution, is to treat all variables as bound throughout the formula.
Binding all variables modifies the view on the above concept of interpretation of a term T with set of variables V in an algebra E by re-currying the family (hv) of functions from T to E where v runs over EV, into a function from T to EEV. So, a first-order formula interpreted in a system E can be understood as a term interpreted in an algebra whose base set is the set OpE ∪ RelE of all operations and all relations in E where

OpE = ⋃n∈ℕ OpE(n) and RelE = ⋃n∈ℕ ℘(En).

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 ℕ for the case we would need to see "all possible formulas" as terms interpreted in one same algebra.
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. Algebras
3.3. Special morphisms
3.4. Monoids
3.5. Actions of monoids
3.6. Categories
3.7. Algebraic terms and term algebras
3.8. Integers and recursion
3.9. Arithmetic with addition
4. Model Theory