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.

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