2
$\begingroup$

Lob's theorem states that:

Let $\textbf{Prov}(n^A)$ be the arithmetic statement such that $PA\vdash$ $A$ iff $\textbf{Prov}(n^A)$, where $PA$ is peano arithmetic, and $n^A$ is the godel number of $A$. Then

$$PA \vdash\textbf{Prov}(n^A)\rightarrow A\quad\quad\text{ implies} \quad \quad PA\vdash A$$

Where the same applies to any system that is at least as powerful as peano arithmetic.

My question is: Is there an intuitive explanation of why this is true? I've read an $n$ step proof in modal logic, but my intuition is not improved by it.

$\endgroup$

closed as off-topic by Andrej Bauer, Evil, Yuval Filmus, Discrete lizard, David Richerby Jul 5 '18 at 17:09

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "This question does not appear to be about computer science, within the scope defined in the help center." – Andrej Bauer, Evil, Yuval Filmus, Discrete lizard, David Richerby
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 2
    $\begingroup$ Doesn't this belong to math.stackexchange.com? $\endgroup$ – Andrej Bauer Jun 26 '18 at 14:34