= Solution
Under the arithmetical interpretation $\square A=P_S(\ulcorner A\urcorner)$, the Löb axiom says that a <formal proof> of the local reflection implication for $A$ already entails a <formal proof> of $A$:
$$
P_S(\ulcorner P_S(\ulcorner A\urcorner)\to A\urcorner)\to P_S(\ulcorner A\urcorner).
$$
It is a formalized constraint on self-verification of a <formal proof> system. Externally, <Löb's theorem> says that if the system itself proves its own local reflection implication for $A$, it proves $A$. Distribution reflects closure of <formal proofs> under implication, necessitation reflects that a theorem has an arithmetically recognizable <formal proof>, and <positive introspection> reflects <formal proof> verification inside <arithmetic>.
Taking $A$ to be a refutable <first-order sentence>, especially a <contradiction>, recovers the obstruction behind the second incompleteness theorem: a <first-order consistent> sufficiently strong system cannot prove the corresponding claim that no <formal proof> of that <first-order sentence> exists. This does not identify provability with truth, nor grant the unrestricted factivity principle $\square A\to A$ as a theorem of the system. The Löb axiom is the <characteristic> additional scheme of Gödel–Löb <provability logic>.
Back to article page
