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'].