coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Chung Kil Hur" <ckh25 AT cam.ac.uk>
- To: "Agda mailing list" <agda AT lists.chalmers.se>, <coq-club AT inria.fr>
- Subject: [Coq-Club] Agda with the excluded middle is inconsistent ?
- Date: Thu, 7 Jan 2010 00:59:14 +0100
Hi everyone,
I proved the absurdity in Agda assuming the
excluded middle.
Is it a well-known fact ?
It seems that Agda's set theory is
weird.
This comes from the injectivity of inductive type
constructors.
The proof sketch is as follows.
Define a family of inductive type
data I : (Set -> Set) ->
Set where
with no constructors.
By injectivity of type constructors, I can show
that I : (Set -> Set) -> Set is injective.
As you may see, there is a size problem with this
injectivity.
So, I just used the cantor's diagonalization to
derive absurdity in a classical way.
Does anyone know whether cantor's diagonalization
essentially needs the classical axiom, or can be done intuitionistically
?
If the latter is true, then the Agda system is
inconsistent.
Please have a look at the Agda code below, and let
me know if there's any mistakes.
All comments are wellcome.
Thanks,
Chung-Kil Hur
============== Agda code
===============
module cantor where
data Empty : Set where
data One : Set where
one : One data coprod (A : Set1) (B : Set1) : Set1
where
inl : ¢£ (a : A) -> coprod A B inr : ¢£ (b : B) -> coprod A B postulate exmid : ¢£ (A : Set1) -> coprod
A (A -> Empty)
data Eq1 {A : Set1} (x : A) : A -> Set1
where
refleq1 : Eq1 x x cast : ¢£ { A B } -> Eq1 A B -> A ->
B
cast refleq1 a = a Eq1cong : ¢£ {f g : Set -> Set} a ->
Eq1 f g -> Eq1 (f a) (g a)
Eq1cong a refleq1 = refleq1 Eq1sym : ¢£ {A : Set1} { x y : A } -> Eq1
x y -> Eq1 y x
Eq1sym refleq1 = refleq1 Eq1trans : ¢£ {A : Set1} { x y z : A } ->
Eq1 x y -> Eq1 y z -> Eq1 x z
Eq1trans refleq1 refleq1 = refleq1 data I : (Set -> Set) -> Set
where
Iinj : ¢£ { x y : Set -> Set } -> Eq1
(I x) (I y) -> Eq1 x y
Iinj refleq1 = refleq1 data invimageI (a : Set) : Set1
where
invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a J : Set -> (Set -> Set)
J a with exmid (invimageI a) J a | inl (invelmtI x y) = x J a | inr b = ¥ë x ¡æ Empty data invimageJ (x : Set -> Set) : Set1
where
invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x IJIeqI : ¢£ x -> Eq1 (I (J (I x))) (I
x)
IJIeqI x with exmid (invimageI (I x)) IJIeqI x | inl (invelmtI x' y) = y IJIeqI x | inr b with b (invelmtI x refleq1) IJIeqI x | inr b | () J_srj : ¢£ (x : Set -> Set) ->
invimageJ x
J_srj x = invelmtJ (I x) (Iinj (IJIeqI x)) cantor : Set -> Set
cantor a with exmid (Eq1 (J a a) Empty) cantor a | inl a' = One cantor a | inr b = Empty OneNeqEmpty : Eq1 One Empty ->
Empty
OneNeqEmpty p = cast p one cantorone : ¢£ a -> Eq1 (J a a) Empty
-> Eq1 (cantor a) One
cantorone a p with exmid (Eq1 (J a a) Empty) cantorone a p | inl a' = refleq1 cantorone a p | inr b with b p cantorone a p | inr b | () cantorempty : ¢£ a -> (Eq1 (J a a) Empty
-> Empty) -> Eq1 (cantor a) Empty
cantorempty a p with exmid (Eq1 (J a a) Empty) cantorempty a p | inl a' with p a' cantorempty a p | inl a' | () cantorempty a p | inr b = refleq1 cantorcase : ¢£ a -> Eq1 cantor (J a)
-> Empty
cantorcase a pf with exmid (Eq1 (J a a) Empty) cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a') cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b)) absurd : Empty
absurd with (J_srj cantor) absurd | invelmtJ a y = cantorcase a (Eq1sym y) =====================================
|
- [Coq-Club] Agda with the excluded middle is inconsistent ?, Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?, Dan Doel
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?,
roconnor
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?, roconnor
- Message not available
- Message not available
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Andreas Abel
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Andreas Abel
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
- Message not available
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
Archive powered by MhonArc 2.6.16.