Mendelson in his book mentioned the Gödel sentence and argued that in standard interpretation it is true. But Peter Milne in his article (On Godel Sentences and What They Say) criticized: "But we know that we cannot move from consistency of T to truth of γ when no restriction has been put on the means of representation, the kind of formulas used". But I cant understand what he means. Can you help me?


There is no real conflict.

Mendelson is talking about a particular type of Gödel sentence, constructed in a standard way following the pattern of Gödel's original paper. [This is the kind of sentence people usually have in mind when they speak of a Gödel sentence for a theory $T$, without further qualification -- the sort of sentence constructed to "say", relative to a coding scheme, "I am unprovable in $T$".]

Milne on the other hand is talking about Gödel sentences in a more generic sense which is rather common nowadays, according to which any old fixed points $\gamma$ of the negation of the provability predicate for a theory $T$ counts as a Gödel sentence for the theory [i.e. any $\gamma$ such that $T \vdash \gamma \leftrightarrow \neg\mathsf{Prov}(\ulcorner\gamma\urcorner)$]. If $T$ is consistent but unsound, then the negation of the provability predicate can have false fixed points, so $T$ can have false Gödel sentences in the general sense.

Milne is complaining about people casually moving from a true claim about standardly constructed Gödel sentences (true if the theory is consistent) to false claim about generic Gödel sentences.

This is all explained in my Gödel book (pp. 182-183 of the second edition).

  • $\begingroup$ Thank you for your attention. But my problem has not been resolved, yet. What does Milne mean? "when no restriction has been put on the means of representation, the kind of formulas used". Why restriction must put on? $\endgroup$
    – user87128
    Jun 24 '14 at 9:47
  • $\begingroup$ Well, there is an issue too about which predicate we use to represent provability -- if Prov(x) represents provability so does Prov(x) $\land \varphi$, for any old theorem $\varphi$. In unsound theories the junk can be false, and using that provability predicate leads to more complications. $\endgroup$ Jun 24 '14 at 9:55
  • $\begingroup$ Ok. But we want to show truth of Godel sentence in standard interpretation. And we should not worry about some interpretations in which provability predicate is false for it. Am I right? $\endgroup$
    – user87128
    Jun 24 '14 at 10:21
  • $\begingroup$ Example, take the theory PA + $\neg$Con, where Con is the standard consistency sentence for PA. This theory is unsound on the standard interpretation. Milne's observation is that while, still on the standard interpretation, its canonical (standardly generated) Gödel sentence is true, it also has non-canonical Gödel sentences in the general sense of fixed points for $\neg$Prov which aren't true. So saying "Gödel sentences are always true on the standard interpretation" is wrong if you are using (as some writers do) "Gödel sentence" in the wider sense that covers non-canonical cases. $\endgroup$ Jun 24 '14 at 10:29
  • $\begingroup$ Ok. I understand it. Thank you very much. $\endgroup$
    – user87128
    Jun 24 '14 at 10:40