The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Vincent,

I think there is some confusion here: assuming Coq is SN (there is some vagueness here about whether SN for Coq has been proved, but let’s side-step that here), then all ground terms of type nat will indeed correspond to finite natural numbers. So, in once sense, you are guaranteed not to have any non-standard natural numbers.

Note, however, that talking about “ground terms” actually means we are focusing on a particular model. There are certainly models of Coq where the type nat corresponds to a set with infinite objects, if that’s what you mean. However, you cannot distinguish anything that counts as a non-standard natural from a standard natural *in the theory*. Again, that’s what leads to the traditional non-standard naturals in Peano arithmetic, because Peano arithmetic is weak enough that it cannot define the notion of “this nat is finite”.

Does this make sense?

-Eddy

On Jun 3, 2021, at 7:15 AM, Vincent Semeria <vincent.semeria AT gmail.com> wrote:

Hi Eddy, 

On the contrary, I would like to avoid non standard numbers, so that the normalization property of Coq does mean that every computation of a nat term terminates.

But since we established that Coq cannot refute non standard nat terms, I am trying to measure the risk that I accidentally try to compute a non standard nat (without any axioms posed). 

On Thu, Jun 3, 2021, 16:06 Eddy Westbrook <westbrook AT galois.com> wrote:

Vincent,

There are certainly non-standard models of Coq (Gödel ensures us of that), but they are bound to be a lot more complicated than non-standard models of Peano arithmetic, which is where the notion of non-standard naturals comes from. The reason for this is that Coq can express a general notion of well-foundedness and induction in the logic (this is in fact the heart of Evan’s answer, that you can use induction in Coq), whereas Peano arithmetic cannot.

If what you really want is non-standard models of Peano arithmetic, then you will probably have to formalize Peano arithmetic, or at least a simpler form of it. I would guess that there are formalizations of it in Coq out there, but am not sure. A simpler form of Peano arithmetic might just be to define a signature (or, better, a type class) of types that have a 0 and successor but not necessarily induction.

If what you want is just infinite natural numbers, maybe you should look at Coq’s coinductive types? These let you define a Coq type that can contain infinite sequences of successors.

Hope this helps,

-Eddy

On Jun 3, 2021, at 6:53 AM, Vincent Semeria <vincent.semeria AT gmail.com> wrote:

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.