The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

> I doubt my boss will be
placated by an argument that if we just give it a non-standard amount of

time to execute, then it will terminate.

How about ack(5,5) milliseconds?

(I should make this my email signature...)

On Tue, Jun 29, 2021 at 2:39 PM <roconnor AT theorem.ca> wrote:

On Tue, 29 Jun 2021, Louis Garde wrote:

> Le 29/06/2021 à 17:12, roconnor AT theorem.ca a écrit :
>       Thus the Goedel sentence G is true when ¬G is not provable.
>
> It is a fact that the notion of truth is not formally part of the Gödel theorem itself, which is "just" the exhibition of an unprovable sentence. To introduce the concept of truth as you
> have done, you had to specify an interpretation of the sentence, and therefore you had to work at the meta level, which is just the point of Pierre Marie Pédrot.

Yes you need to work at a meta level, but it same meta level that is used
to state and prove the incompleteness theorem in the first place.

For the example of PA, I currently have the incompleteness stated as

Theorem PAIncomplete :
  exists f : Formula,
    (Sentence f) /\ ~(SysPrf PA f \/ SysPrf PA (notH f)).

but it would be trival to extend this statement to say

Theorem PAIncomplete :
  exists f : Formula,
    (Sentence f) /\ ~(SysPrf PA f \/ SysPrf PA (notH f))
                 /\ (forall assignment, interpFormula natModel assignment f).

(though to make the above non-trival you'd want to replace (Sentence f)
with (Pi1Sentence f), something that could be defined but isn't currently
defined.)

My point here is that adding "and the Goedel sentence is true" doesn't
involve working at any any new meta level more than we are already working
at in the first place.

But yes, we do have to define a notion of truth, and Tarski's definition
is what is meant when people talk about the Goedel sentence being true
(see also below).

> There is no doubt that the Gödel sentence is true in some interpretations, and in the natural one. There is also no doubt that the Gödel sentence is false in some other interpretations,
> see for instance Truth of the Gödel sentence.

Sure, for non-standard interpretations.  But we didn't invent the rules of
arithemetic simply as a game to play among mathematicians; we are (or at
least I am) trying to reason about actual software, and proving that some
piece of software halts when doesn't actually halts is not particularly
helpful for that pursue, even if it is logically consistent and has a
non-standard model.

Standard and non-standard models are not equally as good in my opinion.
If I could use Coq to prove an algorithm is total, when it in fact is not
total, such an "unsound" conclusion is no good.  I doubt my boss will be
placated by an argument that if we just give it a non-standard amount of
time to execute, then it will terminate.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''