<!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>
<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 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 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></FONT> </DIV>
<DIV><FONT size=2 face=Arial> data Empty : Set where</FONT></DIV>
<DIV> </DIV>
<DIV><FONT size=2 face=Arial> data One : Set where<BR>
one : One</FONT></DIV>
<DIV> </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> </DIV>
<DIV><FONT size=2 face=Arial> postulate exmid : ¢£ (A : Set1) -> coprod
A (A -> Empty)</FONT></DIV>
<DIV> </DIV>
<DIV><FONT size=2 face=Arial> data Eq1 {A : Set1} (x : A) : A -> Set1
where<BR> refleq1 : Eq1 x x</FONT></DIV>
<DIV> </DIV>
<DIV><FONT size=2 face=Arial> cast : ¢£ { A B } -> Eq1 A B -> A ->
B<BR> cast refleq1 a = a</FONT></DIV>
<DIV> </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> </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> </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> </DIV>
<DIV><FONT size=2 face=Arial> data I : (Set -> Set) -> Set
where</FONT></DIV>
<DIV> </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> </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> </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> </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> </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> </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> </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> </DIV>
<DIV><FONT size=2 face=Arial> OneNeqEmpty : Eq1 One Empty ->
Empty<BR> OneNeqEmpty p = cast p one</FONT></DIV>
<DIV> </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> </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> </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> </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> </DIV>
<DIV><FONT size=2 face=Arial></FONT> </DIV></FONT></DIV></BODY></HTML>