Löb's Theorem

Löb's theorem is a result in modal logic that reveals the boundary conditions of self-trust in formal systems. It states that if a formal system S can prove that the provability of a sentence P implies the truth of P — written in modal notation as □(□P → P) — then S can already prove P itself. The theorem generalizes the reasoning behind the second incompleteness theorem: a system cannot bootstrap its own reliability from inside. It can only recognize as reliable those sentences it has already proven by other means. Incompleteness and Löb's theorem together map the closed epistemic topology of formal systems: every attempt at self-validation folds back into prior assumptions. The theorem is the central result of provability logic, the study of what formal systems can know about their own proof procedures.

Löb's theorem is the formal expression of a principle that operates far beyond logic: no system can validate its own foundations from within its own frame. The attempt to do so is not merely difficult — it is structurally self-defeating, and the self-defeat is provable.