[Agda] Agda with the excluded middle is inconsistent ?

[Dan Doel]

On Thursday 07 January 2010 5:01:24 am Chung Kil Hur wrote:
> or Agda added it later? If the latter is the
>  case, has the consistency of Agda been shown?

I imagine it's relatively unique to Agda, as even (many? most?) other theorem 
provers don't assume it. Thorsten may be right in tracing it to Haskell, where 
it's probably more crucial. With the new type/data families, lack of 
injectivity of the former is a frequent annoyance with the inference engine, 
causing type errors where one might not expect them. That sort of thing is 
side stepped in Agda because type abstraction/application is a part of the 
language.

I don't think the consistency of Agda has been shown, since it's not been that 
long since the last time someone came up with a proof of false that didn't 
require excluded middle. :) Of course, you may mean the theory, but I doubt 
that's been proven either, since Agda has a fair amount of fancy stuff each 
individual bit of which you might see proved correct, but probably not all 
together.

As for justifying the injectivity of I (in reference to Thorsen Altenkirch's 
other mails), I suppose it rather depends on what you think data declarations 
are. If

  data I : (Set -> Set) -> Set where

is sugar for something like

  I : (Set -> Set) -> Set
  I _ = data {}

then no, it would appear to not be injective. But the type constructors 
defined by data don't appear to compute like that, at least. If I ask for the 
normal form of:

  I F -> I G

I don't get

  data {} -> data {}

I get what I put in. So all appearances indicate that type constructors 
defined by data (and codata for that matter) declarations do behave rather 
like the constructors of an inductive type, and that the normal form of "I F" 
is just "I F'" where F' is the normal form of F. And presumably the built-in 
equality judgment I F = I G does ensure that F = G.

But, of course, the above analysis may be overly specific to the sort of 
direct implementation of inductives that is currently used. I have no idea if 
it could survive elaboration into a core theory, which would, I assume, give 
you something much more like the "data {}" stuff. And that's really the 
direction to go in (it seems to me), because trusting a core theory is much 
easier than trusting that you've directly implemented all the sugar correctly.

Plus, people may in fact want to reason in the presence of a postulated 
excluded middle, so ruling that out with anti-classical axioms may not be the 
best idea.

-- Dan