Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent


chronological Thread 
  • From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
  • To: Noam Zeilberger <noam.zeilberger AT gmail.com>
  • Cc: Chung Kil Hur <Chung-Kil.Hur AT pps.jussieu.fr>, coq-club AT inria.fr, Agda mailing list <agda AT lists.chalmers.se>
  • Subject: [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent
  • Date: Thu, 7 Jan 2010 17:18:39 +0000


>> We should justify principles like this (i.e. all type constructors are 
>> injective) by a semantic explanation or by a translation into a well 
>> understood core language e.g. (extensional) Marttin-Loef Type Theory with 
>> W-types and universes. I don't know any such explanation which would 
>> justify this principle. Moreover, Chung's example shows that this is not 
>> possible (without giving up something else) since pure type theory is 
>> consistent with EM.
> 
> Agreed that there should be a convincing explanation, but again, I do
> think there is a strong intuition behind the principle (what Dan Doel
> and I were getting at), and the fact that it plays an important role
> in typechecking suggests that we shouldn't jump to conclusions.

I am not sure about this. *Most* datatype constructors are injective on type 
names, hence in functional programming one overgeneralizes this to *all*. 
Indeed this is one of the reasons that it is not clear how to add lambda 
abstractions on type level to Haskell, because Haskell assumes that all 
functions on the type level are injective. 

>  I am
> not sure that Agda should be conservative over classical mathematics:
> it seems there is a fundamental tension between exploiting the full
> power of a constructive type theory and upholding the fictions of
> classical mathematics.  Chung-Kil's paradox shows that you can't
> reason classically in Agda just by adding the law of excluded middle
> -- okay, so don't do it that way.

I don't think this is an instance of a constructive principle which is not 
valid classically (such as continuity). It seems rather an instance of 
something being wrong but not wrong enough to make the theory inconsistent. 
Another example is the propositional axiom of choice which is wrong but it 
doesn't make the theory inconsistent but only entails EM (by the Diaconescu 
construction). I mean being able to derive either EM or ~ EM are indications 
that something is wrong in these cases,

> Could you explain what you meant by: "Also while we may accept that
> extensions of Type Theory may be anticlassical, we should expect that
> core Type Theory is consistent with EM."?

In Martin-Loef Type Theory you cannot refute EM and I would expect that the 
same holds for Agda. Thinking about this, I wouldn't insist on this too 
strongly, but I'd need a better reason than "injectivity of type 
constructors". E.g. the observation that a function of type (Nat -> Nat) -> 
Nat can only use a finite amount of information of its input (i.e. 
continuity) we may want to built into our type theory (but how ?).

Cheers,
Thorsten






Archive powered by MhonArc 2.6.16.

Top of Page