The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

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.