The Coq mailing list

[Noam Zeilberger <noam.zeilberger AT gmail.com>]

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
_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda