# Löb's theorem and working with connectives of two levels

I try to decipher Löb's theorem by getting rid of some of the material implications for something more intuitive and in using classical substitutions for connectives on both levels. I came up with the following

$$([\text{PA} \vdash Bew(\# P)] \rightarrow P)\implies[\text{PA} \vdash P]$$

$$\neg([\text{PA} \vdash Bew(\# P)] \land \neg P)\implies[\text{PA} \vdash P]$$

$$\text{not}\ [\text{PA} \vdash P]\implies \text{not}\ \neg ([\text{PA} \vdash Bew(\# P)] \land \neg P)$$

(Here in the first line I replace "from A follows B" by "it can't be that A, while not B" and in the second line I replace "from A follows B" by "from not B follows not A".)

Now say we consider any false sentence $P$ and assume that $\text{PA}$ can't prove it (is sound w.r.t. to $P$). Then, if the two (arguably different) $not$s do cancel, it would follow that $\text{PA} \vdash Bew(\# P)) \land \neg P$. By assumption the second term $\neg P$ is true indeed, and hence I'm left with $\text{PA}$ having a proof $Bew(\# P)$ of the false statement $P$.

What is the issue with the above deduction? I understand if dropping "$\text{not}\ \neg$" might not be okay, but then I'm still somewhat surprised by the claim which results. Also, do you guys have a formulation of the theorem with a little less implications?

I was also reading this comic on the Löb's theorem. But its sentences $s$ are written in Comic Sans, which I read as notation for $\neg s$.

edit: corrected brackets

$$[\text{PA} \vdash (Bew(\# P) \rightarrow P)]\implies[\text{PA} \vdash P]$$

$$[\text{PA} \vdash \neg(Bew(\# P) \land \neg P)]\implies[\text{PA} \vdash P]$$

$$\text{not}[\text{PA} \vdash P]\implies \text{not}[\text{PA} \vdash \neg(Bew(\# P) \land \neg P)]$$

(Still not sure what now assuming $\neg P$ plus $\text{not}[\text{PA} \vdash P]$ leads to.)

• I don't see how you've gained anything by attempting to remove all of the implication symbols. – Qiaochu Yuan Jun 6 '13 at 22:04
• @QiaochuYuan: Your point being? – Nikolaj-K Jun 6 '13 at 22:05
• We have $(A\rightarrow \bot)\vdash \neg A$. Hence in the $P=\bot$ case the theorem becomes $[\text{PA} \vdash \neg Bew(\# \bot)]\implies [\text{PA} \vdash \bot]$, which becomes $\text{not}[\text{PA} \vdash \bot]\implies\text{not}[\text{PA} \vdash \neg Bew(\# \bot)]$. This reads: Assuming $\text{PA}$ is consistent, we find that $\text{PA}$ can't prove itself to be sound. – Nikolaj-K Jun 7 '13 at 23:49

The first statement is incorrectly parenthesized. The LHS should be $\text{PA} \vdash (\text{Bew}(\#P) \to P)$. I have no idea what your comment about Comic Sans means.
If $P$ is a contradiction, then Löb's theorem says "if $\text{PA}$ proves that a proof of a contradiction would lead to a contradiction, then $\text{PA}$ proves a contradiction," or in other words, "if $\text{PA}$ proves that it is consistent, then $\text{PA}$ is inconsistent," which is just the second incompleteness theorem.