The Coq mailing list

[Daniel Schepler <(e29315a54f%hidden_head%e29315a54f)dschepler(e29315a54f%hidden_at%e29315a54f)gmail.com(e29315a54f%hidden_end%e29315a54f)>]

On Mon, May 7, 2012 at 11:49 AM, Robert Dockins 
<(e29315a54f%hidden_head%e29315a54f)robdockins(e29315a54f%hidden_at%e29315a54f)fastmail.fm(e29315a54f%hidden_end%e29315a54f)>
 wrote:
>
> 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:

And I reorganized it a bit more.  The major changes are in the
statement of V_rel_inv, to allow using it without rewrites, and in
separating out the proofs that membership in "russell" is exactly what
you'd expect it to be.

(* 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).

(* Elimination principle: to prove a statement P y, knowing that
   V_rel y (V_const f), it suffices to substitute y with (f x) for some x. *)
Lemma V_rel_inv : forall X (f:X -> V) (P:V -> Prop),
  (forall x:X, P (f x)) -> forall y:V, V_rel y (V_const f) -> P y.
Proof.
 intros X f P H y H0.
 (* "inversion H0" can't quite handle the dependent types, so we
    roll our own inversion. *)
 revert H.
 refine (match H0 in (V_rel a b) return
           (match b return Prop with
            | V_const X' f' => (forall x:X', P (f' x)) -> P a
            end) with
         | V_rel_def X' f' _ => _
         end). trivial.
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 V_rel x russell is exactly the negation of V_rel x x. *)
 assert (russell_rel : forall x:V, V_rel x russell -> ~V_rel x x).
   intros x H. inversion H using V_rel_inv. exact (@proj2_sig _ _).
 assert (russell_rel_rev : forall x:V, ~V_rel x x -> V_rel x russell).
   intros x H. change x with (proj1_sig (exist _ x H : RT)). apply V_rel_def.

 (* Show that the Russell set fails to contain itself. *)
 assert (Hrussell1 : ~V_rel russell russell).
   intro H. assert (H0 := russell_rel _ H). exact (H0 H).

 (* Therefore, the Russell set contains itself. *)
 assert (Hrussell2 : V_rel russell russell).
   exact (russell_rel_rev _ 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. *)
-- 
Daniel Schepler