Let's take Peano Arithmetic for concreteness. Gödel's sentence $G$ indirectly talks about itself and says "I am not a PA-theorem." Then we come to the conclusion that $G$ cannot be a PA-theorem (since PA proves only true things), and hence $G$ is true.

What about a sentence $H$ that says "I am a PA-theorem"? I think I saw on the internet some references about this issue, but now I cannot find them. Can someone provide references?

(Either $H$ is a PA-theorem and it is true, or it is not a PA-theorem and it is false. In either case, it's not so interesting. But which one is it? I think $H$ is false, because, in order to prove $H$, you would first have to prove $H$. In other words, suppose for a contradiction that $H$ has a proof in PA, and let $X$ be the shortest proof. Then, presumably, $X$ would be of the form: "$Y$ is a proof of $H$, hence $H$ is a PA-theorem, hence $H$ holds." But then $Y$ would be a shorter proof. Contradiction.)

  • 1
    $\begingroup$ The sentence $H$ is a PA-theorem. The proof as I recall goes like this. Construct another sentence $J$ which says "if I am a PA-theorem, then $H$ is a PA-theorem. Prove that $J$ is a PA-theorem, and then conclude that $H$ is also a PA-theorem. $\endgroup$ – bof Feb 8 '17 at 20:39
  • $\begingroup$ I believe this was posed as a problem in the Journal of Symbolic Logic many years ago. I don't remember who posed it or who solved it. $\endgroup$ – bof Feb 8 '17 at 20:42
  • $\begingroup$ Henkin, Kreisel, Löb, 1950s—see this reference. $\endgroup$ – bof Feb 8 '17 at 20:47
  • $\begingroup$ Does $H$ stand for Henkin? $\endgroup$ – bof Feb 8 '17 at 20:48
  • $\begingroup$ Well, now it does ;) $\endgroup$ – Gabriel Nivasch Feb 8 '17 at 20:55

The two answers presented above appear to contradict each other - let me resolve that contradiction.

Lob proved that, for all sentences $\varphi$, $$PA\vdash "(PA\vdash\varphi\implies\varphi)"\implies PA\vdash\varphi;$$ if PA proves that, if PA proves $\varphi$ then $\varphi$ is true, then PA proves $\varphi$. Intuitively, any "reasonable" expression of "I am provable" in the language of arithmetic has the property that PA proves that it is true iff it is provable, so any such sentence should be provable.

Meanwhile, say that a formula $\psi$ expresses provability if for all sentences $\theta$, $PA\vdash \psi([\theta])$ holds iff $PA\vdash\theta$ (where "$[\cdot]$" is the Goedel number operation).

What Kreisel proved was that there is a formula $\psi$ expressing provability, such that PA does not prove "$\psi($me$)$", the fixed point sentence for $\psi$.

The apparent contradiction is resolved by the following:

Just because $\psi$ expresses provability, doesn't mean that PA proves that $\psi$ expresses provability.

Lob's theorem implies that natural expressions of provability in PA - ones for which PA proves all the relevant basic properties - the resulting interpretation of "I am provable" is, in fact, provable.

  • $\begingroup$ That's funny. I was convinced that $H$ is false $\endgroup$ – Gabriel Nivasch Feb 8 '17 at 21:31
  • $\begingroup$ @GabrielNivasch That's quite a reasonable intuition, and your intuitive proof is totally plausible! Where it breaks down, though, is that $H$ has a purely arithmetic meaning as well. The MRDP theorem makes this clearer: it says, for example, that there is a Diophantine equation $E$ such that $E([p])$ has a solution iff $p$ is provable in PA. Similarly we can construe $H$ as an expression of the form "$\exists x[f(x)=0]$", where $f(x)$ is a Diophantine equation. Now a proof of this can consist of just an arithmetic computation; what this proof doesn't contain? Any use of the "meaning" of $H$! $\endgroup$ – Noah Schweber Feb 8 '17 at 21:37
  • $\begingroup$ So essentially, $H$ could be "accidentally" provable. And in fact, your argument shows that $H$ will be! Which is weird as heck. $\endgroup$ – Noah Schweber Feb 8 '17 at 21:38
  • $\begingroup$ Could you say a bit more about what ψ can be? Of Hilbert-Bernays conditions it should satisfy D1, and your post suggests that it does not satisfy D2 or D3. Can it be chosen to satisfy whichever one we like? $\endgroup$ – user21820 Apr 21 '18 at 9:26

Your sentence is constructed to have the property that $$ H \leftrightarrow (\mathsf{PA}\vdash H) $$ In particular, then, PA proves $$ (\mathsf{PA}\vdash H) \to H $$ This is the premise for Löb's theorem which then concludes that PA proves $H$ itself.

So $H$ is true!

  • $\begingroup$ You're saying the answer is "yes", whereas bof above says the answer is "it depends"... $\endgroup$ – Gabriel Nivasch Feb 8 '17 at 21:12
  • $\begingroup$ @GabrielNivasch See my answer; it depends exactly what properties you demand of a provability predicate. $\endgroup$ – Noah Schweber Feb 8 '17 at 21:14
  • $\begingroup$ @GabrielNivasch Sorry! I posted part of my answer before I was done writing it. My bad. $\endgroup$ – bof Feb 8 '17 at 21:21

According to the Stanford Encyclopedia of Philosophy, this question was raised by Leon Henkin in 1952:

L. Henkin, Problem, J. Symbolic Logic 17 (1952), 160.

Georg Kreisel pointed out that "this depends vitally on how provability is expressed; with different choices, one gets opposite answers":

G. Kreisel, On a problem of Henkin's, Proc. Netherlands Acad. Sci. 56 (1953), 405–406.

Martin Löb showed that, if the arithmetized provability predicate satisfies certain natural conditions, then the Henkin sentence $H$ is provable:

M. H. Löb, Solution of a problem of Leon Henkin, J. Symbolic Logic 20 (1955), 115–116.

  • $\begingroup$ I missed your edit. Given that this answer is complete, and preceded mine, should I delete my answer? $\endgroup$ – Noah Schweber Feb 8 '17 at 21:21
  • $\begingroup$ @NoahSchweber Your answer is a real answer, mine just gives references without explaining anything. Why don't you edit the references into your answer and then I can delete mine. $\endgroup$ – bof Feb 8 '17 at 21:26
  • $\begingroup$ You should somehow put all three answers together $\endgroup$ – Gabriel Nivasch Feb 9 '17 at 8:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.