The Coq mailing list

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

Hi Cody,

> A very reasonable question! Here is the "standard" answer, which I *think* I 
> subscribe to?
>
> You're allowed to write/accept Ack 5 5, or indeed Ack 10 10, or any number you 
> like, *as long as* you define it using only EFA 
> (https://en.wikipedia.org/wiki/Elementary_function_arithmetic 
> <https://en.wikipedia.org/wiki/Elementary_function_arithmetic>). You don't get 
> to "meta define" it, using the assumption that PA is consistent, for example: 
> you have to actually write down the definition in full.

I see, so you are essentially not accepting (in general) the use of well-founded 
recursion, such as in your definition of "Ack"? I am now trying to imagine which 
part of maths is even expressible in this subset, and it seems to be tiny, but I 
assume there's tricks one can play.

I'd personally rather take MLTT or pCuIC or some similar calculus as the 
foundation and *define* addition and other parts of elementary arithmetic using 
well-founded recursion, but it seems we have different taste here. ;)

Kind regards,
Ralf

> Anything beyond that is forbidden. I'd add, even the totality of the exponential 
> function seems a bit fishy to an extremist like myself, but that's perhaps 
> another story. Of course you may postulate it's existence, just as you may 
> postulate the existence of non-trivial zeros of the Zeta function.
>
> Strict adherence to this principle would make it impossible for me to use and 
> enjoy Coq or Isabelle though. That said, people don't always become mennonites 
> when some universe inconsistency is discovered, so maybe there's some room for 
> compromise.
>
> Hope this somewhat explains my view.
>
> Best,
> Cody
>
> On Fri, Jun 4, 2021 at 10:10 AM Ralf Jung <jung AT mpi-sws.org 
> <mailto:jung AT mpi-sws.org>> wrote:
>
>     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>
>      > <mailto: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>
>      >>     <mailto: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>
>      >>     <mailto: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>
>      >>>         <mailto: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>
>     <mailto: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>
>      >>>             <mailto: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>
>      >>>>                 <mailto: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>
>      >>>>                 <mailto: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>
>     <mailto: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>
>      >>>>                         <mailto: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/ <https://people.mpi-sws.org/~jung/>

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