The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On May 7, 2012, at 12:59 PM, Chad E Brown wrote:
> I proved Russell's Paradox up to universe inconsistency starting from the 
> Aczel type of sets V and Schepler's V_rel.

I took the liberty of reorganizing this proof a little.  I think it's easier 
to see what's going on this way:


(* Sets, a la Aczel *)
Inductive V : Type := V_const : forall {X:Type}, (X -> V) -> V.

(* Set membership *)
Inductive V_rel : V -> V -> Prop :=
  V_rel_def : forall {X:Type} (f:X -> V) (x:X), V_rel (f x) (V_const f).

Lemma V_rel_inv : forall y X (f:X -> V), V_rel y (V_const f) -> exists x, y = 
f x.
  intros y X f H. inversion H; eauto.
Qed.

(* The proper class of sets not containing themselves. *)
Definition RT : Type := {x:V | ~V_rel x x}.

Theorem Russell_paradox : False.
  (* Define the Russell set. This is the key step that causes universe 
inconsistency.
     If we defined this at top-level, it would already fail. *)
  set (russell := V_const (fun x:RT => proj1_sig x)).
     
  (* Show that the Russell set fails to contain itself. *)
  assert (Hrussell1 : ~V_rel russell russell).
    intro H. subst russell. 
    apply V_rel_inv in H. destruct H as [[x H] Hx].
    apply H. simpl in Hx. pattern x at 2. rewrite <- Hx.
    apply (@V_rel_def RT (@proj1_sig _ _) (exist _ x H)).

  (* Therefore, the Russell set contains itself. *)
  assert (Hrussell2 : V_rel russell russell).
    apply (@V_rel_def RT (@proj1_sig _ _) (exist _ russell Hrussell1)).

  (* Thus, contradiction. *)
  exact (Hrussell1 Hrussell2). (* Coq reports "Proof completed." *)

Show Proof. (* We've generated a complete proof term... *)
Qed. (* Now the typechecking core discovers our mistake: Universe 
inconsistency. *)