[Agda] Agda with excluded middle is inconsistent

[Noam Zeilberger]

On Fri, Jan 8, 2010 at 11:33 AM, Noam Zeilberger
<noam.zeilberger at gmail.com> wrote:
> 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.

On second thought, I am not sure about this.  To derive a
contradiction from Chung-Kil's example you would need to commute a
second-order quantifier.  He uses:

LEM = ∀ P. P \/ ~P

In intuitionistic second-order logic you can prove ∀ P.~~(P \/ ~P),
but not ~~(∀ P. P \/ ~P).

Noam