# Why, intuitively, is Lob's theorem true? [closed]

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.

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