Janos and I started working on extending the fixed point theorem to the infinite case at MIRI's June decision theory workshop with Patrick and Benja. This post attempts to exhibit the finite version of the theorem and speculates about a plausible extension.

Algorithm for the finite case

Suppose we're given variables p1,…,pn, and statements pi↔ϕi(p1,…,pn) where each ϕi is fully modalized (no variables occur outside modal subformulas). We will describe an algorithm for constructing sentences ψi with no free variables, such that the original statements are equivalent to p1↔ψ1,…,pn↔ψn.

For simplification purposes, we will assume that each ϕi is only singly modalized (none of the modal subformulas contain further modal subformulas). If not, we can introduce new variables for each subformula of the form □ϕi,j that occurs in a fully modalized context.

Now consider a sequence of theories W0,W1,…, where Wi≡PA∪{□i+1⊥,¬□i⊥}.

In W0, it's easy to determine the truth value of each pi: every modal subformula can be replaced with ⊤, leaving a propositional formula with no variables.

Now suppose we've done this for W0,…,Wn−1. Then, a statement □ϕ will be true in Wn iff

Therefore □ϕ will be true in Wn iff ϕ is true in W0,…,Wn−1; this will let us evaluate the truth value of pi in all of the theories W1,…,Wn.

It's clearly the case that every modal subformula will have truth value stabilizing, therefore every pi will also. So there is an N such that Wn has the same truth values as WN for n>N. Now if WN⊢pi, construct ψi≡¬⋁i:Wi⊢¬pi(□i+1⊥∧¬□i⊥); otherwise construct ψi≡⋁i:Wi⊢pi(□i+1⊥∧¬□i⊥). These are variable-free formulas.

Infinite case example: Procrastination Bot

def ProcrastinationBotN(X):

if PA+N⊢□X(PBN+1)=C:

return C

else: return D

Constructing the fixed point

Let pij denote whether PBi cooperates with PBj. Then
pij↔□ipj,i+1=□i□jpi+1,j+1
where □i stands for ¬□i⊥→□ (e.g. □0=□).

Then the following statements hold
p00↔□□p11p11↔□1□1p22≡¬□⊥→□(¬□⊥→□p22)…

In W0, any statement with a box in front of it is true, so any statement where a boxed statement is implied is also true. Thus, all the relevant statements are true in W0:

Theory

p00

□□p11

p11

¬□⊥→□(¬□⊥→□p22)

¬□⊥→□p22

p22

…

W0

⊤

⊤

⊤

In Wi+1, all the implied statements are boxed statements that were true in Wi, e.g. □p22 or ¬□⊥→□p22. Thus, all the relevant statements are true in Wi+1:

Theory

p00

□□p11

p11

¬□⊥→□(¬□⊥→□p22)

¬□⊥→□p22

p22

…

W0

⊤

⊤

⊤

⊤

⊤

⊤

⋮

⋮

⋮

⋮

⋮

⋮

⋮

Wi+1

⊤

⊤

⊤

Thus, any Procrastination Bot cooperates with any other Procrastination Bot.

Existence and uniqueness of the fixed point via quining

Given a formula ψ(m,n), there exists
formula ϕ(n) such that ⊢ϕ(n)↔ψ(┌ϕ┐,n).
The quine construction (thanks Benja!) is ϕ(n)≡ψ(let k=┌ψ(let k=x in subst┌x┐(quote(k),k))┐ in subst┌x┐(quote(k),k),n)

Let ψ(┌ϕ┐,n)=□┌ϕ(¯¯¯¯¯¯¯¯¯¯¯¯¯n+1)┐. Then we have
PA⊢∀n:(ϕ(n)↔□┌ϕ(¯¯¯¯¯¯¯¯¯¯¯¯¯n+1)┐).

Now consider that □┌∀n:ϕ(n)┐→□┌ϕ(¯¯¯¯¯¯¯¯¯¯¯¯¯n+1)┐. Using the above, we have
PA⊢□┌∀n:ϕ(n)┐→∀n:ϕ(n).

By Lob's theorem, PA⊢∀n:ϕ(n), so a fixed point exists.

Assume there are two fixed points ϕ and ϕ′. Then we have
PA⊢∀n:[ϕ(n)↔ψ(┌ϕ┐,n)]∧[ϕ′(n)↔ψ(┌ϕ′┐,n)],PA⊢∀┌ϕ┐,┌ϕ′┐:□┌∀n:ϕ(n)↔ϕ′(n)┐→[ψ(┌ϕ┐,n)↔ψ(┌ϕ′┐,n)]
Thus, PA⊢∀n:ϕ(n)↔ϕ′(n), so the fixed points are the same.

Janos and I started working on extending the fixed point theorem to the infinite case at MIRI's June decision theory workshop with Patrick and Benja. This post attempts to exhibit the finite version of the theorem and speculates about a plausible extension.

## Algorithm for the finite case

Suppose we're given variables p1,…,pn, and statements pi↔ϕi(p1,…,pn) where each ϕi is fully modalized (no variables occur outside modal subformulas). We will describe an algorithm for constructing sentences ψi with no free variables, such that the original statements are equivalent to p1↔ψ1,…,pn↔ψn.

For simplification purposes, we will assume that each ϕi is only singly modalized (none of the modal subformulas contain further modal subformulas). If not, we can introduce new variables for each subformula of the form □ϕi,j that occurs in a fully modalized context.

Now consider a sequence of theories W0,W1,…, where Wi≡PA∪{□i+1⊥,¬□i⊥}.

In W0, it's easy to determine the truth value of each pi: every modal subformula can be replaced with ⊤, leaving a propositional formula with no variables.

Now suppose we've done this for W0,…,Wn−1. Then, a statement □ϕ will be true in Wn iff

PA⊢(□n+1⊥∧¬□n⊥)→□ϕ⇔□n⊥∨□(□n⊥→ϕ)⇔□n⊥∨□n−1⋀i=0((□i+1⊥∧¬□i⊥)→ϕ)

Therefore □ϕ will be true in Wn iff ϕ is true in W0,…,Wn−1; this will let us evaluate the truth value of pi in all of the theories W1,…,Wn.

It's clearly the case that every modal subformula will have truth value stabilizing, therefore every pi will also. So there is an N such that Wn has the same truth values as WN for n>N. Now if WN⊢pi, construct ψi≡¬⋁i:Wi⊢¬pi(□i+1⊥∧¬□i⊥); otherwise construct ψi≡⋁i:Wi⊢pi(□i+1⊥∧¬□i⊥). These are variable-free formulas.

## Infinite case example: Procrastination Bot

def ProcrastinationBotN(X):

Constructing the fixed pointLet pij denote whether PBi cooperates with PBj. Then pij↔□ipj,i+1=□i□jpi+1,j+1 where □i stands for ¬□i⊥→□ (e.g. □0=□).

Then the following statements hold p00↔□□p11 p11↔□1□1p22≡¬□⊥→□(¬□⊥→□p22) …

In W0, any statement with a box in front of it is true, so any statement where a boxed statement is implied is also true. Thus, all the relevant statements are true in W0:

In Wi+1, all the implied statements are boxed statements that were true in Wi, e.g. □p22 or ¬□⊥→□p22. Thus, all the relevant statements are true in Wi+1:

Thus, any Procrastination Bot cooperates with any other Procrastination Bot.

Existence and uniqueness of the fixed point via quiningGiven a formula ψ(m,n), there exists formula ϕ(n) such that ⊢ϕ(n)↔ψ(┌ϕ┐,n). The quine construction (thanks Benja!) is ϕ(n)≡ψ(let k=┌ψ(let k=x in subst┌x┐(quote(k),k))┐ in subst┌x┐(quote(k),k),n)

Let ψ(┌ϕ┐,n)=□┌ϕ(¯¯¯¯¯¯¯¯¯¯¯¯¯n+1)┐. Then we have PA⊢∀n:(ϕ(n)↔□┌ϕ(¯¯¯¯¯¯¯¯¯¯¯¯¯n+1)┐).

Now consider that □┌∀n:ϕ(n)┐→□┌ϕ(¯¯¯¯¯¯¯¯¯¯¯¯¯n+1)┐. Using the above, we have PA⊢□┌∀n:ϕ(n)┐→∀n:ϕ(n).

By Lob's theorem, PA⊢∀n:ϕ(n), so a fixed point exists.

Assume there are two fixed points ϕ and ϕ′. Then we have PA⊢∀n:[ϕ(n)↔ψ(┌ϕ┐,n)]∧[ϕ′(n)↔ψ(┌ϕ′┐,n)], PA⊢∀┌ϕ┐,┌ϕ′┐:□┌∀n:ϕ(n)↔ϕ′(n)┐→[ψ(┌ϕ┐,n)↔ψ(┌ϕ′┐,n)] Thus, PA⊢∀n:ϕ(n)↔ϕ′(n), so the fixed points are the same.