Library UniMath.Paradoxes.GirardsParadox

This file provides a direct formalizatoin of Girard's paradox, as explained in Martin-Lof's 1972 "An intuitionistic theory of types". It can serve as a test as to whether the version of Coq being used is (in the most obvious way) inconsistent.

Require Import UniMath.Foundations.All.

Section girard.

Variable Flse : Type.

Definition wf (T : Type) : Type
  := ∑ lt : T → T → Type,
            (∏ x y z: T , lt x y → lt y z → lt x z ) ×
            (∏ h : (nat → T ), (∏ n : nat , lt (h (S n)) (h n)) → Flse ).

Definition wfs : Type := total2 wf.

Definition uset (w : wfs) : Type := pr1 w.
Definition uord (w : wfs) : uset w → uset w → Type := pr1 (pr2 w).
Definition trans (w : wfs) {x y z : uset w}
  : pr1 (pr2 w) x y → pr1 (pr2 w) y z → pr1 (pr2 w) x z
  := pr1 (pr2 (pr2 w)) x y z.
Definition wfp (w : wfs) :
  (λ _ : ∏ x y z : pr1 w , pr1 (pr2 w) x y → pr1 (pr2 w) y z → pr1 (pr2 w) x z ,
                   ∏ h : nat → pr1 w , (∏ n : nat , pr1 (pr2 w) (h (S n)) (h n)) → Flse) (pr1 (pr2 (pr2 w)))
  := pr2 (pr2 (pr2 w)).

Definition wfs_wf_uord (v : wfs) (w : wfs) : Type
  := ∑ f : uset v → uset w ,
           (∏ x y : uset v , (uord v) x y → (uord w) (f x) (f y)) ×
           (∑ y : uset w , ∏ (x: uset v ), (uord w) (f x) y ).

Definition ufun {v : wfs} {w : wfs} (a : wfs_wf_uord v w) : uset v → uset w := pr1 a.
Definition homo {v : wfs} {w : wfs} (a : wfs_wf_uord v w)
  : ∏ (x y : uset v ), uord v x y → uord w (pr1 a x) (pr1 a y)
  := pr1 (pr2 a).
Definition domi {v : wfs} {w : wfs} (a : wfs_wf_uord v w) : uset w := pr1 (pr2 (pr2 a)).
Definition domicom {v : wfs} {w : wfs} (a : wfs_wf_uord v w)
  : (λ y : uset w , ∏ x : uset v , uord w (pr1 a x) y) (pr1 (pr2 (pr2 a)))
  := pr2 (pr2 (pr2 a)).

Definition wfs_wf_trans : ∀ x y z : wfs, wfs_wf_uord x y → wfs_wf_uord y z → wfs_wf_uord x z.
Proof.
  intros x y z.
  intros f g.
  ∃ (fun a : uset x ⇒ (ufun g) ((ufun f) a)).
  split.
  + intros x0 y0.
    intro x0y0.
    exact (homo g _ _ (homo f _ _ x0y0)).
  + ∃ (domi g).
    intro x0.
    set (y0 := ufun f x0).
    set (ydom := domi f).
    set (co := domicom f x0).
    exact (trans z (homo g _ _ co) (domicom g (domi f))).
Defined.

Definition wfs_wf_wfp_shift (f : nat → wfs) (b : ∏ n : nat , wfs_wf_uord (f (S n)) (f n)) :
  ∏ (n : nat ), (uset (f n) → uset (f 0)).
Proof.
  intro n.
  induction n.
  intro a; exact a.
  intro x.
  exact (IHn (ufun (b n) x)).
Defined.

Definition wfs_wf_wfp_seq (f : nat → wfs) (b : ∏ n : nat , wfs_wf_uord (f (S n)) (f n)) :
  nat → uset (f 0).
Proof.
  intro n.
  exact (wfs_wf_wfp_shift f b n (domi (b n))).
Defined.

Definition wfs_wf_wfp_compshift (f : nat → wfs) (b : ∏ n : nat , wfs_wf_uord (f (S n)) (f n)) :
  ∏ (n : nat) {x y : uset (f n)},
    uord (f n) x y → uord (f 0) (wfs_wf_wfp_shift f b n x) (wfs_wf_wfp_shift f b n y).
Proof.
  intros n.
  induction n.
  intros x y p.
  exact p.
  intros x y p.
  exact (IHn _ _ (homo (b n) x y p)).
Qed.

Lemma wfs_wf_wfp_desc (f : nat → wfs) (b : ∀ n : nat, wfs_wf_uord (f (S n)) (f n)) :
  ∏ n : nat , uord (f 0) (wfs_wf_wfp_seq f b (S n)) (wfs_wf_wfp_seq f b n).
Proof.
  intro n.
  exact (wfs_wf_wfp_compshift f b n (domicom (b n) (domi (b (S n))))).
Defined.

Definition wfs_wf : wf wfs.
Proof.
  ∃ wfs_wf_uord.
  split.
  exact wfs_wf_trans.
  intro h.
  intro b.
  exact (wfp _ (wfs_wf_wfp_seq h b) (wfs_wf_wfp_desc h b)).
Defined.

Definition wfs_wf_t : wfs := tpair (fun T ⇒ wf T) wfs (wfs_wf).

Definition maxi_fun (w : wfs) : uset w → wfs.
Proof.
  intro x.
  ∃ (∑ y : uset w, uord w y x).
  ∃ (fun a b ⇒ uord w (pr1 a) (pr1 b)).
  split.
  - intros x0 y z p q.
    exact (trans w p q).
  - intro h.
    intro b.
    exact (wfp w (fun n ⇒ pr1 (h n)) b).
Defined.

Lemma maxi_homo (w : wfs) : ∏ (x y : uset w ),
    uord w x y → wfs_wf_uord (maxi_fun w x) (maxi_fun w y).
Proof.
  intros x y p.
  ∃ (fun (z : uset (maxi_fun w x)) ⇒ tpair _ (pr1 z) (trans w (pr2 z) p)).
  split.
  - intros x0 y0 q.
    exact q.
  - ∃ (tpair _ x p).
    intro x0.
    exact (pr2 x0).
Defined.

Lemma maxidom (w : wfs) : ∏ (x : uset w ), wfs_wf_uord (maxi_fun w x) w.
Proof.
  intro x.
  ∃ (fun (z : uset (maxi_fun w x)) ⇒ pr1 z).
  split.
  - intros x0 y p.
    exact p.
  - ∃ x.
    intro x0.
    exact (pr2 x0).
Defined.

Lemma maxi (w : wfs) : wfs_wf_uord w wfs_wf_t.
Proof.
  ∃ (maxi_fun w).
  split.
  - exact (maxi_homo w).
  - exact (tpair _ _ (maxidom w)).
Defined.

Proposition whoa : uord wfs_wf_t wfs_wf_t wfs_wf_t.
Proof.
  apply maxi.
Defined.

Proposition irref (w : wfs) : ∏ (x : uset w ), (uord w) x x → Flse.
Proof.
  intro x.
  intro p.
  exact (wfp w (fun n ⇒ x) (fun n ⇒ p)).
Defined.

Proposition the_world_explodes : Flse.
Proof.
  exact (irref wfs_wf_t wfs_wf_t whoa).
Defined.

End girard.

Proposition but_seriously_the_world_explodes : empty.
  exact (the_world_explodes empty).
Defined.