The Coq mailing list

[Chad E Brown <cebrown2323 AT yahoo.com>]

I proved Russell's Paradox up to universe inconsistency starting from the Aczel type of sets V and Schepler's V_rel.

Inductive V : Type :=

| V_const : forall {X:Type}, (X -> V) -> V.

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.

exists x0. reflexivity.

Qed.

Definition RT : Type := {x:V | ~V_rel x x}.

Lemma Russell : False.

cut (exists R:V, forall x:V, V_rel x R <-> ~V_rel x x).

intros [R H]. specialize (H R). tauto.

exists (V_const (fun u:RT => proj1_sig u)).

intros x. split; intros H1.

destruct (V_rel_inv x RT (fun u:RT => proj1_sig u) H1) as [[y H2] H3].

simpl in H3. rewrite H3. exact H2.

change (V_rel (proj1_sig (exist (fun x => ~V_rel x x) x H1)) (V_const (fun u : RT => proj1_sig u))).

apply V_rel_def.

Show Proof.

Qed.

- Chad

---

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Sent: Saturday, May 5, 2012 3:08 AM
Subject: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?

I finally managed (in principle) to construct a closed, axiom-free
term of type False, which would be accepted by the type checker if not
for the universe level restrictions...  (All my previous attempts,
like the formalization of the Cauchy paradox from some months ago,
ended up depending on at least eq_rect_eq.)

My question: Is there a simpler known term which would produce the same effect?

Inductive V : Type :=
| V_const : forall {X:Type}, (X -> V) -> V.

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_wf : well_founded V_rel.
Proof.
intro v.
induction v.
constructor.
intros.
revert H;
refine (match H0 in (V_rel v1 v2) return
  (match v2 return Prop with
  | V_const X f => (forall x:X, Acc V_rel (f x)) -> Acc V_rel v1
  end) with
| V_rel_def _ _ _ => _
end); clear X v y H0; intro H.
trivial.
Qed.

Lemma wf_irrefl : forall {X} (R:X->X->Prop),
  well_founded R -> forall x:X, ~ R x x.
Proof.
intros.
pose proof (H x).
induction H0.
intro.
exact (H1 x H2 H2).
Qed.

Lemma contradiction : False.
Proof.
set (V_top := V_const (fun v:V => v)).
pose proof (V_rel_def (fun v => v) V_top :
  V_rel V_top V_top).
pose proof (wf_irrefl _ V_rel_wf V_top).
exact (H0 H).
Qed.
--
Daniel Schepler