The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

> the usual model of arithmetic in Coq does indeed rule out non-standard models.

I am not sure how a model of Coq would solve this problem. Consider Werner's model where types of Coq are interpreted by ZFC sets. Even if type nat was interpreted by the usual set of natural numbers IN (the first limit ordinal), then a definable non-standard c : nat would be interpreted as a non-standard element of IN. That would be sad for both Coq and ZFC, but I see no contradiction, since ZFC also cannot refute non-standard numbers.

On Thu, Jun 3, 2021 at 8:18 PM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

Hi Vincent,

> How do these non standard integers cope with the normalization property of
> Coq? A non standard integer would compute to an infinite sequence of
> successors, so it does not terminate.
>
> Is it a property of Coq that all definable nat terms are standard? If so,
> how is "standard" defined?

One must provide many details in order to have a rigorous discussion
about this, but the informal answer is that the usual model of
arithmetic in Coq does indeed rule out non-standard models.

The usual proof of the existence of non-standard models for PA does rely
on compactness, however, once you move to second order logic,
compactness doesn't work in the same way.

Another way to look at it is that replacing the axiom scheme from PA by
a single, second order induction principle usually rules out
non-standard models.

IIRC, the "Higher-Order Logic" chapter in the Handbook of Philosophical
Logic by Van Benthem and Doets discusses some of these issues.

E.