4.8. More recursion tools
We first defined recursion as a particular case of the interpretation of a draft in an algebra.
Here we shall review diverse variants of this construction, which
can be useful in diverse contexts.
Another proof of interpretability of drafts in algebras
In the second way, let us still partly keep the simplification:
let V = VD by restricting u.
Uniqueness was seen with equational systems,
and will be used to prove existence :
S = {A⊂D | V⊂A ∧ Im ψA⊂
LA}
K = ⋃A∈S
{f∈MorL(A,E) |
f|V = u}
∀f,g ∈K, B = Dom f ∩ Dom g
⇒ (f|B∈K ∧
g|B∈K)
⇒ f|B = g|B
⋃f∈K Gr f = Gr h
C = Dom h = ⋃f∈K Dom f
u ∈ K ∴ V ⊂ C ∈ S ∴ h ∈ K
(C∪D⋆(LC) ∋ x↦ (x∈C ?
h(x) : φE(Lh(ψD(x)))))
∈ K
D⋆(LC) ⊂ C
C = D ∎
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 lx, 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০lx) =
φE(Lu(ψX(x)))
The same proof works in the general case, after a simple re-writing left as an exercise for the reader.
A different generalization will be inspired from the fact the wanted morphism was defined by its graph.
Now the search for morphisms from a system E to an algebra F, is reduced to that of subsets
H∈ SubL(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 =
MinL(E×F), and that E being a ground draft implies the converse:
MinL(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 π
∈ MorL(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 |
(Lπ(x),y) ∈ E}
∀(x,y)∈K, π(Φ(x,y)) = y
G = {(x, Φ(x,y)) | (x,y) ∈ K}
As π is full, π[MinL G] = MinL E.
Thus if E is minimal then π[MinL G] = E, so that
∀H∈ SubL(G), MinL G ⊂ H ∴ (Inj π|H ⇒ H = MinL 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 MinL G is surjective, when E is a ground term algebra and G is expressible by Φ as above, π|MinL 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
MinL 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 ∈ MorL(E,F) amounts to giving a section
IdE⊓f ∈ MorL(E,G) of π
∈ MorL(G,E), thus an embedded subobject of G.
- Dually, it amounts to
a retraction IdF⊔f ∈ MorL(F⊔E,F)
of the natural morphism j ∈ MorL(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)2, and
the minimal stable subset of E×F is part of the minimal congruence of F⊔E:
MinL(E×F) = E×F ∩
MinL(F⊔E)2 ⊂ E×F ∩ ≃F⊔E
with equality when E is a functional draft and F is a partial algebra
(while MinL(F⊔E)2 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, un=0} is countable.
There are different ways to see it:
- A sequence of bijections hn : ℕ↔
En, gives a surjection ∐n∈ℕ
Ei ≈ ℕ×ℕ →
U=⋃n∈ℕ En
so that taking En=ℕ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,
vn=y ∧ ∀k<n, vk =
uk
The following existential result has a simple proof by induction making no use of uniqueness:
∀R⊂ℕ×E2, ∀n∈ℕ,
(∀i<n, ∀x∈E, ∃y∈E, R(i,x,y))
⇒ ∀a∈E,
∃u∈H, u0=a ∧ ∀i<n,
R(i,ui,ui+1).
Its simplicity only goes for this case, only generalizable to conditions of the form
R(n,(uk)k<n,un), 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,ui).
With f∈Eℕ×E the restriction of such u to
numbers ≤ n is also unique by
induction, from which the x∈Eℕ such that
x0=a ∧ ∀n∈ℕ, xn+1 =
f(n,xn), can be defined by its graph
{(n,un) | (n,u)∈ℕ×H,
u0=a ∧ ∀i<n,
ui+1 = f(i,ui)}
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
VD⊂X.
It makes no difference to fix VD=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
(Di,Di)i<ns
such that ∀i<ns,
xi∈Di ∧ Di⊂E.
Let D = ⋃i<ns Di.
Let us check that Ψ = (D ∋ z ↦ Ψi(z) for the smallest
i such that z∈Di), defines a ground draft.
For any nonempty A⊂D, take the smallest i
such that A∩Di ≠ ∅.
∃z∈A∩Di,
∅ = A∩Di∩ Im li,z =
A ∩ Im li,z because
Im li,z ⊂ Di.
Ψ(z) = Ψi(z) because i
is also smallest such that z∈Di,
thus lz = li,z.
We conclude ∃z∈A, A ∩ Im lz = ∅,
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
5. Second-order foundations
6. Foundations of Geometry