The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

That's the limited principle of omniscience. The Coquelicot paper explains how it's used for classical real analysis.

On Tue, Feb 13, 2024 at 7:02 AM mukesh tiwari mukeshtiwari.iiitm-at-gmail.com |coq-club/Example Allow| <dsd13c3nm2whb1t AT sneakemail.com> wrote:

Hi everyone, 

I was looking into Coq standard library and saw this axioms sig_forall_dec [1] by a mere accident. I am trying to understand the intuition behind this axiom but my programming intuition simply cannot get it. I admit it is a classical axiom but I am finding it very hard to wrap my head around it.  

The way I see *sig_forall_dec* is a function that takes a function P --which returns Prop for every natural number-- and a function f ((forall n, {P n} + {~P n})) —which takes a natural number return P n or ~P n-- and it returns a proof object {n | ~P n} or returns a function {forall n, P n}. This whole things, to me, appears like a magic because we are turning a function *f* into proof object ({n | ~P n}) or a function for which P holds for every natural number ({forall n, P n}). I will appreciate if someone can shed a light on the intuition behind this magic. I presume it is used in reasoning of real numbers so what kind of proofs about real numbers require this axioms? 

Axiom sig_forall_dec
  : forall (P : nat -> Prop),
    (forall n, {P n} + {~P n})
    -> {n | ~P n} + {forall n, P n}.

Best, 

Mukesh

[1] https://coq.inria.fr/doc/V8.17.1/stdlib/Coq.Reals.ClassicalDedekindReals.html