The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Sadly, it is possible to compute non-standard numbers in Coq without axioms. Here is an example:

Fixpoint Ack m := fix A_m n :=
  match m with
    | 0 => n + 1
    | S pm =>
      match n with
        | 0 => Ack pm 1
        | S pn => Ack pm (A_m pn)
      end
  end.

Definition c : nat := Ack 5 5.

Indeed adding axioms like c_gt0, c_gtS0, ... (as many as you like!) will all be consistent.

In practice, though, you can pretend that such numbers do not exist, and things will go on relatively undisturbed.

Best,

Cody

On Thu, Jun 3, 2021 at 10:16 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.