The Coq mailing list

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

Hi Cody,

Forgive the possibly naive question, but what I am wondering here is: where do 
you draw the line? With intuitionism, there is a very clear and formal boundary 
for what we consider 'acceptable' and what not. Say, pCuIC. People might 
disagree about which calculus/logic is the "right" one, but each calculus is 
very clearly delineating terms/theorems we accept from those we do not.

On the other hand, you seem to draw a line somewhere between "Ack 1 1" and "Ack 
5 5". I assume you will not want to pin down this line *precisely*, since any 
choice is by necessity arbitrary, but that is exactly my point, and it is why I 
do not agree with your arguments. Put differently: if we lived in a *shrinking* 
universe where more matter comes into the "observable universe" over time, would 
"Ack 5 5" suddenly be an acceptable statement to you once the number of atoms in 
the observable universe has grown enough?

Kind regards,
Ralf

On 03.06.21 23:04, roux cody wrote:
> Not sure how kosher it is to talk about foundational issues on the Club, since 
> it seems to tend to inspire a lot of opinionated debate...
>
> However... :)
>
> I stand by my analogy!
>
> I can certainly imagine an oracle that decides the Truth of an arbitrary 
> arithmetic statement, and communicate the idea to other humans (I just did!).
>
> I can also imagine wanting evidence that, in addition to an explanation being 
> constructive, that the answer to a question might fit on a computer composed of 
> all the atoms in the universe, or (if I'm feeling demanding) on my own computer.
>
> A reasonable objection to the above: we can always prove a concrete bound on a 
> number using intuitionistic logic.
>
> My rejoinder: the same can be said about constructive results and classical 
> logic: we can always just exhibit a Turing machine and classically prove that it 
> terminates.
>
> At any rate: In Coq, we may assume that every term has some hypothetical 
> ghost-like normal form, and maybe even that is a theorem in ZFC+some 
> inaccessible, and that's that.
>
> Personally, I treat Ack 5 5 the same way one might treat Hypercompact cardinals: 
> fun to do math at, but I don't feel it "really" exists. I'll assume it if I need 
> it to prove something though.
>
> Best,
>
> On Thu, Jun 3, 2021 at 3:10 PM Thorsten Altenkirch 
> <Thorsten.Altenkirch AT nottingham.ac.uk 
> <mailto:Thorsten.Altenkirch AT nottingham.ac.uk>> wrote:
>
>       No it’s not the same. The idea that some computation will terminate
>     eventually even if we are not able to perform it in practice is clearly
>     understandable and communicable among humans. It is different to ignoring
>     the need for constructive explanations altogether.
>
>     Sent from my iPhone
>
> >     On 3 Jun 2021, at 18:34, roux cody <cody.roux AT gmail.com
> >     <mailto:cody.roux AT gmail.com>> wrote:
> >
> >     
> >     It certainly feels very hard to distinguish between Very Large Numbers and
> >     Non Standard ones, and the distinction does seem very closely related to
> >     normalization.
> >
> >     But I'd advocate a slightly more subtle position than "There are
> >     absolutely less than 10^74 integers", but rather, "Gee, it sure gets hard
> >     to name (most) numbers bigger than 2^10^74..."
> >
> >     The same way intuitionism doesn't say: "This specific machine, M, neither
> >     terminates nor runs forever" but says "Maybe we shouldn't make the blanket
> >     assumption that *all* machines either terminate or run forever".
> >
> >     I suspect this agnosticism is what I'm really advocating (but one can't
> >     really be too sure...)
> >
> >     Best,
> >     Cody
> >
> >     Best,
> >     Cody
> >
> >     On Thu, Jun 3, 2021 at 12:26 PM Eddy Westbrook <westbrook AT galois.com
> >     <mailto:westbrook AT galois.com>> wrote:
> >
> >         Cody,
> >
> >         My initial reaction was that Ack 5 5 will eventually compute to a
> >         specific finite natural number, so at some point c_gtN will be
> >         inconsistent.
> >
> >         But I think your argument has an interesting twist: you are basically
> >         arguing using a version of Ultrafinitism, that there are finite
> >         numbers that are just too big to represent in the 10^74 atoms in the
> >         universe. What you are saying is that it is not possible to actually
> >         write down a counterexample.
> >
> >         A counter-argument, then: if we are starting from ultrafinitism, then
> >         there are definitely no infinitary natural numbers, because there are
> >         in fact only finitely many elements of any type.
> >
> >         -Eddy
> >
> > >         On Jun 3, 2021, at 9:13 AM, roux cody <cody.roux AT gmail.com
> > >         <mailto:cody.roux AT gmail.com>> wrote:
> > >
> > >         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 <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.
>     This message and any attachment are intended solely for the addressee
>     and may contain confidential information. If you have received this
>     message in error, please contact the sender and delete the email and
>     attachment.
>
>     Any views or opinions expressed by the author of this email do not
>     necessarily reflect the views of the University of Nottingham. Email
>     communications with the University of Nottingham may be monitored
>     where permitted by law.

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