INDUCTION AND RECURSION

Theorem S.I.1 - Induction Principle
If (X,E) is a well ordered set, YcX and
/\(x:-X) (/\(y:-X) yEx and y!=x => y:-Y) => x:-Y
then X = Y.

Proof
Let D = X\Y.
Assume to the contrary that D != O.
Since (X,E) is a well ordered set, 
there exist t:-D such that /\(d:-D) tEd.
Take any y:-X such that yEt and t!=y.
It is obvious that !(y:-D). Thus y:-Y.
By assumptions of this theorem we have t:-Y.
Contradiction.
We have shown that Y = X.

Theorem S.I.2 - Recursion Principle
If (X,E) is a well ordered set, Y is a set,
I:X->P(X) such that I(x) = {y:-X|yEx and y!=x},
D = { j:-P(XxY) | \/(x:-X) j:I(x)->Y },
and g:D->Y
then there is a unique function f:X->Y such that
/\(x:-X) f(x) = g(f|I(x)).

Remark: Notice that if m:-X is the least element
then f(m) = g(O).

Proof of Theorem S.I.2
If X = O there is no problem.
Assume that X != O.

We will write that
(A,f) is a proper collection if and only if
A is an initial segment of X
and f:A->Y such that
/\(x:-A) f(x) = g(f|I(x)).

We will show that:
If (A,f) and (A,g) are proper collections
then f = g.

Let T = {x:-A|f(x) = h(x)}.
By the Induction Principle restricted to A.
we get T = A. Thus f = h.

We will show that:
If (A,f) and (B,h) are proper collections and AcB
then f c h.

It is obvious that (A,h|A) is a proper collection. 
Thus h|A = f. So f c h.

Let J(z) = {x:-X|xEz}. 
It is easy to show that J(z) is an initial segment of X.
Let H = {z:-X | \/(f) (J(z),f) is a proper collection}.

We want to use the Induction Principle to show that H = X.

Take any x:-X.
Assume that (/\(y:-X) yEx and y!=x => y:-H).
We want to show that x:-H.
Let L = {f:-P(XxY):\/(z:-I(x)) (J(z),f) is a proper collection}.
It is easy to show that 
/\(a,b:-X) (J(a) c J(b) or J(a) c J(b)).
Thus u(L) is a function by Theorem S.C.14.
Let h:J(x)->Y such that /\(q:-I(x)) h(q) = u(L)(q)
and h(x) = g(u(L)|I(x)).
Thus (J(x),h) is a proper collection.
So x:-H.
By the Induction Principle H = X.

Let K = {h:-P(XxY)|\/(z:-H) (J(z),h) is a proper collection}.
Let f = u(K).
We will show that. 
(1) f:X->Y,
(2) /\(x:-X) f(x) = g(f|I(x)).

(1)
f is a function by Theorem S.C.14.
f:X->Y because H = X.

(2)
Take any x:-X.
Since x:-H we have h:J(x)->Y 
such that (J(x),h) is a proper collection.
It is obvious that h c f.
Thus f(x) = g(f|I(x)).
We have shown (2).

f is unique because 
if (X,f) (X,f1) are proper collections
then f = f1.