The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> 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.

This will be a (very) big number, but in which sense is it "non-standard"? Seems 
like a completely well-behaved number to me?

Kind regards,
Ralf

> 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 
> <mailto: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
>     <mailto: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
> >         <mailto: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
> >         <mailto: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
> >             <mailto: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 <mailto: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.

--
Website: https://people.mpi-sws.org/~jung/