helm/software/matita/contribs/igft/cantor.ma

   1 include "logic/cprop_connectives.ma".
   2 include "igft.ma".
   3
   4 axiom A: Type.
   5 axiom S_: A → Ω^A.
   6
   7 inductive Unit : Type := unit : Unit.
   8
   9 definition axs: AxiomSet.
  10  constructor 1;
  11   [ apply A;
  12   | intro; apply Unit;
  13   | intros; apply (S_ a)]
  14 qed.
  15
  16 definition S : axs → Ω^axs ≝ S_.
  17
  18 definition emptyset: Ω^axs ≝ {x | False}.
  19
  20 notation "∅︀" non associative with precedence 90 for @{'emptyset}.
  21 interpretation "emptyset" 'emptyset = emptyset.
  22 notation "∅" non associative with precedence 91 for @{'emptyset1}.
  23 interpretation "emptyset1" 'emptyset1 = emptyset.
  24
  25 definition Z: Ω \sup axs ≝ {x | x ⊲ ∅}.
  26
  27 theorem cantor: ∀a:axs. ¬ (Z ⊆ S a ∧ S a ⊆ Z).
  28  intros 2; cases H; clear H;
  29  cut (a ⊲ S a);
  30   [2: apply infinity; [apply unit] change with (S a ⊲ S a);
  31       intros 2; apply refl; apply H;]
  32  cut (a ⊲ ∅︀);
  33   [2: apply (trans (S a)); [ assumption ]
  34       intros 2; lapply (H2 ? H) as K;
  35       change in K with (x ⊲ ∅ );
  36       assumption;]
  37  cut (a ε S a);
  38   [2: apply H1; apply Hcut1;]
  39  generalize in match Hcut2; clear Hcut2;
  40  elim Hcut1 using covers_elim;
  41   [ intros 2; cases H;
  42   | intros; apply (H3 a1); [apply H4|apply H4]]
  43 qed.