coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?
chronological Thread
- From: Chad E Brown <cebrown2323 AT yahoo.com>
- To: Daniel Schepler <dschepler AT gmail.com>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?
- Date: Mon, 7 May 2012 09:59:05 -0700 (PDT)
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Mailer:References:Message-ID:Date:From:Reply-To:Subject:To:In-Reply-To:MIME-Version:Content-Type; b=otP/ZXYFIczv0w/9yd6YZChN74z0IARGG4yNDdKnIo6365KZjiECR4CeZaDimrx0DnjCwfzQEchZN51J9cMepa9hZcLC7KA/N1PiPRwt8k2WxWTH6KjZ7RImTRDD6v6pgy6bSbb6pKpnq6tHgfBI4fuCTzllOXenTI/AQKPu7PM=;
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
- [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?, Daniel Schepler
- Re: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?,
Randy Pollack
- Re: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?, Daniel Schepler
- Message not available
- Re: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?, Chad E Brown
- Re: [Coq-Club] Simple demonstration that the type hierarchy is needed for consistency?,
Randy Pollack
Archive powered by MhonArc 2.6.16.