Library hydras.Schutte.Critical
- Cr(zero) = AP (the set of additive principal ordinals )
- if zero < alpha, then Cr(alpha) is the intersection of all the sets of fixpoints of the ordering functions of Cr(beta) for beta < alpha.
From Coq Require Import Arith Logic.Epsilon Ensembles Classical.
From ZornsLemma Require Import CountableTypes.
From hydras Require Export Schutte_basics Ordering_Functions
Countable Schutte.Addition AP CNF Well_Orders MoreEpsilonIota.
Set Implicit Arguments.
Let us define a functional, the fixpoint of which we shall consider
Definition Cr_fun : ∀ alpha : Ord,
(∀ beta : Ord, beta < alpha → Ensemble Ord) →
Ensemble Ord
:=
fun (alpha: Ord)
(Cr : ∀ beta, beta < alpha → Ensemble Ord)
(x : Ord) ⇒ (
(alpha = zero ∧ AP x) ∨
(zero < alpha ∧
∀ beta (H:beta < alpha),
In (the_ordering_segment (Cr beta H)) x ∧
ord (Cr beta H) x = x)).
Definition Cr (alpha : Ord) : Ensemble Ord :=
(Fix all_ord_acc
(fun (_:Ord) ⇒ Ensemble Ord) Cr_fun) alpha.
Definition strongly_critical alpha := In (Cr alpha) alpha.
Definition maximal_critical alpha : Ensemble Ord :=
fun gamma ⇒
In (Cr alpha) gamma ∧
∀ xi, alpha < xi → ¬ In (Cr xi) gamma.
Definition Gamma0 := the_least strongly_critical.
See Gamma0.Gamma0.phi
Definition phi (alpha : Ord) : Ord → Ord := ord (Cr alpha).
Definition A_ (alpha : Ord) : Ensemble Ord := the_ordering_segment (Cr alpha).
Lemma Cr_extensional :
∀ (x:Ord)
(f g : ∀ y : Ord, y < x → (fun _ : Ord ⇒ Ensemble Ord) y),
(∀ (y : Ord) (p : y < x), f y p = g y p) →
((Cr_fun f :Ensemble Ord) = (Cr_fun g :Ensemble Ord)).
Lemma Cr_equation (alpha : Ord) :
Cr alpha =
Cr_fun
(fun (y : Ord) (h : y < alpha) ⇒ Cr y).
Lemma Cr_inv (alpha x : Ord):
Cr alpha x →
((alpha = zero ∧ (Cr alpha x ↔ AP x)) ∨
(zero < alpha ∧
(∀ beta (H:beta < alpha),
A_ beta x ∧ ord (Cr beta ) x = x))).
Lemma Cr_zero : ∀ x, AP x → Cr zero x.
Lemma Cr_pos : ∀ alpha,
zero < alpha →
∀ x : Ord ,
(∀ beta (H:beta < alpha),
A_ beta x ∧ ord (Cr beta) x = x) →
Cr alpha x.
Lemma Cr_zero_inv : ∀ x, Cr zero x → AP x.
Lemma Cr_zero_AP : Cr zero = AP.
Lemma Cr_pos_inv (alpha : Ord) :
zero < alpha →
∀ x,
Cr alpha x →
(∀ beta (H:beta < alpha), In (A_ beta) x ∧ phi beta x = x).
Lemma Cr_pos_iff (alpha : Ord) :
zero < alpha →
∀ x,
(Cr alpha x ↔
(∀ beta (H:beta < alpha), In (A_ beta) x ∧ phi beta x = x)).
Lemma A_Cr (alpha beta:Ord) : In (A_ alpha) beta → phi alpha beta = beta →
In (Cr alpha) beta.
Lemma Cr_lt : ∀ alpha beta,
beta < alpha → ∀ x, Cr alpha x → Cr beta x.
Lemma Cr_incl (alpha beta : Ord) (H :beta ≤ alpha) :
Included (Cr alpha) (Cr beta).
Lemma phi0_well_named : ∀ alpha, phi0 alpha = phi 0 alpha.
Lemma Cr_1_iff (alpha : Ord):
Cr 1 alpha ↔ AP alpha ∧ phi0 alpha = alpha.
Lemma epsilon0_Cr1 : In (Cr 1) epsilon0.
Lemma 5, p 82 of Schutte's book
Section Proof_of_Lemma5.
Let P (alpha:Ord) := Unbounded (Cr alpha) ∧ Closed (Cr alpha).
Lemma Lemma5_0 : P zero.
Section Alpha_positive.
Variable alpha : Ord.
Hypothesis alpha_pos : zero < alpha.
Hypothesis IHalpha : ∀ xi, xi < alpha → P xi.
Section Proof_unbounded.
Variable beta : Ord.
Fixpoint gamma_ (n:nat) : Ord :=
match n with
O ⇒ succ beta
| S n ⇒ sup
(fun (y : Ord) ⇒
∃ xi: Ord, xi < alpha ∧
y = phi xi (gamma_ n))
end.
Let gamma := omega_limit gamma_.
Lemma Lemma5_01 : beta < gamma.
Lemma Lemma5_02 : ∀ xi, xi < alpha →
phi xi gamma = gamma.
Lemma Lemma5_03 : In (Cr alpha) gamma.
Remark A_full : ∀ xi, xi < alpha → A_ xi = ordinal.
Lemma Lemma5_04 : ∃ gamma, In (Cr alpha) gamma ∧ beta < gamma.
End Proof_unbounded.
Lemma Lemma5_1 : Unbounded (Cr alpha).
Section closedness.
Variable M : Ensemble Ord.
Hypothesis HM : Inhabited M.
Hypothesis CM : Countable M.
Hypothesis IM : Included M (Cr alpha).
Lemma Lemma5_2 : ∀ xi eta, xi < alpha →
In M eta →
phi xi eta = eta.
Check (Cr_pos_iff alpha_pos).
Qed.
Lemma Lemma5_7 : In (Cr alpha) (sup M).
End closedness.
Lemma induct_step : P alpha.
End Alpha_positive.
Lemma Lemma5 : ∀ alpha, P alpha.
End Proof_of_Lemma5.
Theorem Unbounded_Cr alpha : Unbounded (Cr alpha).
Theorem Closed_Cr alpha : Closed (Cr alpha).
Theorem Th13_8 alpha : normal (phi alpha) (Cr alpha).
Corollary Th13_8_1 alpha : A_ alpha = ordinal.