Provability Logic

views updated

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 2^x exists. In more technical terms: T extends I Δ₀ + EXP.
T does not prove any false Σ₁ sentences.

For such theories, it is also clear that PRL is sound if we read □ as Prov_T (where Prov_T is a natural provability predicate with respect to a sufficiently simple axiomatization of 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 Δ₀ + 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.

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)

Encyclopedia of Philosophy