The Coq mailing list

[roconnor AT theorem.ca]

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