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

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!
