<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div><blockquote type="cite"><div>Thanks for your answer.<br>Ok, Agda is a kind of constructive math assuming an anti-classical axiom.<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>No, see my last email.<br><div><br></div><blockquote type="cite"><div>Then, I have a few more questions.<br><br>Does the orginal Martin-Lof type theory also assume the injectivity of inductive type constructors ? </div></blockquote><div><br></div><div>No. You cannot even show that List : Set -> Set is injective without using universe recursion. Without this you can only show injectivity if it holds upto isomorphism, I think. (Which is how it should be, actually, extensionally equality of sets should be isomorphism).</div><br><blockquote type="cite"><div>or Agda added it later?<br>If the latter is the case, has the consistency of Agda been shown?<br></div></blockquote><div><br></div><div>Nope. I suspect it is easier to establish the contrary... :-)</div><div><br></div><blockquote type="cite"><div>Or, is there a set-theoretic model of Agda ?<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>As you have shown there isn't at least not wrt the current implementation. There should be one and Agda should not be anticlassical.</div><div><br></div><div>We clearly have to make a difference between the system we want and the system which is actually implemented. While we may want a system where we can prove injectivity of type constructors which are intensionally injective (such as List) we certainly don't want a system where we can prove injectivity of type constructors which are not even intensionally injective such as your example. This is just a bug, but it may be not easy to fix in a reasonable way.</div><div><br></div><div>Cheers,</div><div>Thorsten<br><div><br></div><br><blockquote type="cite"><div>Thanks,<br>Chung-Kil Hur<br><br>----- Original Message ----- <br>From: "Dan Doel" <<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>><br>To: <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>Cc: "Chung Kil Hur" <<a href="mailto:ckh25@cam.ac.uk">ckh25@cam.ac.uk</a>>; <<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>><br>Sent: Thursday, January 07, 2010 3:43 AM<br>Subject: Re: [Agda] Agda with the excluded middle is inconsistent ?<br><br><br><blockquote type="cite">On Wednesday 06 January 2010 6:59:14 pm Chung Kil Hur wrote:<br></blockquote><blockquote type="cite"><blockquote type="cite">Hi everyone,<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">I proved the absurdity in Agda assuming the excluded middle.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Is it a well-known fact ?<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">It seems that Agda's set theory is weird.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">This comes from the injectivity of inductive type constructors.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">The proof sketch is as follows.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Define a family of inductive type<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">data I : (Set -> Set) -> Set where<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">with no constructors.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">By injectivity of type constructors, I can show that I : (Set -> Set) -><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> Set is injective.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">As you may see, there is a size problem with this injectivity.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">So, I just used the cantor's diagonalization to derive absurdity in a<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> classical way.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Does anyone know whether cantor's diagonalization essentially needs the<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> classical axiom, or can be done intuitionistically ? If the latter is<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> true, then the Agda system is inconsistent.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Please have a look at the Agda code below, and let me know if there's any<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> mistakes.<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">I could certainly be wrong, but I don't think your code can be done without <br></blockquote><blockquote type="cite">assuming the excluded middle. For instance, I know of no way to write J <br></blockquote><blockquote type="cite">without it, because it would involve examining the parameter 'a' to see if it <br></blockquote><blockquote type="cite">is of the form 'I f' for some f, and that is not an operation that Agda <br></blockquote><blockquote type="cite">provides. You use the LEM that way several times, so I'm not particularly <br></blockquote><blockquote type="cite">worried that type constructor injectivity might be inconsistent. :)<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">More to the point, there are a couple ways to approach <br></blockquote><blockquote type="cite">constructivism/intuitionism. On the one hand, you can eliminate the classical <br></blockquote><blockquote type="cite">axioms, and see what kind of things you can still prove. But, you don't <br></blockquote><blockquote type="cite">necessarily have to stop there; you can also add anti-classical axioms that <br></blockquote><blockquote type="cite">would lead to inconsistency in a classical setting, but don't (and, perhaps, <br></blockquote><blockquote type="cite">are intuitively 'true') in a constructive setting. For instance, I've heard <br></blockquote><blockquote type="cite">some intuitionistic mathematics adds "all functions are continuous" as an <br></blockquote><blockquote type="cite">axiom.* And from that, and another anti-classical axiom or two, you can prove <br></blockquote><blockquote type="cite">that Nat is isomorphic to (Nat -> Bool) -> Bool, which is rather weird.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Injectivity of type constructors seems to be another anti-classical axiom. <br></blockquote><blockquote type="cite">Engaging in some loose meta-reasoning about Agda, we know that Set -> Set is <br></blockquote><blockquote type="cite">really the same size as Set, because every element of both corresponds to a <br></blockquote><blockquote type="cite">finite character string---the Agda program(s) that denotes it. So there isn't <br></blockquote><blockquote type="cite">really a size paradox in saying that there are injective functions into Set <br></blockquote><blockquote type="cite">from Set -> Set. And, intuitively, it's pretty clear that if f is a Set -> <br></blockquote><blockquote type="cite">Set, then I f is a Set such that if it is equal to I g, then f is equal to g, <br></blockquote><blockquote type="cite">because I f and I g aren't subject to any kind of reduction beyond <br></blockquote><blockquote type="cite">normalization of f an g.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">But, as you've demonstrated this cuts us off from postulating and reasoning <br></blockquote><blockquote type="cite">about classical things in our language. So I could see why Coq wouldn't want <br></blockquote><blockquote type="cite">it (since they turned off impredicative set by default for the same reason). <br></blockquote><blockquote type="cite">And, of course, I could be wrong, and it may not be intuitionistically valid, <br></blockquote><blockquote type="cite">either.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Cheers,<br></blockquote><blockquote type="cite">-- Dan<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">* <a href="http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/">http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/</a></blockquote>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></blockquote></div><br></body></html>