Löb's theorem
In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula P, if it is provable in PA that "if P is provable in PA then P is true", then P is provable in PA. If Prov(P) is the assertion that the formula P is provable in PA, we may express this more formally as If P A ⊢ P r o v ( P ) → P {\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} (P)\rightarrow P}} then P A ⊢ P {\displaystyle {\mathit {PA}}\vdash P} . An immediate corollary (the contrapositive) 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 1 + 1 = 3 {\displaystyle 1+1=3} is provable in PA, then 1 + 1 = 3 {\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.