Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent


chronological Thread 
  • From: Noam Zeilberger <noam.zeilberger AT gmail.com>
  • To: David Wahlstedt <david.wahlstedt AT gmail.com>
  • Cc: Chung Kil Hur <Chung-Kil.Hur AT pps.jussieu.fr>, coq-club AT inria.fr, Agda mailing list <agda AT lists.chalmers.se>
  • Subject: [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent
  • Date: Fri, 8 Jan 2010 11:33:16 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=pd5VATqZtxaCO4oknY37l58mejVFZAhNM0iCI11mwlR2n/0J1UBjo0Yw9Uzw1ehRum fkp3iIVXo+0wZjVRtOOHkQSMYmJFarnF2zprj5sm+Zy2Y3LLoJsVU0/joAfC9KhAnBEL ycTTtxYL2StZEFWgp55PTekm+M5XT20R+i+iU=
  • List-archive: <http://lists.chalmers.se/pipermail/agda>
  • List-id: Agda implementors and users group <agda.lists.chalmers.se>
  • Resent-date: Tue, 19 Jan 2010 15:52:11 +0100
  • Resent-date: Tue, 19 Jan 2010 15:52:11 +0100
  • Resent-from: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • Resent-message-id: <20100119145211.GG17061 AT pirogue.inria.fr>
  • Resent-to: coq-club AT inria.fr
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
_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda


Archive powered by MhonArc 2.6.16.

Top of Page