Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Agda with the excluded middle is inconsistent ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Agda with the excluded middle is inconsistent ?


chronological Thread 
  • 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)
 
=====================================
 
 



Archive powered by MhonArc 2.6.16.

Top of Page