[Agda] Agda with excluded middle is inconsistent

[David Wahlstedt]

Hmm, yes, I did miss something :-)

David

On Fri, Jan 8, 2010 at 12:05 PM, Noam Zeilberger
<noam.zeilberger at gmail.com>wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100108/9feb2bb3/attachment.html