The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Hi, Eddy.

  The work by Russel O’Connor on Gödel’s theorem is now maintained by Coq community. It contains a formalization of PA.

  For maintenance and development reasons, it is hosted in two libraries.

  Definition of primitive recursive functions and PA : as  the Ackermann sub-library  of https://github.com/coq-community/hydra-battles

  Proof of Gödel’s theorem (requires also the Pocklington library) https://github.com/coq-community/goedel

Best regards,

Pierre

Le 3 juin 2021 à 16:05, Eddy Westbrook <westbrook AT galois.com> a écrit :

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.