Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page