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.