[Agda] Agda with the excluded middle is inconsistent ?
Chung Kil Hur
ckh25 at cam.ac.uk
Thu Jan 7 22:15:03 CET 2010
Hi,
I need to mention one more thing.
Indeed, the injectivity of inductive type constructor is inconsistent in the prsence of Prop without LEM.
Actually, the original idea came from Alexandre Miquel.
He told Hugo that the injectivity of type constroctors for inductive familes of Prop is inconsistent without any help of axioms like "P <-> Q" -> "P = Q".
His proof in Coq is as follows:
----------------------------------------------------------------------
Inductive I : (Prop -> Prop) -> Prop := .
Axiom inj_I : forall x y, I x = I y -> x = y.
Definition R (x : Prop) := forall p, x = I p -> ~ p x.
Lemma R_eqv :
forall p, R (I p) <-> ~ p (I p).
Proof.
split; intros.
unfold R; apply H.
reflexivity.
unfold R; intros q H0.
rewrite <- (inj_I p q H0).
assumption.
Qed.
Lemma R_eqv_not_R :
R (I R) <-> ~ R (I R).
Proof (R_eqv R).
Lemma absurd : False.
Proof.
destruct R_eqv_not_R.
exact (H (H0 (fun x => H x x)) (H0 (fun x => H x x))).
Qed.
-----------------------------------------------------
From this proof, I realized it can be applied to Set as well.
-----------------------------------------------------
Inductive I : (Set -> Set) -> Set :=
| i1 : I (fun x => x)
| i2 : I (fun x => x)
.
Axiom inj_I : forall x y, I x = I y -> x = y.
Definition R (x : Set) : Set := forall p: Set -> Set, x = I p -> p x -> False.
Lemma R_eqv_1 :
forall p, R (I p) -> (p (I p) -> False).
Proof.
intros ? ?.
apply H. reflexivity.
Qed.
Lemma R_eqv_2 :
forall p, (p (I p) -> False) -> R (I p).
intros.
unfold R; intros q H0.
rewrite <- (inj_I p q H0).
assumption.
Qed.
Lemma R_eqv_not_R_1 :
R (I R) -> R (I R) -> False.
Proof (R_eqv_1 R).
Lemma R_eqv_not_R_2 :
(R (I R) -> False) -> R (I R).
Proof (R_eqv_2 R).
Lemma absurd : False.
Proof.
set (H := R_eqv_not_R_1).
set (H0 := R_eqv_not_R_2).
exact (H (H0 (fun x => H x x)) (H0 (fun x => H x x))).
Qed.
------------------------------------------------
But, in this proof, we need to notice that we use "False : Prop" rather than "Empty_set : Set".
If you change "False" to "Empty_set", then the type of R cannot be "Set -> Set", rather it should "Set -> Type".
The reason why R is typable as Set -> Set is due to the impredicativity of Prop, because R is typepable as Set -> Prop, which is
coercible to Set -> Set.
This proof does not need any axiom, but just the impredicativity of Prop.
So, this idea does not aplly to Agda because it does not have any impredicative set like Prop.
So, I applied cantor's diagonalization assuming the law of excluded middle.
I think the presence of Prop is one of the fancy features of Coq as a proof assistant (at least to me).
So, the injectivity seems unatural to me in this view point.
Cheers,
Chung-Kil Hur
----- Original Message -----
From: Chung Kil Hur
To: Agda mailing list ; coq-club at inria.fr
Sent: Thursday, January 07, 2010 12:59 AM
Subject: [Agda] Agda with the excluded middle is inconsistent ?
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)
=====================================
------------------------------------------------------------------------------
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100107/e3310d04/attachment-0001.html
More information about the Agda
mailing list