More recursion tools

4.8. More recursion tools

Rebuilding recursion

Let us work in a first-order 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², ∀n∈ℕ, (∀i<n, ∀x∈E, ∃y∈E, R(i,x,y)) ⇒ ∀a∈E, ∃u∈H, u₀=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₀=a ∧ ∀n∈ℕ, x_n+1 = f(n,x_n), can be defined by its graph

{(n,u_n) | (n,u)∈ℕ×H, u₀=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 L-algebras E, F, ∀f∈F^E, f ∈ Mor_L(E,F) ⇔ Gr f ∈ Sub_L(E×F).

Proof: ∀s∈L,

(∀x∈E^n_s, f(s_E(x)) = s_F(f⚬x))	⇔ ∀x∈E^n_s, ∀y∈F^n_s, (y = f⚬x ⇒ f(s_E(x)) = s_F(y))
	⇔ ∀(x⊓y)∈(Gr f)^n_s, (s_E(x), s_F(y)) ∈ Gr f
	⇔ ∀z∈(Gr f)^n_s, s_E×F(z) ∈ Gr f ∎

Other proof from previous results:

_{0|Gr f}

^-1

Hence another proof of the stability of equalizers:

₀

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 L-algebra and F is an injective L-system then ∀f ∈Mor_L(E,F),

A = {x∈E | ∀y∈E, f(x) = f(y) ⇒ x=y} ∈ Sub_LE.
B = {y∈F | !: f^•(y)} ∈ Sub_LF
Thus if more precisely E, F are algebras, {y∈F | ∃!: f^•(y)} ∈ Sub_LF.

While they are almost the same, let us write separate proofs.
The condition f ∈Mor_L(E,F) is read Im f ⊂ Dom ψ_F ∧ ^Lf_{|Dom φ_E} = ψ_F⚬f⚬φ_E.

∀x∈^LA⋂Dom φ_E, ∀y∈E, ∃z∈φ_E^•(y),
f(φ_E(x)) = f(y) ⇒ ^Lf(x) = ψ_F(f(φ_E(x))) = ψ_F(f(y)) = ψ_F(f(φ_E(z))) = ^Lf(z)
⇒ x = z ⇒ φ_E(x) = y.
∀y∈F_*(^LB), ψ_F(y) ∈ ^LB ∴ (!z∈Dom φ_E, ψ_F(y) = ^Lf(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 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: 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^n_s×F^n_s ≡ ∐_s∈L (E×F)^n_s = 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(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 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 Id_E⊓u because π⚬f ∈ Mor(E, E) ∴ π⚬f = Id_E.

But one can do without it, based on the following property of this L-algebra 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 L-algebra 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 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