Variant of Gödel sentence

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


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.


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!