The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

> the case for these Goedel sentences being true seems pretty solid to me

Yes, Goedel's sentence is a better example than my original question about consistency. It encodes the liar's paradox "I am not provable", which is not provable by definition, and hence obviously true somewhere. And since it is not refutable either, it must be false somewhere else. As it happens, "somewhere" is the standard model of arithmetic and "somewhere else" is a non standard model. In other words, the liar's paradox has proofs encoded by non standard numbers only.

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

Agreed.

But all this applies to theories that include Peano arithmetic. I still do not understand how to generalize this to theories in other languages, like ZFC or Coq. To remain first-order, let's take ZFC as the meta-theory. What could then be an arithmetical proposition P true in the set of natural numbers IN, but not provable? In other words, what is the difference between

ZFC |-- IN satisfies P

and

ZFC |-- P_IN

where P_IN is the syntactic transformation of P where all quantifiers are made over IN. Those 2 sequents seem equivalent to me, by induction on the arithmetic proposition P. 

On Tue, Jun 29, 2021, 21:44 roux cody <cody.roux AT gmail.com> wrote:

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