Löb's theorem

In mathematical logic, Löb's theorem states that in any formal system F with Peano arithmetic (PA), for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F. More formally, if Bew(#P) means that the formula P with Gödel number #P is provable (from the German "beweisbar"), then

or

An immediate corollary of Löb's theorem is that, if P is not provable in PA, then "if P is provable in PA, then P is true" is not provable in PA. For example, "If ${\displaystyle 1+1=3}$ is provable in PA, then ${\displaystyle 1+1=3}$" is not provable in PA.

Löb's theorem is named for Martin Hugo Löb, who formulated it in 1955.

Provability logic abstracts away from the details of encodings used in Gödel's incompleteness theorems by expressing the provability of ${\displaystyle \phi }$ in the given system in the language of modal logic, by means of the modality ${\displaystyle \Box \phi }$.

...
Wikipedia