The Coq mailing list

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

One of my favorite examples of incompleteness is the value of the busy beaver 
function for "large" inputs, where I think "large" has been brought down below 
1000 at this point.
See §4.2 of <https://www.scottaaronson.com/papers/bb.pdf> (but the bound of 7910 
states there has been improved since then):

> There’s an explicit 7910-state Turing machine that halts iff the set theory
> ZF + SRP (where SRP means Stationary Ramsey Property) is inconsistent. Thus, 
> assuming that
> theory is consistent, ZF cannot prove the value of BB(7910).

Kind regards,
Ralf

On 24.06.21 04:48, Marco Servetto wrote:
> I'm more and more confused, but now I have an example that may help to
> clarify (and ends up hitting non-standard numbers too)
> -One of the typical examples for Propositions that may not be provable
> is termination of programs:
> -lets have "halt(p) = n" a partial function from program->nat, that returns 
> the
> number of steps the program p takes to terminate.
> - For all terminating programs, their execution trace is a valid and
> finite 'proof of termination'
> - For some programs, there is no proof of neither
>      Exists n: halt(p)=n       nor       not Exists n: halt(p)=n
> -Those programs do not terminate, otherwise we would have a
> termination proof using their execution trace.
>
> -Question1:  Where is the 'model' that defines 'truth' in my reasoning above?
>
> -Question2:  If I can somehow write down one of those programs, I
> could add as an axiom that Exists n: halt(p)=n, and the system should
> still be unable to prove true=false, right? is then such 'n' a non
> standard number? Is the reason we keep talking about non standard
> numbers connected with this question/issue?
>
> Marco.
>
> On Thu, 24 Jun 2021 at 06:44, Ken Kubota <mail AT kenkubota.de> wrote:
> > This is exactly my position!
> > (I read this after writing the other email.)
> >
> > All presentations of Goedel's theorems tacitly (implicitly) convey a specific 
> > philosophical approach without being conscious of the relativity of the 
> > approach as a whole when relying on a metatheory.
> >
> > Philosophically, relying on a metatheory is even self-contradictory.
> >
> >
> > Kind regards,
> >
> > Ken Kubota
> >
> > ____________________________________________________
> >
> > Ken Kubota
> > https://doi.org/10.4444/100
> >
> >
> >
> > Am 22.06.2021 um 11:11 schrieb Pierre-Marie Pédrot 
> > <pierre-marie.pedrot AT inria.fr>:
> >
> > What does that mean? Truth is always relative to your meta-theory so you
> > can't say much about "satisfaction in the meta" without explicitly
> > specifying the rules of your meta.
> >
> > I personally really hate the phrasing of Gödel's incompleteness theorem
> > as "there are unprovable true statements" because it's implicitly
> > referring to the meta and confusing the reader about some grand and
> > transcendental notion of "truth" when this does not exist. Except maybe
> > when you're a Girard fan and / or some neo-Popperian believer, in which
> > case you may claim that Π01 formulae are falsifiable in the only
> > standard model we have, a.k.a. our local universe, and thus there is
> > some well-behaved notion of truth for these (but not above).
> >
> > Incompleteness is really a boring theorem that can be phrased purely in
> > terms of provability without any irrelevant references to truth,
> > anchovies or hairy Schwarzschild black holes.

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