Browse the main library: A B C D E F G or go to appendix or return to overview.

# Library e_recursion

initial import of the development

Require Export d_isomorphy.

## Bounded Transfinite Induction

Lemma worder_ind M R (P: set -> Prop): wordering R M
-> (forall x, x <e M -> (forall y, y <e (iseg M R x) -> P y) -> P x)
-> forall x, x <e M -> P x.

Lemma trans_ind_b a (P: set -> Prop): ordinal a
-> (forall b, b <e a -> (forall c, c <e b -> P c) -> P b)
-> forall b, b <e a -> P b.

## Unbounded Transfinite Induction

Lemma ordinal_wf (P: set -> Prop): ~(forall a, ordinal a -> P a)
-> exists a, ordinal a /\ ~ P a /\ forall b, b <e a -> P b.

Theorem trans_ind (P: set -> Prop):
(forall a, ordinal a -> (forall b, b <e a -> P b) -> P a)
-> forall a, ordinal a -> P a.

## Examples

Lemma iseg_oisoeq M R x x': wordering R M -> x <e M -> x' <e M
-> oiso (iseg M R x) (iseg M R x') R R -> (iseg M R x) = (iseg M R x').
Lemma ordinal_ordiso a b: ordinal a -> ordinal b ->
oiso a b (elorder a) (elorder b) -> a = b.

Corollary ordiso_eq a b M R: ordiso M a R -> ordiso M b R -> a = b.

Corollary ordinal_iso M R: (exists a, ordiso M a R) -> (exists! a, ordiso M a R).

## Unbounded Transfinite Recursion

Section TransRec.
Variable G: set -> set.

We first define the notion of a computation.

Definition compB t a B :=
function t (succ a) B /\ forall b, b <e (succ a) -> t[b] = G (t|b).

Definition comp t a :=
exists B, compB t a B.

Lemma comp_res x y t: ordinal x -> comp t x -> y <e x -> comp (t|(succ y)) y.

Lemma comp_eq t1 t2 x: ordinal x -> comp t1 x -> comp t2 x -> t1 = t2.

Lemma comp_unique t x: ordinal x -> comp t x -> exists! u, comp u x.

Lemma comp_subs t1 x1 t2 x2: ordinal x1 -> x2 <e x1 -> comp t1 x1 -> comp t2 x2 ->
t2 c= t1.

Lemma comp_linear t1 x1 t2 x2: ordinal x1 -> ordinal x2 -> comp t1 x1 -> comp t2 x2 ->
t1 c= t2 \/ t2 c= t1.

Lemma comp_res_eq x y t u: ordinal x -> y <e x -> comp t x -> comp u y ->
t|(succ y) = u.

Lemma comp_agree x y z t u i1 i2: ordinal x -> ordinal y -> comp t x -> comp u y ->
(z,i1) <e t -> (z,i2) <e u -> i1=i2.

Step 1: we define tao x, which will serve as the unique computation of length x.

Definition t x := desc (fun t => comp t x).
Definition T x := replacement x t.
Definition TU x := union (T x).
Definition tao x := bunion (TU x) (singleton (x, G (TU x))).

Definition R1 x := replacement (TU x) pi2.
Definition R2 x := bunion (R1 x) (singleton (G (TU x))).

We begin with some simple statements.

Lemma T_el x b u: b <e x -> unique (fun t : set => comp t b) u -> u <e T x.

Lemma tao_T x t: t <e T x -> t c= tao x.

Lemma u_t x u: ordinal x -> comp u x -> u = t x.

Lemma TU_el t x y B a: (exists! t, comp t y) -> compB t y B ->
y <e x -> a <e succ y -> (a,t[a]) <e TU x.

Lemma R1_el t x y B a: (exists! t, comp t y) -> compB t y B ->
y <e x -> a <e succ y -> t[a] <e R1 x.

Lemma R1_subs t x y B: (exists! t, comp t y) ->
y <e x -> compB t y B -> compB t y (R1 x).

Lemma R2_subs t x y B: (exists! t : set, comp t y) ->
y <e x -> compB t y B -> compB t y (R2 x).

Now we prepare the inductive step, meaning we assume all shorter computations to exist, then we prove that TU is a function and tao a computation.

Lemma TU_rel x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
relation (TU x) x (R1 x).

Lemma TU_total x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
total (TU x) x (R1 x).

Lemma TU_functional x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
functional (TU x).

Lemma TU_fun1 x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
function (TU x) x (R1 x).

Lemma TU_fun2 x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
function (TU x) x (R2 x).

Lemma tao_fun x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
function (tao x) (succ x) (R2 x).

Lemma tao_x x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
(tao x) [x] = G (TU x).

Lemma tao_TU x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
(tao x)|x = TU x.

Lemma tao_compB_step x: (forall y, y <e x -> exists! t, comp t y) -> ordinal x ->
compB (tao x) x (R2 x).

Step 2: tao is a unique computation. We apply transfinite induction.

Lemma tao_compB x: ordinal x -> compB (tao x) x (R2 x).

Lemma tao_comp x: ordinal x -> comp (tao x) x.

Lemma tao_unique x sigma: ordinal x -> comp sigma x -> sigma = (tao x).

Lemma comp_exists x: ordinal x -> exists! t, comp t x.

Lemma tao_t x: ordinal x -> t x = tao x.

Lemma TU_fun x: ordinal x -> function (TU x) x (R1 x).

Lemma tao_app x: ordinal x -> (tao x) [x] = G (TU x).

Lemma tao_eq x y: ordinal x -> y <e x -> (tao x)|x [y] = (tao y) [y].

Lemma tao_res x: ordinal x -> function (tao x)|x x (R1 x).

Step 3: we define the recursive function F and prove it to satisfy the Unbounded Transfinite Recursion Theorem.

Definition F x := tao x [x].

Lemma F_fun a: ordinal a -> function (lam F a) a (R1 a).

Lemma F_eq2 a: ordinal a -> (tao a)|a = (lam F a).

Theorem trans_rec: forall a, ordinal a -> F a = G (lam F a).

End TransRec.

## Bounded Transfinite Recursion

Definition fset a' B := specification (power (product a' B)) (fun f => function f a' B).
Definition space a B := union (replacement a (fun a' => fset a' B)).

Section TransRecB.
Variable a: set.
Variable B: set.
Variable g: set.

Variable AO: ordinal a.
Variable GF: function g (space a B) B.

Definition G := app g.
Definition f := lam (F G) a.

Lemma B_tao_app1 b c: ordinal b -> c <e b -> function (tao G c) (succ c) B ->
(tao G b)[c] <e B.

Lemma B_tao_TU b: b <e a -> (forall c, c <e b -> function (tao G c) (succ c) B) ->
TU G b <e fset b B.

Lemma B_tao_app2 b: b <e a -> (forall c, c <e b -> function (tao G c) (succ c) B) ->
(tao G b)[b] <e B.

Lemma B_tao: forall b, b <e a -> function (tao G b) (succ b) B.

Lemma f_fun: function f a (R1 G a).

Lemma f_funB: function f a B.

Lemma f_rec: forall a', a' <e a -> f[a'] = g[f|a'].

Lemma f_unique f': function f' a B /\
(forall a', a' <e a -> f'[a'] = g[f'|a']) -> f = f'.

End TransRecB.

Theorem trans_rec_b a B g: ordinal a -> function g (space a B) B ->
exists! f, function f a B /\ forall a', a' <e a -> f[a'] = g[f|a'].