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:37:36 -0400
  • Authentication-results: mail2-smtp-roc.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:I9B9CByYO255wF/XCy+O+j09IxM/srCxBDY+r6Qd0e4XIJqq85mqBkHD//Il1AaPBtSDragdwLOK7ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL2PbrnD61zMOABK3bVMzfbWtXNSLxJ3riaibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtM0rzyMFsPU4ssVETK/SfqIiTLUeAi51HXoy4ZjAsZjGQA2T0UMdTiBTuR5BHgTI6FmuVZP8tyb8qqxl2TWyMsj/TLRyUjOnufQ4ACT0gTsKYmZquFrcjdZ92fpW
On 2016-07-03 16:36, Clément Pit--Claudel wrote:
> 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).

Also related: https://en.wikipedia.org/wiki/Drinker_paradox

Attachment: signature.asc
Description: OpenPGP digital signature


Archive powered by MHonArc 2.6.18.

Top of Page