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 \to □ (q \to 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., $φ (p_{1}, \dots, p_{n})$ .

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. $\neg φ$ is translated to $\neg ~ φ$ .)

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:

The soundness theorem states that if a formula $φ (p_{1}, \dots, p_{n})$ is provable in GL, then for any closed formulas $ψ_{1}, \dots, ψ_{n}$ in the language of arithmetic, $φ (ψ_{1}, \dots, ψ_{n})$ is provable in PA.
The completeness theorem is the exact converse: It states that if $φ (p_{1}, \dots, p_{n})$ is a formula of provability logic, and if for any closed formulas $ψ_{1}, \dots, ψ_{n}$ in the language of arithmetic, $φ (ψ_{1}, \dots, ψ_{n})$ is provable in PA, then $φ (p_{1}, \dots, p_{n})$ is provable in GL.

In summary: $G L ⊢ φ (p_{1}, \dots, p_{n}) ⟺ \forall ψ_{1}, \dots, ψ_{n} . P A ⊢ φ (ψ_{1}, \dots, ψ_{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 $P A ⊢ □ φ \to φ$ , then $P A ⊢ φ$ . This implies that the analogous statement holds in GL: Suppose that $G L ⊢ □ φ (p_{1}, \dots, p_{n}) \to φ (p_{1}, \dots, p_{n})$ . Then by soundness, $P A ⊢ □ φ (ψ_{1}, \dots, ψ_{n}) \to φ (ψ_{1}, \dots, ψ_{n})$ for all $ψ_{1}, \dots, ψ_{n}$ , and hence by Löb, $P A ⊢ φ (ψ_{1}, \dots, ψ_{n})$ . But by completess, this implies $G L ⊢ φ (p_{1}, \dots, p_{n})$ .

Similarly, $G L ⊢ φ (p_{1}, \dots, p_{n})$ implies $G L ⊢ □ φ (p_{1}, \dots, p_{n})$ , 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 memorize the 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 $φ (p_{1}, \dots, p_{n})$ and $φ^{'} (p_{1}, \dots, p_{n})$ equivalent, then you can substitute $φ^{'}$ for $φ$ in any other formula, even inside boxes; in other words, in this case, GL will prove that $ψ (p_{1}, \dots, p_{n}, φ (p_{1}, \dots, p_{n}))$ is equivalent to $ψ (p_{1}, \dots, p_{n}, φ^{'} (p_{1}, \dots, p_{n}))$ , for every formula $ψ (p_{1}, \dots, p_{n}, q)$ .

Fixed points

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

We say that a formula $φ (p, q_{1}, \dots, q_{n})$ is modalized in $p$ if all occurrences of $p$ in $φ (p, q_{1}, \dots, q_{n})$ are inside boxes. We say that $φ (p_{1}, \dots, p_{n})$ is fully modalized if it is modalized in each $p_{i}$ . (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 point of $F (p, q)$ in the sense that $G L ⊢ A (q) \leftrightarrow 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 $q_{1}, \dots, q_{n}$ and multiple formulas $F_{i} (p_{1}, \dots, p_{m}, q_{1}, \dots, q_{n})$ , $i = 1, \dots, m$ . In that case, we can find formulas $A_{i} (q_{1}, \dots, q_{n})$ such that for every $i$ , GL proves that $A_{i} (q_{1}, \dots, q_{n})$ is equivalent to $F_{i} (A_{1} (q_{1}, \dots, q_{n}), \dots, A_{m} (q_{1}, \dots, q_{n}), q_{1}, \dots, q_{n}) .$

Moreover, it can be shown that these fixed points are unique—not in the sense that there is only one set of formulas $A_{1}, \dots, A_{m}$ satisfying the above condition, of course (if $A_{i}$ works, so does $A_{i} \land ⊤$ : see the rule about substitution of equivalent formulas), but in the sense that if $A_{1}, \dots, A_{m}$ is a solution and $B_{1}, \dots, B_{m}$ is also a solution, then $G L ⊢ A_{i} (q_{1}, \dots, q_{n}) \leftrightarrow B_{i} (q_{1}, \dots, q_{n})$ , $i = 1, \dots, 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}, \dots, φ_{m}$ , $φ_{1}, \dots, φ_{m}$ , and $ψ_{1}, \dots, ψ_{n}$ are all closed formulas of arithmetic, such that for $i = 1, \dots, m$ , PA proves $φ_{i} \leftrightarrow F_{i} (φ_{1}, \dots, φ_{m}, ψ_{1}, \dots, ψ_{n})$ and $φ_{i}^{'} \leftrightarrow F_{i} (φ_{1}^{'}, \dots, φ_{m}^{'}, ψ_{1}, \dots, ψ_{n})$ . Then $P A ⊢ φ_{i} \leftrightarrow φ_{i}^{'}$ , for $i = 1, \dots, 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.

A primer on provability logic

The language

Soundness and completeness

Substitution of equivalent formulas

Fixed points

Decidability

Further reading