13 Provability Logic

The language of propositional modal logic has been used to shed further light on the logic of provability and Gödel’s incompleteness theorems.

Arithmetic

The subject matter of arithmetic is the structure of the natural numbers with the usual order and the operations of addition and multiplication. The language of arithmetic is a first-order language with a constant symbol $0$ for zero, a function symbol $S$ for the successor operation, and two binary functional symbols $+$ and $\times$ for addition and multiplication, respectively. A numeral consists of either $0$ or finite applications of $S$ to $0$ , e.g., the numeral for zero is $0$ , the numeral for two is $S S 0$ , and the numeral for five is $S S S S S 0$ .

We may take for granted a recursive axiomatization of arithmetic such as Robinson’s Arithmetic. One group of axioms makes sure that zero is no successor and that successor is a one-one operation. $\begin{array}{lll} Q 1 & \forall x \neg S x = 0 \\ Q 2 & \forall x \forall y (S x = S y \to x = y) \end{array}$ The second group of axioms governs the behavior of addition and multiplication: $\begin{array}{lll} Q 3 & \forall x (x + 0) = x \\ Q 4 & \forall x \forall y (x + S y) = S (x + y) \\ Q 5 & \forall x (x \times 0) = 0 \\ Q 6 & \forall x \forall y (x \times S y) = (x \times y) + x \end{array}$ There is a final group of axioms on the structure of the less than relation on the natural numbers: $\begin{array}{lll} Q 7 & \forall x \neg x < 0 \\ Q 8 & \forall x \forall y (x < S y \to (x < y \lor x = y)) \\ Q 9 & \forall x \forall y (x < y \lor x = y \lor y < x) \end{array}$ The axioms of Robinson’s Arithmetic are true in the natural number structure: $(N, <, +, \times, S, 0)$ A proof of a formula $φ$ of the language of arithmetic in $Q$ is a finite sequence of formulas each of which is either an axiom of $Q$ or derivable from earlier formulas in first-order logic. A formula $φ$ is a theorem of $Q$ , written $⊢_{Q} φ$ , if there is a proof of $φ$ in $Q$ .

We say that Robinson’s Arithmetic is sound with respect to the natural number structure to mean that every theorem of Robinson’s Arithmetic is true in the natural number structure. In symbols: $If ⊢_{Q} φ, then (N, <, +, \times, S, 0) ⊩ φ$

Kurt Gödel famously established that we do not have the converse — or, more carefully, we do not have the converse if $Q$ is a consistent theory. More generally, if $T$ is a recursively axiomatizable theory, then if $T$ is consistent, then there are sentences of the language of arithmetic which are true in $(N, <, +, \times, S, 0)$ but are not theorems of $T$ .

He explained how to use natural numbers to encode formulas of the language of arithmetic and arithmetical formulas to encode syntactic facts. More generally, he found a way to encode syntactic facts by means of arithmetical sentences. To each sentence $φ$ of the language, he assigned a natural number $⌜ φ ⌝$ as a code, and he managed to define an arithmetical formula $P r o v_{Q} (⌜ φ ⌝)$ to encode the fact that $φ$ is a theorem of the system $Q$ .

The provability predicate for a system like $Q$ is governed by three conditions known as the Hilbert-Bernays provability conditions:

If $⊢_{Q} φ$ , then $⊢_{Q} P r o v_{Q} (⌜ φ ⌝)$
If $⊢_{Q} P r o v_{Q} (⌜ φ \to ψ ⌝)$ , then if $⊢_{Q} P r o v_{Q} (⌜ φ ⌝)$ , then $⊢_{Q} P r o v_{Q} (⌜ ψ ⌝)$
If $⊢_{Q} P r o v_{Q} (⌜ φ ⌝)$ , then $⊢_{Q} P r o v_{Q} (⌜ P r o v_{Q} (⌜ φ ⌝) ⌝)$

If these conditions look familiar, it is because they are; they are completely parallel the rule of necessitation and axioms $K$ and $4$ .

What Gödel noticed is that a framework such as Robinson’s Arithmetic provides the resources to build a self-referential arithmetical formula $G$ such that:

$⊢_{Q} G \leftrightarrow \neg P r o v_{Q} (⌜ G ⌝) .$ He used that formula to prove his celebrated first incompleteness theorem, since he argued that unless $Q$ is inconsistent, $⊬_{Q} G$ , which is exactly what $G$ says.77 Why? On the one hand, by condition I, if $⊢_{Q} G$ , then $⊢_{G} P r o v_{Q} (⌜ G ⌝)$ . But on the other hand, if $⊢_{Q} G$ , then since $⊢_{Q} G \leftrightarrow \neg P r o v_{Q} (⌜ G ⌝)$ , given the provability conditions I and II, $⊢_{G} \neg P r o v_{Q} (⌜ G ⌝)$ , which would make $Q$ inconsistent.

Before we introduce the modal logic of provability, we should note that there is an important further condition on provability from a recursively axiomatizable system isolated by Martin Löb in response to a question by Leon Henkin. Henkin had been interested in the status of certain self-referential formula $H$ for which: $⊢_{Q} H \leftrightarrow P r o v_{Q} (⌜ H ⌝)$

Löb proved, in particular, that $Q$ proves the conditional $P r o v_{Q} (⌜ H ⌝) \to H$ only if $H$ is in fact a theorem of the system. More generally, if T is, as usual, a recursively axiomatizable arithmetical theory, then:

If $⊢_{T} P r o v_{T} (⌜ φ ⌝) \to φ$ , then $⊢_{T} φ$ .

This is Löb’s theorem for which there is a further formalization in the language of arithmetic:

$⊢_{T} (P r o v_{T} (⌜ P r o v_{T} (⌜ φ ⌝) \to φ ⌝) \to P r o v_{T} (⌜ φ ⌝)) .$ This is the formalized Löb’s theorem.

Provability

We will now consider an interpretation of $◻$ as “it is a theorem of first-order theory $T$ ”. To flesh out the interpretation of the language of propositional modal logic, we define a realization function as an assignment $α$ of formulas of arithmetic to propositional variables of propositional modal logic. That is, for each propositional variable $p$ , $α (p)$ is a formula of the language of arithmetic. This, in turn, determines a translation from the language of propositional modal logic into the language of arithmetic. The translation $φ^{⋆}$ of a modal formula $φ$ under a realization $α$ is defined inductively:

$\begin{array}{lll} p^{⋆} & = & α (p) \\ (\neg φ)^{⋆} & = & \neg φ^{⋆} \\ (φ \to ψ)^{⋆} & = & φ^{⋆} \to ψ^{⋆} \\ (◻ φ)^{⋆} & = & P r o v_{T} (⌜ φ^{⋆} ⌝) \end{array}$ We are now in a position to verify the axioms of $K 4$ for this interpretation of $◻$ . The rule of necessitation corresponds to the first Hilbert-Bernays derivability condition whereas $K$ corresponds to the second derivability condition. Finally, the third derivability condition is the translation of axiom $4$ .

$K 4$ is still too weak to encode the logic of provability, since we want to be able to deliver the formalized Löb’s theorem: $⊢_{T} (P r o v_{T} (⌜ P r o v_{T} (⌜ φ ⌝) \to φ ⌝) \to P r o v_{T} (⌜ φ ⌝)) .$ This brings us to the characteristic axiom of the modal logic of provability: $\begin{matrix} (L) & ◻ (◻ φ \to φ) \to ◻ φ . \end{matrix}$ The modal logic $G L$ (for Gödel and Löb) is the normal modal logic, which extends $K$ with all substitution instances of axiom $L$ .

One important observation at this point is that on pain of inconsistency, GL cannot in general extend KT.

Proposition 13.1 GL does not extend KT

Proof. $G L$ is closed under necessitation. So, $⊢_{G L} ◻ ⊥ \to ⊥$ only if $⊢_{G L} ◻ (◻ ⊥ \to ⊥)$ and $⊢_{G L} ◻ ⊥$ . It follows that if $⊢_{G L} ◻ ⊥ \to ⊥$ , then it must be the case that $⊢_{G L} ⊥$ . Since $⊬_{G L} ⊥$ , we conclude that $⊬_{G L} ◻ ⊥ \to ⊥$ .

This is a modal counterpart of the fact that a recursively axiomatizable consistent theory $T$ cannot even prove the arithmetical formula $P r o v_{T} (⌜ 0 = 1 ⌝) \to 0 = 1$ on account of Löb’s theorem.

Proposition 13.2 GL extends K4

Proof. That is because $⊢_{G L} ◻ p \to ◻ ◻ p$ .

The key to this proof is to substitute $◻ p \land p$ for $p$ in $L$ :

$◻ (◻ (◻ p \land p) \to (◻ p \land p)) \to ◻ (◻ p \land p)$ The antecedent of that conditional follows from $◻ p$ alone: $⊢_{K} ◻ p \to ◻ (◻ (◻ p \land p) \to (◻ p \land p))$ Here is a justification for that fact: $\begin{array}{lllll} 1 & (◻ p \land p) \to p & PL \\ 2 & ◻ (◻ p \land p) \to ◻ p & RK 1 \\ 3 & p \to (◻ (◻ p \land p) \to (◻ p \land p)) & PL 2 \\ 4 & ◻ p \to ◻ (◻ (◻ p \land p) \to (◻ p \land p)) & RK 3 \end{array}$ So, it follows that $⊢_{G L} ◻ p \to ◻ (◻ p \land p)$ and $⊢_{G L} ◻ p \to ◻ ◻ p$

Part of the interest of the modal logic of provability is that it casts some light upon Gödel’s incompleteness theorems.

Proposition 13.3 If $⊢_{G L} p \leftrightarrow \neg ◻ p$ , then $⊢_{G L} \neg ◻ ⊥ \to \neg ◻ p$ .

Given a realization $α$ for which $α (p)$ is the Gödel formula, $⊢_{G L} p \leftrightarrow \neg ◻ p$ would correspond to the fact that $⊢_{Q} G \leftrightarrow \neg P r o v_{Q} (⌜ G ⌝)$ . On the other hand, $\neg ◻ ⊥$ corresponds to $\neg P r o v_{Q} (⌜ 0 = 1 ⌝)$ . Now:

Proof. We argue as follows: $\begin{array}{lllll} 1 & p \leftrightarrow \neg ◻ p \\ 2 & ◻ p \to \neg p & PL 1 \\ 3 & ◻ ◻ p \to ◻ \neg p & RK 2 \\ 4 & ◻ p \to ◻ ◻ p & 4 \\ 5 & ◻ p \to ◻ \neg p & PL 3, 4 \\ 6 & ◻ p \to (◻ \neg p \land ◻ p) & PL 5 \\ 7 & (◻ \neg p \land ◻ p) \to ◻ (\neg p \land p) & K \\ 8 & ◻ p \to ◻ (\neg p \land p) & PL 6, 7 \\ 9 & ◻ p \to ◻ ⊥ & PL 8 \\ 10 & \neg ◻ ⊥ \to \neg ◻ p & PL 9 \end{array}$

Proposition 13.4 $⊢_{G L} \neg ◻ ⊥ \to \neg ◻ \neg ◻ ⊥$ .

This corresponds to the fact that if $T$ is consistent, then $T$ does not prove its own consistency.

Proof. We argue as follows: $\begin{array}{lllll} 1 & \neg ◻ ⊥ \to (◻ ⊥ \to ⊥) & PL \\ 2 & ◻ \neg ◻ ⊥ \to ◻ (◻ ⊥ \to ⊥) & RK 1 \\ 3 & ◻ (◻ ⊥ \to ⊥) \to ◻ ⊥ & L \\ 4 & ◻ \neg ◻ ⊥ \to ◻ ⊥ & PL 2, 3 \\ 5 & \neg ◻ ⊥ \to \neg ◻ \neg ◻ ⊥ & PL 4 \end{array}$

Definition 13.1 (Converse Well-Founded) A binary relation $R$ on a set $W$ is converse well-founded if, and only if, for every non-empty subset $X$ of $W$ , there is a greatest $R$ -member of $X$ , that is, there is some $w \in X$ such that for every $x \in X$ , $\neg R w x$ . In other words, $R$ is converse well-founded on $W$ if there are no infinite ascending $R$ -chains of the form $x_{1} R x_{2} R x_{3} \dots$ .

Notice that a relation $R$ is converse well-founded on $W$ only if it is irreflexive and asymmetric on $W$ .

Proposition 13.5 All theorems of $G L$ are valid in all transitive and converse well-founded frames.

Proof. All axioms of $G L$ are valid in all transtive and converse well-founded frames. That is because $◻ (◻ p \to p) \to ◻ p$ modally defines the class of transtive converse well-founded frames — as observed in proposition 6.3 above.

Proposition 13.6 $G L$ is complete with respect to the class of transitive and converse well-founded frames.

The argument for completeness is more elaborate than usual, since there is no reason to expect the canonical model for $G L$ to be irreflexive, which means that we cannot prove that the canonical model for $G L$ is converse well-founded.