2

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

Nikolaj-K
  • 12,249
  • I don't see how you've gained anything by attempting to remove all of the implication symbols. – Qiaochu Yuan Jun 06 '13 at 22:04
  • @QiaochuYuan: Your point being? – Nikolaj-K Jun 06 '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 07 '13 at 23:49

1 Answers1

1

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.

Qiaochu Yuan
  • 419,620
  • 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. – Nikolaj-K Jun 06 '13 at 21:58