Provability Logic and Löb's Theorem

Truth is not definable in arithmetic. Provability is, and the incompleteness proof leaned on the fact throughout. That leaves a predicate of the language of arithmetic, holding of exactly the codes of the theorems of Peano arithmetic, sitting inside the theory it describes, and the question of this article is what that predicate obeys.

The answer is not a loose analogy with necessity. It is a particular modal system, identified exactly, and the theorem saying it is the right one is one of the more satisfying results in the subject.

The predicate behaves like an operator

Write $\Box A$ for the arithmetical sentence saying that $A$ is provable in Peano arithmetic. The abbreviation is doing real work and hiding none: behind it is a formula with a free variable applied to a numeral coding $A$, and everything below could be written out in the language of arithmetic at the cost of legibility.

Three facts about this predicate were isolated by Hilbert and Bernays and sharpened by Löb, and they are what the second incompleteness theorem needs.

The first says the theory recognises its own proofs: when a derivation exists, the arithmetised statement that it exists is itself derivable, because the verification that a particular finite object is a derivation is a computation the theory can carry out. The second says the theory knows that its own derivations close under modus ponens. The third is the first condition internalised, and it is by a distance the most laborious to establish, since it requires formalising inside arithmetic the argument that any provable sentence has a provable provability statement.

Anyone who has seen a modal system will recognise the shape. The first condition is the rule of necessitation, the second is the distribution axiom $\mathsf{K}$, and the third is the axiom $\mathsf{4}$. So the logic of this predicate contains the normal modal logic $\mathsf{K4}$, and the question becomes what else it contains.

The axiom that is missing

The obvious candidate for a further axiom is the one every system of necessity has: $\Box A \rightarrow A$, provable things are true. It is the characteristic axiom of system T and it is in system S4 alongside the $\mathsf{4}$ axiom already present, so if provability behaved like necessity in the familiar way, S4 would be the answer.

It is true that everything Peano arithmetic proves is true. What fails is that Peano arithmetic can prove this about itself, and the failure is total rather than partial.

The theorem answers a question Henkin raised in 1952. Gödel's sentence says of itself that it is unprovable and turns out to be unprovable and true. Henkin asked about the opposite construction: a sentence saying of itself that it is provable. Is it provable, or not? The diagonal lemma delivers such a sentence and gives no obvious verdict, since both answers look consistent at first inspection. Löb settled it in 1955, and the sentence is provable, as a special case of a general theorem far more useful than the question that prompted it.

The proof is a diagonal argument with one moving part. Suppose Peano arithmetic proves $\Box A \rightarrow A$. Apply the diagonal lemma to obtain a sentence $\psi$ for which the theory proves $\psi \leftrightarrow (\Box \psi \rightarrow A)$. From $\psi$ and the derivability conditions, the theory can derive $\Box \psi \rightarrow \Box(\Box \psi \rightarrow A)$, hence $\Box \psi \rightarrow (\Box \Box \psi \rightarrow \Box A)$, and since $\Box \psi \rightarrow \Box \Box \psi$ is the third condition, $\Box \psi \rightarrow \Box A$. Chaining with the assumed reflection gives $\Box \psi \rightarrow A$, which is $\psi$. So $\psi$ is proved outright, so $\Box \psi$ is proved, and $A$ follows.

Set $A$ to a contradiction and the second incompleteness theorem falls out in a line. The consistency statement is $\neg \Box \bot$, which is $\Box \bot \rightarrow \bot$, an instance of reflection. If the theory proved it, Löb's theorem would hand over $\bot$. A consistent theory therefore does not prove its own consistency, and the usual construction of a Gödel sentence is not needed to see it.

The system

Löb's theorem is a fact about Peano arithmetic. Formalised inside it, the theorem becomes an axiom.

The axiom is the internalised form of Löb's theorem, with the outer assertion of provability replacing the metatheoretic claim that the theory proves something. A first surprise is that the $\mathsf{4}$ axiom, which the third derivability condition supplied and which looked indispensable, is derivable from the Löb axiom in $\mathsf{K}$ and need not be assumed.

A second is what happens on frames.

Irreflexivity is the striking part. In every familiar modal system the accessibility relation is reflexive, because that is what makes necessity entail truth. Here no world sees itself, which is the frame-level image of the fact that a theory does not have access to its own soundness. The absence of infinite ascending chains is well-foundedness in the other direction, and it is what makes the Löb axiom valid: if there were an endless chain of worlds each accessible from the last, one could falsify the axiom along it.

That condition is not expressible by any first-order condition on frames, which has a consequence worth recording: $\mathsf{GL}$ is not canonical, and the standard completeness proof by canonical models does not apply to it. Completeness holds anyway, by way of finite models. Segerberg proved in 1971 that $\mathsf{GL}$ is exactly the logic of finite transitive irreflexive frames, and since the system has the finite model property and is finitely axiomatised, it is decidable. Whether a modal principle about provability holds can be settled by a machine.

Arithmetical completeness

The system matches the derivability conditions and the Löb axiom, which is encouraging but not conclusive. Some further principle about provability might hold in arithmetic and not be derivable in $\mathsf{GL}$. Ruling that out requires making the question precise.

One direction is the work already done: each axiom of $\mathsf{GL}$ interprets into something Peano arithmetic proves. The other direction is Solovay's, and it is the substantial half. Given a modal formula not derivable in $\mathsf{GL}$, there is a finite frame falsifying it, and Solovay's technique embeds that frame into arithmetic by constructing a sentence that describes a computation walking through the frame's worlds. The construction yields an assignment under which the formula's interpretation is not provable.

The result deserves to be read slowly, because it says more than that the system is adequate. Every principle of provability expressible in the modal language, whether or not anyone has thought of it, is a consequence of the Löb axiom and the rules of $\mathsf{K}$. The self-referential apparatus of the incompleteness theorems, which looks open-ended and full of scope for ingenuity, is captured completely by one schema. And since $\mathsf{GL}$ is decidable, so is the question of which such principles hold.

Solovay proved a companion result in the same paper. Ask not which modal formulas interpret into theorems of arithmetic but which interpret into truths, and the answer is a different and slightly larger system, the closure of $\mathsf{GL}$ under a reflection rule. The distinction between what arithmetic proves about its own provability and what is true about it is itself exactly axiomatisable.

Next

The last three articles have taken the internal perspective, asking what arithmetic can say about itself. The next takes the external one. Compactness forces models of arithmetic other than the intended one, and the first incompleteness theorem forces models satisfying sentences the natural numbers falsify. The question is what these structures look like, and the answer is more definite than one might expect, right up to the point where a theorem says no such model can ever be exhibited.