A primer on provability logic

1Benya Fallenstein

4Jaime Sevilla Molina

4Jaime Sevilla Molina

New Comment

3 comments, sorted by Click to highlight new comments since: Today at 8:17 PM

Thread for proofs of results claimed above (not limited to stuff not found in Lindström); contributions appreciated. Stuff not in Lindström includes the uniqueness of arithmetic fixed points in PA (found in the modal agents paper), and I think the version of the fixed point theorem with more than one (the latter should be provable by iterated application of the fixed point theorem for a single ).

**Generalized fixed point theorem**:

Suppose that are modal sentences such that is modalized in (possibly containing sentence letters other than ).

Then there exists in which no appears such that .

We will prove it by induction.

For the base step, we know by the fixed point theorem that there is such that

Now suppose that for we have such that .

By the second substitution theorem, . Therefore we have that .

If we iterate the replacements, we finally end up with .

Again by the fixed point theorem, there is such that .

But as before, by the second substitution theorem, .

Let stand for , and by combining the previous lines we find that .

By Goldfarb's lemma, we do not need to check the other direction, so and the proof is finished

An immediate consequence of the theorem is that for those fixed points and every , .

Indeed, since is closed under substitution, we can make the change for in the theorem to get that .

Since the righthand side is trivially a theorem of , we get the desired result.

One remark: the proof is wholly constructive. You can iterate the construction of fixed point following the procedure implied by the construction of the to compute fixed points.

**Uniqueness of arithmetic fixed points**:

*Notation*:

Let be a fixed point on of ; that is, .

Suppose is such that . Then by the first substitution theorem, for every formula . If , then , from which it follows that .

Conversely, if and are fixed points, then , so since is closed under substitution, . Since , it follows that .

(Taken from *The Logic of Provability*, by G. Boolos.)

MIRI's paper on robust cooperation in the one-shot prisoner's dilemma (by Patrick LaVictoire and others) models agents which know their opponents' source code through Gödel-Löb provability logic, a modal logic for reasoning about provability in Peano Arithmetic. This framework of "modal agents" has turned out to be a really useful way of reasoning about these agents. Vladimir Slepnev recently proposed reformulating UDT with a halting oracle in terms of provability logic as well, and I agree that this is the right tool for the job. This post is a primer on provability logic and the results about it that we've been using in our work.

## The language

Gödel-Löb provability logic ("GL") is propositional logic plus a modal operator, □, which we interpret as "provable". Formulas may contain variables which denote propositions; for example p→□(q→q) is a formula saying that if the proposition p is true, then it's provable that the proposition q implies itself. We usually write ⊤ for the proposition "true" and ⊥ for the proposition "false".

Some conventions that we've been using: Use small letters (e.g. p, q) to refer to propostional variables; use capital letters (e.g. A, B) to refer to particular formulas; use φ, ψ as metavariables ranging over formulas. (The line between "concrete formula" and "metavariable standing in for a formula" isn't hard-and-fast.) When a formula contains propositional variables, list them in parantheses when talking about the formula: e.g., φ(p1,…,pn).

The meaning of a closed formula (i.e., a formula without propositional variables) is given by a recursive translation to a sentence of Peano arithmetic: If the modal formula φ is translated to the arithmetic formula ~φ, then □φ is translated to the arithmetic formula stating "the formula ┌~φ┐ is provable in PA". (Propositional connectives are translated in the obvious way, e.g. ¬φ is translated to ¬~φ.)

In practice, instead of making this translation explicit, we just abbreviate "┌φ┐ is provable in PA" as □φ in formulas of arithmetic, and leave it to the context to disambiguate whether we're talking about a modal or an arithmetic formula. Because of this, we may sometimes write □┌φ┐ instead of □φ to emphasize the Gödel quotations in the arithmetic version of the formula.

## Soundness and completeness

The axioms and inference rules of GL can be stated in the usual style of a modal logic, but in practice, two basic results about GL provide a much more convenient way to reason about it:

soundness theoremstates that if a formula φ(p1,…,pn) is provable in GL, then for any closed formulas ψ1,…,ψn in the language of arithmetic, φ(ψ1,…,ψn) is provable in PA.completeness theoremis the exact converse: It states that if φ(p1,…,pn) is a formula of provability logic, and if for any closed formulas ψ1,…,ψn in the language of arithmetic, φ(ψ1,…,ψn) is provable in PA, then φ(p1,…,pn) is provable in GL.In summary: GL⊢φ(p1,…,pn)⟺∀ψ1,…,ψn.PA⊢φ(ψ1,…,ψn).

This means that we can argue that something is provable in GL by arguing that the analogous thing is provable in PA. For example, Löb's theorem states that if PA⊢□φ→φ, then PA⊢φ. This implies that the analogous statement holds in GL: Suppose that GL⊢□φ(p1,…,pn)→φ(p1,…,pn). Then by soundness, PA⊢□φ(ψ1,…,ψn)→φ(ψ1,…,ψn) for all ψ1,…,ψn, and hence by Löb, PA⊢φ(ψ1,…,ψn). But by completess, this implies GL⊢φ(p1,…,pn).

Similarly, GL⊢φ(p1,…,pn) implies GL⊢□φ(p1,…,pn), again because the analogous statement holds about PA.

As a matter of fact, both of these happen to be an inference rules of GL. But the point is that you don't need to

memorizethe axioms and inference rules of GL in order to use it; it's sufficient to know about its soundness and completeness.## Substitution of equivalent formulas

Despite the above, there is one important result about GL that is not obvious from soundness and completeness: If GL proves two formulas φ(p1,…,pn) and φ′(p1,…,pn) equivalent, then you can substitute φ′ for φ in any other formula, even inside boxes; in other words, in this case, GL will prove that ψ(p1,…,pn,φ(p1,…,pn)) is equivalent to ψ(p1,…,pn,φ′(p1,…,pn)), for every formula ψ(p1,…,pn,q).

## Fixed points

The other really important results about GL are the existence and uniqueness of fixed points.

We say that a formula φ(p,q1,…,qn) is

modalized in pif all occurrences of p in φ(p,q1,…,qn) are inside boxes. We say that φ(p1,…,pn) isfully modalizedif it is modalized in each pi. (We don't need the latter notion in the rest of this post, but it's frequently used in applications.)Suppose that F(p,q) is modalized in p. Then there is a formula A(q) which is a

fixed pointof F(p,q) in the sense that GL⊢A(q)↔F(A(q),q). Moreover, there's a computer program that computes A(q) given F(p,q); and if q is modalized in F(p,q), then it is modalized in A(q) as well.More generally, this holds for multiple parameters q1,…,qn and multiple formulas Fi(p1,…,pm,q1,…,qn), i=1,…,m. In that case, we can find formulas Ai(q1,…,qn) such that for every i, GL proves that Ai(q1,…,qn) is equivalent to Fi(A1(q1,…,qn),…,Am(q1,…,qn),q1,…,qn).

Moreover, it can be shown that these fixed points are

unique---not in the sense that there is only one set of formulas A1,…,Am satisfying the above condition, of course (if Ai works, so does Ai∧⊤: see the rule about substitution of equivalent formulas), but in the sense that if A1,…,Am is a solution and B1,…,Bm is also a solution, then GL⊢Ai(q1,…,qn)↔Bi(q1,…,qn), i=1,…,m.This is true not only about solutions that can be written in the language of provability logic, but for any solution in the language of arithmetic: Suppose that φ1,…,φm, φ1,…,φm, and ψ1,…,ψn are all closed formulas of arithmetic, such that for i=1,…,m, PA proves φi↔Fi(φ1,…,φm,ψ1,…,ψn) and φ′i↔Fi(φ′1,…,φ′m,ψ1,…,ψn). Then PA⊢φi↔φ′i, for i=1,…,m.

## Decidability

Provability in GL turns out to be decidable, though it's PSPACE-complete, which sounds pretty bad, but perhaps the formulas we're interested in are mostly so short that it doesn't matter---I don't know. In the case of modal agents, Mihaly and Marcello wrote program which computes what two such agents do against each other, and it was efficient enough that we were able to use it to verify the examples in the paper. I don't know whether the techniques would generalize to the application to UDT.

## Further reading

If you want to go dig deeper, you may want to consult the Stanford Encyclopedia of Philosophy entry on provability logic or Per Lindström's excellent article "Provability logic---a short introduction" (

Theoria, 62(1-2):19--61, 1996). Gated copy.Some of the results claimed here aren't in Lindström, though they follow straight-forwardly from what is there; I'll later add the proofs in comments. In the meantime, some of the additional stuff can be found in the modal agents paper.