[Agda] Agda with the excluded middle is inconsistent ?

[Chung Kil Hur]

Dear Dan,

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

Then, I have a few more questions.

Does the orginal Martin-Lof type theory also assume the injectivity of inductive type constructors ? or Agda added it later?
If the latter is the case, has the consistency of Agda been shown?
Or, is there a set-theoretic model of Agda ?

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/