The Coq mailing list

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

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? 

On Wed, Jun 2, 2021, 22:25 roux cody <cody.roux AT gmail.com> wrote:

Sure, I mean your notional proof that the axiom schema is consistent.

On Wed, Jun 2, 2021 at 4:10 PM Evan Marzion <emarzion AT gmail.com> wrote:

By induction, c is greater than n for all n.  Thus, c > c, a contradiction.

On Wed, Jun 2, 2021 at 2:53 PM Vincent Semeria <vincent.semeria AT gmail.com> wrote:

Dear Coq club,

Is it possible to axiomatize a term c : nat, such as c is greater than all standard natural numbers ? The first 2 lines are easy,

Axiom c : nat.
Axiom c_gt0 : 0 < c.

But then, could we consistently add this axiom ?

Axiom c_non_standard : forall n:nat, n < c -> S n < c.

If the last axiom is not consistent, we could modify Coq's type checker to interpret all names of the form c_gtSSSS...S0 as closed terms of the corresponding types SSSS...S0 < c. I am pretty sure that these terms are consistent, because if they introduced a proof of False, that proof would be a finite lambda-term with only a finite number of these c_gt terms. Then c could be replaced by the greatest of these terms, and we would obtain a proof of False in basic Coq.