More recursion tools

4.8. More recursion tools

We first defined recursion as a particular case of the interpretation of a draft in an algebra, whose proof of existence was a little hard (its use of the conditional operator may be removed by adding the proper justifications). Here we shall review diverse variants of this construction, which can be useful in diverse contexts.

Well-founded recursion

Let R ⊂ X² be a well-founded relation, and denote its reverse curried form R⃖(x) as [x], so that ∀x,y∈X, xRy ⇔ x∈[y].
As first seen for drafts where [x] = Im l_x, the well-foundedness of R can be equivalently written

∀A⊂X, (∀x∈X, [x] ⊂ A ⇒ x ∈ A) ⇒ A = X
∀A⊂X, A ≠ X ⇒ ∃x∈X\A, [x] ⊂ A
∀A⊂X, A≠∅ ⇒ ∃x∈A, A∩[x] = ∅

Then, for any set E and any Φ : ∐_x∈X E^[x] → E, there exists a unique h : X→E such that

∀x∈X, h(x) = Φ(x,h_|[x]).

The interpretation of a ground draft (X, ^tGr ψ_X) in an algebra E, was the particular case of Φ defined as

∀x∈X, ∀u∈E^[x], Φ(x,u) = σ(x)_E(u০l_x) = φ_E(^Lu(ψ_X(x)))

The same proof works in the general case, after a simple re-writing left as an exercise for the reader.

Graphs of morphisms

A different generalization will be inspired from the fact the wanted morphism was defined by its graph.

Let L an algebraic language, E, F two L-systems, G = E×F the product system, f : E → F and H = Gr f ⊂ G. Then

(E injective ∧ H ⊂ G^⋆(^LH)) ⇒ f ∈ Mor_L(E,F)
(E surjective ∧ f ∈ Mor_L(E,F)) ⇒ H ⊂ G^⋆(^LH)
(F serial ∧ G^⋆(^LH) ⊂ H)) ⇒ f ∈ Mor_L(E,F)
(F functional ∧ f ∈ Mor_L(E,F)) ⇒ G^⋆(^LH) ⊂ H

The proofs are easy and left as exercises to the reader. The last formula provides another proof of the stability of equalizers:

₀

The last two together give : if F is an L-algebra then ∀f∈F^E, f ∈ Mor_L(E,F) ⇔ Gr f ∈ Sub_L(E×F).
This can also be deduced from previous results when both E,F are L-algebras and thus G too:

_{0|Gr f}

^-1

Now the search for morphisms from a system E to an algebra F, is reduced to that of subsets H∈ Sub_L(E×F) which would be graphs of functions with domain E. Hence the idea of a different view on the construction of H, as an intersection instead of a union (generalizing the proof from Halmos's Naive Set Theory): we shall prove that, when E is minimal, these conditions imply H = Min_L(E×F), and that E being a ground draft implies the converse: Min_L(E×F) is functional with domain E.

Generalized algebraic recursion

Let us modify our hypothesis to handle a more general case, very similar to the case of well-founded recursion, but still using an algebraic language (for compatibility with previous concepts).

Let L an algebraic language, and E, G two L-systems. We shall forget F and the hypothesis G = E×F, to only remember its first projection π ∈ Mor_L(G,E).
The hypothesis that F was an algebra, is re-expressed by the formula of the fullness of π modified by replacing ∃ by ∃! :

∀x∈^LG, ∀y∈E, (^Lπ(x),y) ∈ E ⇒ ∃!z∈G, π(z) = y ∧ (x,z)∈G

letting the structure G of G be expressed by a function Φ : K → G where

K = {(x,y)∈ ^LG×E | (^Lf(x),y) ∈ E}
∀(x,y)∈K, π(Φ(x,y)) = y
G = {(x, Φ(x,y)) | (x,y) ∈ K}

As π is full, π[Min_L G] = Min_L E. Thus if E is minimal then π[Min_L G] = E, so that

∀H∈ Sub_L(G), Min_L G ⊂ H ∴ (Inj π_|H ⇒ H = Min_L G)

Then, for any H ⊂ G, the following hypotheses

H is surjective (H ⊂ G^⋆(^LH))
E is injective
∀(x,y)∈K, !z∈G, π(z) = y ∧ (x,z)∈G

imply the stability of B = {y∈E | !z∈H, π(z) = y}.
Indeed ∀u∈^LB, !x∈^LH, ^Lπ(x) = u and the conclusion easily follows.
Finally since Min_L G is surjective, when E is a ground term algebra and G is expressible by Φ as above, π_{|Min_L G} is injective with image E. ∎

An easy further generalization comes by only using the second half of this proof: while keeping E a ground term algebra, the hypothesis on G is weakened to the use of ! only, fitting a Φ with domain a subset of K. Then Min_L G is the only surjective stable subset of G, and the graph of a function with domain a subset of E, called the function defined by a partial recursion, whose exact formulation will be left to the reader.

The use of the coproduct

The above construction can be dualized, once expressed in terms of categories :

Giving an f ∈ Mor_L(E,F) amounts to giving a section Id_E⊓f ∈ Mor_L(E,G) of π ∈ Mor_L(G,E), thus an embedded subobject of G.
Dually, it amounts to a retraction Id_F⊔f ∈ Mor_L(F⊔E,F) of the natural morphism j ∈ Mor_L(F,F⊔E); its description as a co-subobject consists in a congruence of F⊔E if F is functional, namely its minimal congruence when E is a ground term algebra. This was already used to define the synonymity of terms in 4.3.

Both are concretely related, since E×F ⊂ (F⊔E)², and the minimal stable subset of E×F is part of the minimal congruence of F⊔E:

Min_L(E×F) = E×F ∩ Min_L(F⊔E)² ⊂ E×F ∩ ≃_F⊔E

with equality when E is a functional draft and F is a partial algebra (while Min_L(F⊔E)² is not generally an equivalence relation when F is not injective).

The below will be revised later
Countability of the set of finite number sequences

Also the set ℕ^(ℕ) = {u∈ ℕ^ℕ | ∃k∈ ℕ, ∀n>k, u_n=0} is countable. There are different ways to see it:

A sequence of bijections h_n : ℕ↔ E_n, gives a surjection ∐_n∈ℕ E_i ≈ ℕ×ℕ → U=⋃_n∈ℕ E_n so that taking E_n=ℕⁿ we find that U=ℕ^(ℕ) is countable.
With the decomposition in prime numbers
As the binary representation maps ℕ to the set 2^(ℕ) of finite subsets of ℕ, it also maps ℕ^(ℕ) to the set 2^(ℕ×ℕ) of finite subsets of ℕ×ℕ.

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.

Covering of stable subsets by terms

For any L'-system (E,E), any X⊂E and any x∈〈X〉_L in E there exists a draft (D,D) where x∈D⊂E, D⊂E and V_D⊂X.
It makes no difference to fix V_D=X, or X=∅ by adding it as a set of constants to the language.

Proof, fixing X=∅ to simplify.
Let us show the stability of the union B of the D such that there exists a ground draft (D,D) with D⊂E.
Let (s,x,y)∈E such that Im x ⊂B. By finite choice there exists a tuple of ground drafts (D_i,D_i)_{i<n_s} such that ∀i<n_s, x_i∈D_i ∧ D_i⊂E.
Let D = ⋃_{i<n_s} D_i.
Let us check that Ψ = (D ∋ z ↦ Ψ_i(z) for the smallest i such that z∈D_i), defines a ground draft.
For any nonempty A⊂D, take the smallest i such that A∩D_i ≠ ∅.
∃z∈A∩D_i, ∅ = A∩D_i∩ Im l_i,z = A ∩ Im l_i,z because Im l_i,z ⊂ D_i.
Ψ(z) = Ψ_i(z) because i is also smallest such that z∈D_i, thus l_z = l_i,z.
We conclude ∃z∈A, A ∩ Im l_z = ∅, thus Ψ defines a ground draft on D.
Then either y∈D, or adding it there with (s,x,y) gives a ground draft that fits.∎

Thus independently of the axiom of infinity (existence of term algebras) anyway all elements of a minimal algebra are values of ground terms.

Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory
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
4.7. Countability and Completeness
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