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

[Benjamin Werner]

Isn't it about the quantification over P ?

In Coq with impredicative Set one can indeed prove
~(forall P : Set, P \/ ~P)
and from what I (quickly) read, it seems that Agda is now in this situation
(except probably that you quantify P over a predicative universe ?),
but it does not make the theory inconsistent.

I personally think that having this anti-classical theorem is indeed
uncomfortable for a proof system.

Since the discussed feature is even more about intentionality, I guess
extentional axioms would also be problematic ?

Best,

Benjamin


Le 8 janv. 2010 à 11:37, Thorsten Altenkirch a écrit :

> Red face... :-)
> 
> Thorsten
> 
> On 8 Jan 2010, at 10:18, David Wahlstedt wrote:
> 
>> Hi, 
>> I have read through the two threads on this topic, and:
>> Sorry if I mention something that is "too basic" / "naive", but, to clarify even more on Thorstens remark about the compatibility of MLTT with EM, it should be recalled that ~~(P \/ ~P) is a theorem even in very basic intuitionistic logic.
>> So if we add something to our system such that ~(P \/ ~P) becomes a theorem, we really have got an inconsistent system, without having to assume anything non-constructive. Or have I missed something ?
>> 
>> Best regards,
>> 
>> David Wahlstedt
>> 
>> On Thu, Jan 7, 2010 at 5:24 PM, Noam Zeilberger <noam.zeilberger at gmail.com> wrote:
>> On Thu, Jan 7, 2010 at 4:15 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>> >> ...I'm not sure about this expansion, and the analogy.  I think the
>> >> question is whether we view the declaration of type constructors in
>> >> the same way that we view the declaration of term constructors (i.e.,
>> >> as stipulating a new way of constructing things, in this case
>> >> inhabitants of Set).  If we do, then type constructors are by
>> >> definition injective.
>> >
>> > I don't see the analogy. A term constructor is injective because an inductive type is freely generated from constructors. Indeed, we can show that the structure map of an initial algebra is an isomorphism and hence injective. However the universe of sets is not freely constructed from type constructors but they are really definitions.
>> 
>> But freeness ("inductive type = no confusion + no junk") is only a
>> sufficient condition, right?  Injectivity = no confusion.
>> 
>> > 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 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.
>> 
>> 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."?
>> 
>> Noam
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100108/639e14d1/attachment.html