coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] help with excluded middle at point vs. all

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] help with excluded middle at point vs. all
Date: Sun, 3 Jul 2016 16:36:33 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:34NByRHOO83pRqYYqbs8PZ1GYnF86YWxBRYc798ds5kLTJ75o82wAkXT6L1XgUPTWs2DsrQf2rKQ6fmrADBeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxjbn5osGNKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCCLZ34RVHkhqhtURk3u6BjnUpr1+n/xsud41S+Ge9X3UZg7XD2j6+FgTxq+23RPDCIw7GyC0p84t6lcuh/0/xE=

On 2016-07-03 15:56, Jonathan Leivent wrote:
> I hit another constructive goal that is messing with my classical logic
> encumbered brain - a form of excluded middle at a point vs. overall:
>
> A : Type
> P : A -> Prop
> emp : forall a : A, P a \/ ~ P a
> ============================
> (forall a : A, P a) \/ ~ (forall a : A, P a)

If I read this right, then (for an arbitrary P) this is the omniscience
property of type A. The omniscience of nat isn't provable constructively, but
you can assume it under the so-called "limited principle of omniscience"
(https://en.wikipedia.org/wiki/Limited_principle_of_omniscience).

There's a nice discussion of this at
http://math.andrej.com/2014/05/08/seemingly-impossible-proofs/.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] help with excluded middle at point vs. all, Jonathan Leivent, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Vilhelm Sjoberg, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/03/2016
  - Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/14/2016
    - Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/14/2016
      - Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/15/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Clément Pit--Claudel, 07/03/2016
  - Re: [Coq-Club] help with excluded middle at point vs. all, Clément Pit--Claudel, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Abhishek Anand, 07/03/2016
  - Re: [Coq-Club] help with excluded middle at point vs. all, Jonathan Leivent, 07/03/2016