[Agda] Agda with the excluded middle is inconsistent ?

[Dan Doel]

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/