The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

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