[Agda] Agda with excluded middle is inconsistent

[Noam Zeilberger]

On Fri, Jan 8, 2010 at 11:18 AM, David Wahlstedt
<david.wahlstedt at gmail.com> 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 ?

Of course you're right.

Noam