## Provability Logic

## Provability Logic

# PROVABILITY LOGIC

Even though "provability logic" did not come into its own until the early seventies, it has its roots in two older fields: metamathematics and modal logic. In metamathematics, we study what theories can say about themselves. The first—and most outstanding—results are Kurt Gödel's two incompleteness theorems.

If we take a sufficiently strong formal theory *T* —say, Peano arithmetic—we can use Gödel numbering to construct in a natural way a predicate *Prov(x)* in the language of *T* that expresses "*x* is the Gödel number of a sentence which is provable in *T*." About *T* we already know that it satisfies *modus ponens* :

If it is provable that *A* implies *B*, then, if *A* is provable, *B* is provable as well.

Now it turns out that, using Gödel numbering and the predicate *Prov*, we can express *modus ponens* in the language of *T*, and show that in *T* we can actually prove this formalized version of *modus ponens* :*Prov* (⌈*A* → *B* ⌉) → (*Prov* (⌈*A* ⌉) → *Prov* (⌈*B* ⌉)).

When we rephrase both the normal and the formalized version of *modus ponens* using the modal operator □, reading □*A* as "*A* is provable in *T*," we get the modal rule**(1)**

and the modal axiom**(2)** □(*A* → *B* ) → (□*A* → □*B* ).

Indeed both the rule and the axiom are well known from the basic modal logic *K*.

Similarly, we can show that if there is a proof of the sentence *A* in *T*, then *T* itself can check this proof, so *T* proves *Prov* (⌈*A* ⌉)—we shall call this principle *Prov* -completeness. Again, though in a less straightforward way than in the case of *modus ponens*, we can formalize the principle itself and see that *T* actually proves:*Prov* (⌈*A* ⌉) → *Prov* (⌈*Prov* (⌈*A* ⌉)⌉).

When we rephrase the principle of *Prov* -completeness and its formalization in modal logical terms, we get the modal rule that is usually called necessitation:**(3)** ,

and the modal axiom**(4)** □*A* → □□*A*,

which is the transitivity axiom 4 well known from modal systems such as K4 and S4.

Finally, one might wonder whether *T* proves the intuitively valid principle that "all provable sentences are true," that is, whether *T* proves *Prov* (⌈*A* ⌉) → *A*. Unexpectedly, this turns out not to be the case at all. Löb proved in 1953, using Gödel's technique of diagonalization, that *T* proves *Prov* (⌈*A* ⌉) → *A* only in the trivial case that *T* already proves *A* itself!

Löb's theorem has a formalization that can also be proved in *T*. Writing both the theorem and its formalization in modal terms, we get the modal rule**(5)** ,

and the modal axiom**(6)** □(□*A* → *A* ) → □*A*,

usually called *W* (for well-founded) by modal logicians.

Now we can define provability logic, which goes by various names in the literature—*PRL, GL* (for Gödel/Löb), *L* (for Löb), and, in modal logic texts, *KW* 4. It is generated by all the modal formulas that have the form of a tautology of propositional logic, plus the rules (1),(3),(5) and axioms (2),(4),(6) given above. One can prove that rule (5) and axiom (4) already follow from the rest, so that *PRL* is equivalently given by the well-known system *K* plus the axiom □(□*A* → *A* ) → □*A*.

The main "modal" theorem about *PRL* —but one with great arithmetical significance—is the "fixed point theorem," which D. de Jongh and G. Sambin independently proved in 1975. The theorem says essentially that "self-reference is not really necessary." Suppose that all occurrences of the propositional variable *p* in a given formula *A* are under the scope of □-es, for example, *A(p)* = ¬ □*p* or *A(p)* = □(*p* → *q* ). Then there is a formula *B* in which *p* does not appear, such that all propositional variables that occur in *B* already appear in *A(p)*, and such that *PRL* ⊦ *B* ↔ *A(B)*. This *B* is called a fixed point of *A(p)*. Moreover, the fixed point is unique, or more accurately, if there is another formula *B′* such that *PRL* ⊦ *B′* ↔ *A(B′)*, then we must have *PRL* ⊦ *B* ↔ *B′*. Most proofs of the fixed point theorem in the literature give an algorithm by which one can compute the fixed point.

For example, suppose that *A(p)* = ¬□*p*. Then the fixed point produced by the algorithm is ¬□⊥, and indeed we have *PRL* ⊦ − □⊥ ↔ − □(−□⊥). If we read this arithmetically, the direction from left to right is just the formalized version of Gödel's second incompleteness theorem. Thus, if *T* does not prove a contradiction, then it is *not* provable in *T* that *T* does not prove a contradiction.

The landmark result in provability logic is Solovay's "arithmetical completeness theorem" of 1976. This theorem says essentially that the modal logic *PRL* captures *everything* that Peano arithmetic can say in modal terms about its own provability predicate. Before formulating Solovay's theorem more precisely, we turn to the semantics of *PRL*.

Provability logic has a suitable Kripke semantics, just like many other modal logics. Unaware of the arithmetical relevance of *PRL*, Krister Segerberg proved in 1971 that it is sound and complete with respect to finite irreflexive transitive frames, and even with respect to finite trees. This completeness theorem immediately gives a decision procedure to decide for any modal formula *A* whether *A* follows from *PRL* or not. Looking at the procedure a bit more precisely, it can be shown that *PRL* is "very decidable": Like the well-known modal logics *K, T*, and *S* 4, it is decidable in PSPACE. This means that there is a Turing machine that, given a formula *A* as input, answers whether *A* follows from *PRL* ; the size of the memory that the Turing machine needs for its computations is only polynomial in the length of *A*.

The modal completeness theorem was an important first step in Solovay's proof of the arithmetical completeness of *PRL*. Suppose that *PRL* does not prove the modal formula *A*. Then there is a finite tree such that *A* is false at the root of that tree. Now Solovay devised an ingenious way to describe the tree in the language of Peano arithmetic. Thus he found a translation *f* from modal formulas to sentences of arithmetic, such that Peano arithmetic does not prove *f* (*A* ). Such a *translation f* respects the logical connectives (so, e.g., *f* (*B* ∧*C* ) = *f* (*B* ) ∧ *f* (*C* )), and □ is translated as *Prov* (so *f* (□*B* ) = *Prov* (⌈*f* (*B* )⌉)). Thus Solovay's arithmetical completeness theorem gives an alternative way to construct many nonprovable sentences. For example, we know that *PRL* does not prove □*p* ∨ □¬*p*, so by the theorem, there is an arithmetical sentence *f* (*p* ) such that Peano arithmetic does not prove *Prov* (⌈*f* (*p* )⌉) ∨ *Prov* (⌈¬*f* (*p* )⌉). In particular, if we suppose that Peano arithmetic does not prove any false sentences, this implies that neither *f* (*p* ) nor ¬*f* (*p* ) is provable in Peano arithmetic.

In recent years, logicians have investigated many other systems of arithmetic that are weaker than Peano arithmetic. They have given a partial answer to the question: "For which theories of arithmetic does Solovay's arithmetical completeness theorem still hold¿" It certainly holds for theories *T* that satisfy the following two conditions:

*T*proves induction for formulas in which all quantifiers are bounded (like the quantifier ∀*x*≤*y*+*z*) and*T*proves that for all*x*, its power 2exists. In more technical terms:^{x}*T*extends*I*Δ_{0}+*EXP*.*T*does not prove any false Σ_{1}sentences.

For such theories, it is also clear that *PRL* is sound if we read □ as *Prov _{T}* (where

*Prov*is a natural provability predicate with respect to a sufficiently simple axiomatization of

_{T}*T*). To sum up, we have the following theorem: If

*T*satisfies 1 and 2, and

*A*is a modal sentence, then

*PRL*⊦

*A*⇔ for all translations

*f,T*⊦

*f*(

*A*).

This result shows a strength of provability logic: For many different theories,

*PRL*captures exactly what those theories say about their own provability predicates. At the same time this is of course a weakness: For example, provability logic does not point to any differences between those theories that are finitely axiomatizable and those that are not.

In order to be able to speak in a modal language about such distinctions between theories, researchers have extended provability logic in many different ways, only a few of which are mentioned here. One way is to add a binary modality, ▹, where for a given theory *T*, the modal sentence *A* ▹ *B* stands for "*T* + *B* is interpretable in *T* + *A*." It appears that the interpretability logic of *I* Δ_{0} + *superexp* is different from the interpretability logic of Peano arithmetic.

Another way to extend the framework of *PRL* is to add propositional quantifiers, so that one can express principles like Goldfarb's:

∀*p* ∀*q* ∃*r* □((□*p* ∨ □*q* ) ↔ □*r* ).

Finally, one can of course study predicate provability logic. V. A. Vardanyan proved that the set of always provable sentences of predicate provability logic is not even recursively enumerable, so it has no reasonable axiomatization.

** See also ** Gödel, Kurt; Gödel's Incompleteness Theorems; Kripke, Saul; Logic, History of; Modal Logic; Peano, Giuseppe.

## Bibliography

Artemov, S. N., and L. D. Beklemishev. "On Propositional Quantifiers in Provability Logic." *Notre Dame Journal of Formal Logic* 34 (1993): 401–419.

Boolos, G. *The Logic of Provability*. New York: Cambridge University Press, 1993.

de Jongh, D. H. J., M. Jumelet, and F. Montagna. "On the Proof of Solovay's Theorem." *Studia Logica* 50 (1991): 51–70.

Smoryński, C. *Self-Reference and Modal Logic*. New York: Springer-Verlag, 1985.

Solovay, R. M. "Provability Interpretations of Modal Logic." *Israel Journal of Mathematics* 25 (1976): 287–304.

Visser, A. "Interpretability Logic." In *Mathematical Logic (Proceedings, Chaika, Bulgaria, 1988)*, edited by P. P. Petkov. New York: Plenum Press, 1990.

*Rineke Verbrugge (1996)*