[Agda] Agda with the excluded middle is inconsistent ?

[Thorsten Altenkirch]

> Thanks for your answer.
> Ok, Agda is a kind of constructive math assuming an anti-classical axiom.

No, see my last email.

> Then, I have a few more questions.
> 
> Does the orginal Martin-Lof type theory also assume the injectivity of inductive type constructors ?

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).

> or Agda added it later?
> If the latter is the case, has the consistency of Agda been shown?

Nope. I suspect it is easier to establish the contrary... :-)

> Or, is there a set-theoretic model of Agda ?

As you have shown there isn't at least not wrt the current implementation. There should be one and Agda should not be anticlassical.

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.

Cheers,
Thorsten


> Thanks,
> Chung-Kil Hur
> 
> ----- Original Message ----- 
> From: "Dan Doel" <dan.doel at gmail.com>
> To: <agda at lists.chalmers.se>
> Cc: "Chung Kil Hur" <ckh25 at cam.ac.uk>; <coq-club at inria.fr>
> Sent: Thursday, January 07, 2010 3:43 AM
> Subject: Re: [Agda] Agda with the excluded middle is inconsistent ?
> 
> 
>> On Wednesday 06 January 2010 6:59:14 pm Chung Kil Hur wrote:
>>> 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.
>> 
>> I could certainly be wrong, but I don't think your code can be done without 
>> assuming the excluded middle. For instance, I know of no way to write J 
>> without it, because it would involve examining the parameter 'a' to see if it 
>> is of the form 'I f' for some f, and that is not an operation that Agda 
>> provides. You use the LEM that way several times, so I'm not particularly 
>> worried that type constructor injectivity might be inconsistent. :)
>> 
>> More to the point, there are a couple ways to approach 
>> constructivism/intuitionism. On the one hand, you can eliminate the classical 
>> axioms, and see what kind of things you can still prove. But, you don't 
>> necessarily have to stop there; you can also add anti-classical axioms that 
>> would lead to inconsistency in a classical setting, but don't (and, perhaps, 
>> are intuitively 'true') in a constructive setting. For instance, I've heard 
>> some intuitionistic mathematics adds "all functions are continuous" as an 
>> axiom.* And from that, and another anti-classical axiom or two, you can prove 
>> that Nat is isomorphic to (Nat -> Bool) -> Bool, which is rather weird.
>> 
>> Injectivity of type constructors seems to be another anti-classical axiom. 
>> Engaging in some loose meta-reasoning about Agda, we know that Set -> Set is 
>> really the same size as Set, because every element of both corresponds to a 
>> finite character string---the Agda program(s) that denotes it. So there isn't 
>> really a size paradox in saying that there are injective functions into Set 
>> from Set -> Set. And, intuitively, it's pretty clear that if f is a Set -> 
>> Set, then I f is a Set such that if it is equal to I g, then f is equal to g, 
>> because I f and I g aren't subject to any kind of reduction beyond 
>> normalization of f an g.
>> 
>> But, as you've demonstrated this cuts us off from postulating and reasoning 
>> about classical things in our language. So I could see why Coq wouldn't want 
>> it (since they turned off impredicative set by default for the same reason). 
>> And, of course, I could be wrong, and it may not be intuitionistically valid, 
>> either.
>> 
>> Cheers,
>> -- Dan
>> 
>> * http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/
> _______________________________________________
> 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/adfb1a9b/attachment.html