The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

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

Attachment: signature.asc
Description: PGP signature