<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META content="text/html; charset=ks_c_5601-1987" http-equiv=Content-Type>
<META name=GENERATOR content="MSHTML 8.00.6001.18854">
<STYLE></STYLE>
</HEAD>
<BODY bgColor=#ffffff>
<DIV><FONT size=2 face=Arial>Hi,</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>I need to mention one more thing.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Indeed, the injectivity of inductive type
constructor is inconsistent in the prsence of Prop without LEM.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Actually, the original idea came from Alexandre
Miquel.</FONT></DIV>
<DIV><FONT size=2 face=Arial>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".</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>His proof in Coq is as follows:</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2
face=Arial>----------------------------------------------------------------------<BR>Inductive
I : (Prop -> Prop) -> Prop := .<BR><BR>Axiom inj_I : forall x y, I x = I y
-> x = y.<BR><BR>Definition R (x : Prop) := forall p, x = I p -> ~ p
x.<BR><BR>Lemma R_eqv :<BR> forall p, R (I p) <-> ~ p (I
p).<BR><BR>Proof.<BR>split; intros.<BR> unfold R; apply
H.<BR> reflexivity.<BR> unfold R; intros q H0.<BR> rewrite <-
(inj_I p q H0).<BR> assumption.<BR>Qed.<BR><BR>Lemma R_eqv_not_R
:<BR> R (I R) <-> ~ R (I R).<BR><BR>Proof (R_eqv R).<BR><BR>Lemma
absurd : False.<BR><BR>Proof.<BR>destruct R_eqv_not_R.<BR>exact (H (H0 (fun x
=> H x x)) (H0 (fun x => H x
x))).<BR>Qed.<BR>-----------------------------------------------------</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>From this proof, I realized it can be applied to
Set as well.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2
face=Arial>-----------------------------------------------------</FONT></DIV>
<DIV><FONT size=2 face=Arial>Inductive I : (Set -> Set) -> Set := <BR>| i1
: I (fun x => x)<BR>| i2 : I (fun x => x)<BR>.<BR><BR>Axiom inj_I : forall
x y, I x = I y -> x = y.<BR><BR>Definition R (x : Set) : Set := forall p: Set
-> Set, x = I p -> p x -> False.<BR><BR>Lemma R_eqv_1 :<BR>
forall p, R (I p) -> (p (I p) -> False).<BR><BR>Proof.<BR>intros ? ?.
<BR> apply H. reflexivity.<BR>Qed.<BR><BR>Lemma R_eqv_2 :<BR> forall
p, (p (I p) -> False) -> R (I p).<BR><BR>intros.<BR> unfold R; intros
q H0.<BR> rewrite <- (inj_I p q
H0).<BR> assumption.<BR>Qed.<BR><BR>Lemma R_eqv_not_R_1 :<BR> R (I R)
-> R (I R) -> False.<BR><BR>Proof (R_eqv_1 R).<BR><BR>Lemma R_eqv_not_R_2
:<BR> (R (I R) -> False) -> R (I R).<BR><BR>Proof (R_eqv_2
R).<BR><BR>Lemma absurd : False.<BR><BR>Proof.<BR>set (H :=
R_eqv_not_R_1).<BR>set (H0 := R_eqv_not_R_2).<BR><BR>exact (H (H0 (fun x => H
x x)) (H0 (fun x => H x
x))).<BR>Qed.<BR>------------------------------------------------</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>But, in this proof, we need to notice that we use
"False : Prop" rather than "Empty_set : Set".</FONT></DIV>
<DIV><FONT size=2 face=Arial>If you change "False" to "Empty_set", then the type
of R cannot be "Set -> Set", rather it should "Set -> Type".</FONT></DIV>
<DIV><FONT size=2 face=Arial>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</FONT></DIV>
<DIV><FONT size=2 face=Arial>coercible to Set -> Set.</FONT></DIV>
<DIV><FONT size=2 face=Arial>This proof does not need any axiom, but just the
impredicativity of Prop.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>So, this idea does not aplly to Agda because it
does not have any impredicative set like Prop.</FONT></DIV>
<DIV><FONT size=2 face=Arial>So, I applied cantor's diagonalization assuming the
law of excluded middle.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>I think the presence of Prop is one of the fancy
features of Coq as a proof assistant (at least to me).</FONT></DIV>
<DIV><FONT size=2 face=Arial>So, the injectivity seems unatural to me in this
view point.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Cheers,</FONT></DIV>
<DIV><FONT size=2 face=Arial>Chung-Kil Hur</FONT></DIV>
<DIV><FONT face=Arial></FONT> </DIV>
<DIV><FONT face=Arial></FONT> </DIV>
<DIV><FONT face=Arial>----- Original Message ----- </FONT></DIV>
<BLOCKQUOTE
style="BORDER-LEFT: #000000 2px solid; PADDING-LEFT: 5px; PADDING-RIGHT: 0px; MARGIN-LEFT: 5px; MARGIN-RIGHT: 0px">
<DIV style="FONT: 10pt ±¼¸²; BACKGROUND: #e4e4e4; font-color: black"><FONT
face=Arial><B>From:</B> </FONT><A title=ckh25@cam.ac.uk
href="mailto:ckh25@cam.ac.uk"><FONT face=Arial>Chung Kil Hur</FONT></A><FONT
face=Arial> </FONT></DIV>
<DIV style="FONT: 10pt ±¼¸²"><FONT face=Arial><B>To:</B> </FONT><A
title=agda@lists.chalmers.se href="mailto:agda@lists.chalmers.se"><FONT
face=Arial>Agda mailing list</FONT></A><FONT face=Arial> ; </FONT><A
title=coq-club@inria.fr href="mailto:coq-club@inria.fr"><FONT
face=Arial>coq-club@inria.fr</FONT></A><FONT face=Arial> </FONT></DIV>
<DIV style="FONT: 10pt ±¼¸²"><FONT face=Arial><B>Sent:</B> Thursday, January 07,
2010 12:59 AM</FONT></DIV>
<DIV style="FONT: 10pt ±¼¸²"><FONT face=Arial><B>Subject:</B> [Agda] Agda with
the excluded middle is inconsistent ?</FONT></DIV>
<DIV><FONT face=Arial><BR><FONT size=2></FONT></FONT></DIV>
<DIV>
<DIV><FONT size=2 face=Arial>Hi everyone,</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>I proved the absurdity in Agda assuming the
excluded middle.</FONT></DIV>
<DIV><FONT size=2 face=Arial>Is it a well-known fact ?</FONT></DIV>
<DIV><FONT size=2 face=Arial>It seems that Agda's set theory is
weird.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>This comes from the injectivity of inductive type
constructors.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>The proof sketch is as follows.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Define a family of inductive type</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>data I : (Set -> Set) ->
Set where</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>with no constructors.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>By injectivity of type constructors, I can show
that I : (Set -> Set) -> Set is injective.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>As you may see, there is a size problem with this
injectivity.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>So, I just used the cantor's diagonalization to
derive absurdity in a classical way.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Does anyone know whether cantor's diagonalization
essentially needs the classical axiom, or can be done intuitionistically
?</FONT></DIV>
<DIV><FONT size=2 face=Arial>If the latter is true, then the Agda system is
inconsistent.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Please have a look at the Agda code below, and
let me know if there's any mistakes.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>All comments are wellcome.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>Thanks,</FONT></DIV>
<DIV><FONT size=2 face=Arial>Chung-Kil Hur</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>============== Agda code
===============</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial>module cantor where</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data Empty : Set where</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data One : Set where<BR>
one : One</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data coprod (A : Set1) (B : Set1) : Set1
where<BR> inl : ¢£ (a : A) -> coprod A
B<BR> inr : ¢£ (b : B) -> coprod A B </FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> postulate exmid : ¢£ (A : Set1) ->
coprod A (A -> Empty)</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data Eq1 {A : Set1} (x : A) : A -> Set1
where<BR> refleq1 : Eq1 x x</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> cast : ¢£ { A B } -> Eq1 A B -> A
-> B<BR> cast refleq1 a = a</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> Eq1cong : ¢£ {f g : Set -> Set} a ->
Eq1 f g -> Eq1 (f a) (g a)<BR> Eq1cong a refleq1 =
refleq1</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> Eq1sym : ¢£ {A : Set1} { x y : A } ->
Eq1 x y -> Eq1 y x<BR> Eq1sym refleq1 = refleq1</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> Eq1trans : ¢£ {A : Set1} { x y z : A }
-> Eq1 x y -> Eq1 y z -> Eq1 x z<BR> Eq1trans refleq1 refleq1 =
refleq1</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data I : (Set -> Set) -> Set
where</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> Iinj : ¢£ { x y : Set -> Set } -> Eq1
(I x) (I y) -> Eq1 x y <BR> Iinj refleq1 = refleq1</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data invimageI (a : Set) : Set1
where<BR> invelmtI : forall x -> (Eq1 (I x) a) ->
invimageI a</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> J : Set -> (Set -> Set)<BR> J
a with exmid (invimageI a)<BR> J a | inl (invelmtI x y) = x<BR> J
a | inr b = ¥ë x ¡æ Empty</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data invimageJ (x : Set -> Set) : Set1
where<BR> invelmtJ : forall a -> (Eq1 (J a) x) ->
invimageJ x</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> IJIeqI : ¢£ x -> Eq1 (I (J (I x))) (I
x)<BR> IJIeqI x with exmid (invimageI (I x))<BR> IJIeqI x | inl
(invelmtI x' y) = y<BR> IJIeqI x | inr b with b (invelmtI x
refleq1)<BR> IJIeqI x | inr b | ()</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> J_srj : ¢£ (x : Set -> Set) ->
invimageJ x<BR> J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> cantor : Set -> Set<BR> cantor a
with exmid (Eq1 (J a a) Empty)<BR> cantor a | inl a' = One<BR>
cantor a | inr b = Empty</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> OneNeqEmpty : Eq1 One Empty ->
Empty<BR> OneNeqEmpty p = cast p one</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> cantorone : ¢£ a -> Eq1 (J a a) Empty
-> Eq1 (cantor a) One <BR> cantorone a p with exmid (Eq1 (J a a)
Empty)<BR> cantorone a p | inl a' = refleq1<BR> cantorone a p |
inr b with b p<BR> cantorone a p | inr b | ()</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> cantorempty : ¢£ a -> (Eq1 (J a a) Empty
-> Empty) -> Eq1 (cantor a) Empty<BR> cantorempty a p with exmid
(Eq1 (J a a) Empty)<BR> cantorempty a p | inl a' with p a'<BR>
cantorempty a p | inl a' | ()<BR> cantorempty a p | inr b =
refleq1</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> cantorcase : ¢£ a -> Eq1 cantor (J a)
-> Empty<BR> cantorcase a pf with exmid (Eq1 (J a a) Empty)<BR>
cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone
a a')) (Eq1cong a pf)) a')<BR> cantorcase a pf | inr b = b (Eq1trans
(Eq1sym (Eq1cong a pf)) (cantorempty a b))</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial> absurd : Empty<BR> absurd with
(J_srj cantor)<BR> absurd | invelmtJ a y = cantorcase a (Eq1sym
y)</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2
face=Arial>=====================================</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV></DIV>
<P><FONT size=2 face=Arial></FONT></P><FONT size=2 face=Arial>
<HR>
</FONT>
<P></P><FONT size=2
face=Arial>_______________________________________________<BR>Agda mailing
list<BR>Agda@lists.chalmers.se<BR>https://lists.chalmers.se/mailman/listinfo/agda<BR></FONT></BLOCKQUOTE></BODY></HTML>