The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

This implies full classical logic.
Perhaps you meant to include decidability of P?
Such a similar statement can be found in the reals part of the std lib.

On Thu, Sep 18, 2014 at 2:05 PM, Alan Schmitt
<alan.schmitt AT polytechnique.org>
 wrote:
> Hello Daniel,
>
> My courses on logic are very far, so I have a question about one of your
> axioms.
>
> On 2014-09-15 17:55, Daniel de Rauglaudre 
> <daniel.de_rauglaudre AT inria.fr>
>  writes:
>
>> 5/ ∀ P : nat → Prop, { ∃ n, P n } + { ∀ n, ¬P n }.
>
> Isn't it too strong? If I take "P k" to be "function F terminate when
> given input k", doesn't this mean you can decide termination?
>
> Thanks,
>
> Alan
>
> --
> OpenPGP Key ID : 040D0A3B4ED2E5C7