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

  • $\begingroup$ I don't see how you've gained anything by attempting to remove all of the implication symbols. $\endgroup$ – Qiaochu Yuan Jun 6 '13 at 22:04
  • $\begingroup$ @QiaochuYuan: Your point being? $\endgroup$ – Nikolaj-K Jun 6 '13 at 22:05
  • $\begingroup$ 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. $\endgroup$ – 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.

  • $\begingroup$ Okay thanks, makes sense. I'll leave this open a bit and if nothing we comes in I'll accept this answer. Although I still have issues with it. Regarding Comic Sans, this is a short review on its history and it's response. On a related note, I recommend the movie Helvetica. $\endgroup$ – Nikolaj-K Jun 6 '13 at 21:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.