[Agda] Agda with excluded middle is inconsistent

[David Wahlstedt]

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/6f47cae3/attachment.html