4.8. More recursion tools
Rebuilding recursion
Let us work in a firstorder theory just assumed to have 3 types ℕ, E and
H⊂E^{ℕ},
the language and axioms of arithmetic for ℕ with the schema of induction over expressible
subsets of ℕ, and the axiom that H provides "all finite sequences"
∀n∈ℕ, ∀u∈H, ∀y∈E, ∃v∈H,
v_{n}=y ∧ ∀k<n, v_{k} =
u_{k}
The following existential result has a simple proof by induction making no use of uniqueness:
∀R⊂ℕ×E^{2}, ∀n∈ℕ,
(∀i<n, ∀x∈E, ∃y∈E, R(i,x,y))
⇒ ∀a∈E,
∃u∈H, u_{0}=a ∧ ∀i<n,
R(i,u_{i},u_{i+1}).
Its simplicity only goes for this case, only generalizable to conditions of the form
R(n,(u_{k})_{k<n},u_{n}), while the case of algebraic terms is also true but more difficult to prove.
As a particular case, comes the finite choice theorem written as
∀R⊂ℕ×E, ∀n∈ℕ,
(∀i<n, ∃y∈E, R(i,y))
⇒ ∃u∈H, ∀i<n,
R(i,u_{i}).
With f∈E^{ℕ×E} the restriction of such u to
numbers ≤ n is also unique by
induction, from which the x∈E^{ℕ} such that
x_{0}=a ∧ ∀n∈ℕ, x_{n+1} =
f(n,x_{n}), can be defined by its graph
{(n,u_{n})  (n,u)∈ℕ×H,
u_{0}=a ∧ ∀i<n,
u_{i+1} = f(i,u_{i})}
As H contains any finite sequence expressible in the theory, this definition
of recursion turns out to be "the recursion which the theory can express"
independently of the particular choice of H.
The construction of ℕ^{(ℕ)} from the last section, 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 an independent expression of an enumerated
H, which is harder but finally possible. Such a construction was achieved by Godel
as part of his work to prove the incompleteness theorem.
Morphisms as subalgebras
For any Lalgebras E, F,
∀f∈F^{E}, f ∈ Mor_{L}(E,F)
⇔ Gr f ∈ Sub_{L}(E×F).
Proof: ∀s∈L,
(∀x∈E^{ns},
f(s_{E}(x)) = s_{F}(f⚬x))

⇔ ∀x∈E^{ns},
∀y∈F^{ns}, (y = f⚬x ⇒
f(s_{E}(x)) = s_{F}(y)) 

⇔ ∀(x⊓y)∈(Gr f)^{ns},
(s_{E}(x), s_{F}(y)) ∈ Gr f 

⇔ ∀z∈(Gr f)^{ns},
s_{E×F}(z) ∈ Gr f ∎ 
Other proof from previous results:
f ∈ Mor_{L}(E,F)
⇔ Id_{E}⊓f ∈ Mor_{L}(E,E×F)
⇒ Gr f = Im(Id_{E}×f ) ∈ Sub_{L}(E×F).
Gr f ∈ Sub_{L}(E×F)
⇒ π_{0Gr f} ∈ Mor_{L}(Gr f, E)
⇒ Id_{E}⊓f = (π_{0Gr f})^{1} ∈ Mor_{L}(E, Gr f)
⊂ Mor_{L}(E, E×F).∎
Hence another proof of the stability
of equalizers:
∀f,g∈Mor_{L}(E,F),
(Gr f ⋂ Gr g) ∈ Sub_{L} (E×F)
∴ {x∈E f(x) = g(x)} = π_{0}
[Gr f ⋂ Gr g] ∈ Sub_{L} E.
Another proof of recursion
By seeing morphisms as subalgebras, we can write another
construction of recursive sequences u∈Mor_{(0,S)}(ℕ,(E,a,f)),
as follows.
Let M be the minimal subalgebra of ℕ×E_{a,f},
and let A={n∈ℕ  ∃!x∈E, (n,x)∈M}.
As M is a minimal (0,S)algebra, M = {(0,a)}∪
Im S_{M}.
Substituting this into the definition of A we get
∀p∈ℕ, p∈A ⇔ (∃!y∈E,
(p=0 ∧ y=a)∨∃(n,x)∈M,
(p=Sn ∧ y=f(x))).
From 0 ∉ Im S we get 0∈A, and
∀n∈ℕ, Sn∈A ⇔ ∃!y∈E,
∃(n',x)∈M, (Sn=Sn' ∧ y=f(x)).
From the injectivity of S we get
∀n∈ℕ, Sn∈A ⇔ ∃!y∈E,
∃x∈E, (n,x)∈M∧ y=f(x).
Thus (∀n∈A, Sn∈A), so that A
= ℕ, i.e. M is the graph of a function u ∈ E^{ℕ}.
As M ∈ Sub(ℕ×E_{a,f}), we
conclude u ∈ Mor_{(0,S)}(ℕ,E_{a,f}).
Injectivity lemma
If E is a surjective partial Lalgebra and
F is an injective Lsystem then ∀f ∈Mor_{L}(E,F),
 A = {x∈E  ∀y∈E, f(x) =
f(y) ⇒ x=y}
∈ Sub_{L}E.
 B = {y∈F  !: f^{ •}(y)} ∈ Sub_{L}F
Thus if more precisely E, F are algebras,
{y∈F  ∃!: f^{ •}(y)} ∈ Sub_{L}F.
While they are almost the same, let us write separate proofs.
The condition
f ∈Mor_{L}(E,F) is read Im f ⊂
Dom ψ_{F} ∧
^{L}f_{Dom φE} =
ψ_{F}⚬f⚬φ_{E}.
 ∀x∈^{L}A⋂Dom φ_{E},
∀y∈E, ∃z∈φ_{E}^{•}(y),
f(φ_{E}(x)) = f(y) ⇒ ^{L}f(x)
= ψ_{F}(f(φ_{E}(x))) = ψ_{F}(f(y))
= ψ_{F}(f(φ_{E}(z))) = ^{L}f(z)
⇒ x = z ⇒ φ_{E}(x) = y.
 ∀y∈F_{*}(^{L}B),
ψ_{F}(y) ∈ ^{L}B ∴ (!z∈Dom
φ_{E}, ψ_{F}(y) = ^{L}f(z)
= ψ_{F}(f(φ_{E}(z))))
∴
!x∈Im φ_{E}=E, y = f(x).∎
A more general form of recursion
Some useful sequences need recursive definitions where the term defining
u_{Sn} uses not only u_{n} 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 : E → F, where, instead of a draft, E is first
assumed to be an Lalgebra (then a ground term algebra to conclude).
The version we saw was formalized by giving the term in the recursive definition as an
Lalgebra structure on F, φ_{F}: L⋆F → F,
then expressing the request for u to satisfy this condition as u∈Mor(E,F),
namely ∀(s,x)∈L⋆E,
u(s_{E}(x)) = φ_{F}(s,u⚬x).
Let us generalize this as u(s_{E}(x))
= φ(s,x,u⚬x) which by the canonical bijection
Dom φ ≡ ∐_{s∈L} E^{ns
}×F^{ns} ≡ ∐_{s∈L}
(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), asu(s_{E}(x))
= h(s,x⊓(u⚬x)).
As ∀u∈F^{E}, x⊓(u⚬x)
= (Id_{E}⊓u)⚬x, this becomes
the second component of the formula Id_{E}⊓u ∈ Mor(E, E×F)
when giving E×F the structure φ_{E×F} =
(φ_{E}⚬π_{L})⊓h.
The first component (φ_{E}⚬π_{L}) we give to
φ_{E×F},
makes π∈ Mor(E×F, E) and makes tautological the first component
of the formula Id_{E}⊓u
∈ Mor(E, E×F), namely
Id_{E}(s_{E}(x)) = φ_{E}(s,x)
= (φ_{E}⚬π_{L})(s,x⊓(u⚬x)).
It is then possible to conclude by reusing the previous result of existence of interpretations:
If E is a closed term Lalgebra then
∃!f ∈ Mor(E, E×F), which is
of the form Id_{E}⊓u because
π⚬f ∈ Mor(E, E) ∴ π⚬f = Id_{E}.
But one can do without it, based on the following property of this Lalgebra E×F:
∀u∈F^{E}, Id_{E}⊓u
∈ Mor_{L}(E, E×F) ⇔ Gr u
∈ Sub_{L}(E×F)
Indeed the defining formulas of both sides coincide. To see it otherwise,
 ⇒ is a case of image of an algebra by a
morphism, Gr u = Im (Id_{E}⊓u).

For the converse, the inverse of the bijective morphism π_{Gr u}
∈ Mor_{L}(Gr u, E)
is a morphism Id_{E}⊓u ∈ Mor_{L}(E, Gr u)
⊂ Mor_{L}(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 Lalgebra then M =
Min_{L}(E×F) is one of them because
π_{M}∈ Mor_{L}(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. ∎
Set theory and foundations
of mathematics
1. First foundations of
mathematics
2. Set theory (continued)
3. Algebra 1
4. Arithmetic and firstorder foundations
5. Secondorder foundations
6. Foundations of Geometry