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.)
 A: 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!
A: 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.

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