Hmm, yes, I did miss something :-)<br><br><div>David<br><div><br><div class="gmail_quote">On Fri, Jan 8, 2010 at 12:05 PM, Noam Zeilberger <span dir="ltr"><<a href="mailto:noam.zeilberger@gmail.com">noam.zeilberger@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">On Fri, Jan 8, 2010 at 11:33 AM, Noam Zeilberger<br>
<div class="im"><<a href="mailto:noam.zeilberger@gmail.com">noam.zeilberger@gmail.com</a>> wrote:<br>
</div><div><div></div><div class="h5">> On Fri, Jan 8, 2010 at 11:18 AM, David Wahlstedt<br>
> <<a href="mailto:david.wahlstedt@gmail.com">david.wahlstedt@gmail.com</a>> wrote:<br>
>> Hi,<br>
>> I have read through the two threads on this topic, and:<br>
>> Sorry if I mention something that is "too basic" / "naive", but, to clarify<br>
>> even more on Thorstens remark about the compatibility of MLTT with EM, it<br>
>> should be recalled that ~~(P \/ ~P) is a theorem even in very basic<br>
>> intuitionistic logic.<br>
>> So if we add something to our system such that ~(P \/ ~P) becomes a theorem,<br>
>> we really have got an inconsistent system, without having to assume anything<br>
>> non-constructive. Or have I missed something ?<br>
><br>
> Of course you're right.<br>
<br>
</div></div>On second thought, I am not sure about this. To derive a<br>
contradiction from Chung-Kil's example you would need to commute a<br>
second-order quantifier. He uses:<br>
<br>
LEM = ∀ P. P \/ ~P<br>
<br>
In intuitionistic second-order logic you can prove ∀ P.~~(P \/ ~P),<br>
but not ~~(∀ P. P \/ ~P).<br>
<font color="#888888"><br>
Noam<br>
</font></blockquote></div><br></div></div>