Library hilbert.Paradoxical
Set Implicit Arguments.
Require Import Ensembles.
Definition compose (S T U:Type)(g : T -> U)(f:S ->T)x := g (f x).
Definition star (S T:Type)(f:S->T) : Ensemble S -> Ensemble T :=
fun X => (fun y => exists x:S, X x /\ y=f x).
Lemma star_com : forall (S T U : Type) (f : S -> Ensemble T)
(g : Ensemble T -> U)
(X: Ensemble S),
star (compose g f) X =
compose (star g) (star f) X.
Proof.
unfold compose, star.
intros.
apply Extensionality_Ensembles.
split.
red.
red.
intros.
red in H.
case H;intros.
exists (f x0).
split;auto.
exists x0;auto.
case H0;auto.
case H0;auto.
red.
intros.
case H.
intros.
red.
case H0.
intros.
case H1;intros y (Hy,Hy').
exists y;split;auto.
subst x0;auto.
Qed.
Definition Paradoxical
(U:Type)
(sigma : U -> Ensemble U)
(tau : Ensemble U -> U) :=
forall X, sigma (tau X) =
star (compose tau sigma) X.
Section decouverte.
Variables
(U:Type)
(sigma : U -> Ensemble U)
(tau : Ensemble U -> U)
(Hp : Paradoxical sigma tau).
Definition lt y x := In _ (sigma x) y.
Notation "x < y" :=(lt x y):para_scope.
Open Scope para_scope.
Lemma paraphrase : forall x, sigma x = (fun y => y < x).
Proof.
intro;apply Extensionality_Ensembles.
split; unfold lt;repeat red;auto.
Qed.
Lemma L2 : forall x z, z < tau(sigma x) -> exists y, y < x /\ z=tau(sigma y).
Proof.
intros.
do 2 red in H.
generalize (Hp (sigma x)).
intro.
rewrite H0 in H.
info auto.
Qed.
Lemma L2' : forall x y, y < x -> tau(sigma y) < tau(sigma x).
Proof.
intros.
generalize (Hp (sigma x)).
intro.
clear Hp.
red.
red.
rewrite H0.
red.
exists y;auto.
Qed.
Definition inductive (X:Ensemble U) :=
forall x, (forall y, y < x -> X y) -> X x.
Definition well_founded x := forall X, inductive X -> X x.
Definition Omega := tau (fun x => well_founded x).
Lemma L4 : forall y, y < Omega -> exists w, well_founded w /\
y = tau(sigma w).
Proof.
unfold Omega, lt.
unfold In.
generalize (Hp (fun x : U => well_founded x)).
intro.
rewrite H.
auto.
Qed.
Lemma L5 : forall w, well_founded w -> tau(sigma w) < Omega.
Proof.
unfold Omega, lt.
unfold In.
generalize (Hp (fun x : U => well_founded x)).
intro.
rewrite H.
intros;exists w;auto.
Qed.
Section Omega_wf.
Variable X: Ensemble U.
Hypothesis ind_X : inductive X.
Remark R1 : forall y, y < Omega -> X y.
intros.
case (L4 H).
intros w (Ww,eqw).
subst y.
clear H.
unfold well_founded in Ww.
assert (inductive (fun y => X (tau (sigma y)))).
red.
intros.
red in ind_X.
apply ind_X.
intros.
case (L2 H0).
intros.
decompose [and] H1.
clear H1.
subst y.
apply H.
auto.
apply Ww.
auto.
Qed.
Lemma R2 : X Omega.
Proof.
red in ind_X.
apply ind_X.
exact R1.
Qed.
End Omega_wf.
Theorem Omega_well_founded : well_founded Omega.
Proof.
red.
exact R2.
Qed.
Section the_contrtadiction.
Hypothesis Omega_wf : well_founded Omega.
Lemma L55 : tau (sigma Omega) < Omega.
Proof.
apply L5.
auto.
Qed.
Lemma induc : inductive (fun y => not (tau (sigma y) < y)).
Proof.
red.
intros x Hx.
red;intro H'.
absurd (tau(sigma(tau(sigma x))) < tau(sigma x)).
apply Hx.
auto.
apply L2'.
auto.
Qed.
Lemma L66 : not (tau (sigma Omega) < Omega).
Proof.
pattern Omega.
apply Omega_wf.
apply induc.
Qed.
Lemma Omega_not_well_founded : False.
Proof.
case L66.
apply L55.
Qed.
End the_contrtadiction.
Theorem paradox : False.
Proof.
case Omega_not_well_founded.
apply Omega_well_founded.
Qed.
End decouverte.