coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] [Agda] Agda with excluded middle is inconsistent, Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Dan Doel
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
David Wahlstedt
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Andreas Abel
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
Archive powered by MhonArc 2.6.16.