The fixed point theorem of provability logic is a key result that gives a explicit procedure to find equivalences for sentences such as the ones produced by the diagonal lemma.

In its most simple formulation, it states that:

Let \(\phi(p)\) be a modal sentence modalized in \(p\). Then there exists a letterless \(H\) such that \(GL\vdash \boxdot[p\leftrightarrow \phi(p)] \leftrightarrow \boxdot[p\leftrightarrow H]\) noteNotation: \(\boxdot A = A\wedge \square A\).

This result can be generalized for cases in which letter sentences other than \(p\) appear in the original formula, and the case where multiple formulas are present.

Fixed points

The \(H\) that appears in the statement of the theorem is called a fixed point of \(\phi(p)\) on \(p\).

In general, a fixed point of a formula \(\psi(p, q_1...,q_n)\) on \(p\) will be a modal formula \(H(q_1,...,q_n)\) in which \(p\) does not appear such that \(GL\vdash \boxdot[p\leftrightarrow\psi(p, q_1,...,q_n)] \leftrightarrow \boxdot[p_i\leftrightarrow H(q_1,...,q_n)]\).

The fixed point theorem gives a sufficient condition for the existence of fixed points, namely that \(\psi\) is modalized in \(\psi\). It is an open problem to determine a necessary condition for the existence of fixed points.

Fixed points satisfy some important properties:

If \(H\) is a fixed point of \(\phi\) on \(p\), then \(GL\vdash H(q_1,...,q_n)\leftrightarrow \phi(H(q_1,...,q_n),q_1,...,q_n)\). This coincides with our intuition of what a fixed point is, since this can be seen as an argument that when fed to \(\phi\) it returns something equivalent to itself.

But trivially \(GL\vdash \boxdot[H(q_1,...,q_n)\leftrightarrow H(q_1,...,q_n)\), so \(GL\vdash \boxdot[H(q_1,...,q_n)\leftrightarrow\psi(H(q_1,...,q_n), q_1,...,q_n)]\). <div><div>

\(H\) and \(I\) are fixed points of \(\phi\) if and only if \(GL\vdash H\leftrightarrow I\). This is knows as the uniqueness of fixed points.

Suppose \(I\) is such that \(GL\vdash H\leftrightarrow I\). Then by the first substitution theorem, \(GL\vdash F(I)\leftrightarrow F(H)\) for every formula \(F(q)\). If \(F(q)=\boxdot(p\leftrightarrow q)\), then \(GL\vdash \boxdot(p\leftrightarrow H)\leftrightarrow \boxdot(p\leftrightarrow I)\), from which it follows that \(GL\vdash \boxdot(p\leftrightarrow \phi(p))\leftrightarrow (p\leftrightarrow I)\).

Conversely, if \(H\) and \(I\) are fixed points, then \(GL\vdash \boxdot (p\leftrightarrow H)\leftrightarrow \boxdot (p\leftrightarrow I)\), so since \(GL\) is closed under substitution, \(GL\vdash\boxdot (H\leftrightarrow H)\leftrightarrow \boxdot (H\leftrightarrow I)\). Since \(GL\vdash \boxdot (H\leftrightarrow H)\), it follows that \(GL\vdash (H\leftrightarrow I)\). <div><div>

Special case fixed point theorem

The special case of the fixed point theorem is what we stated at the beginning of the page. Namely:

Let \(\phi(p)\) be a modal sentence modalized in p. Then there exists a letterless \(H\) such that \(GL\vdash \boxdot[p\leftrightarrow \phi(p)] \leftrightarrow \boxdot[p\leftrightarrow H]\).

There is a nice semantical procedure based on Kripke models that allows to compute \(H\) as a truth functional compound of sentences \(\square^n \bot\) note$\square^n A = \underbrace{\square,\square,\ldots,\square}_{n\text{-times}} A$ . (ie, \(H\) is in normal form).

$A$-traces

Let \(A\) be a modal sentence modalized in \(p\) in which no other sentence letter appears (we call such a sentence a \(p\)-sentence). We want to calculate \(A\)’s fixed point on \(p\). This procedure bears a resemblance to the trace method for evaluating letterless modal sentences.

We are going to introduce the notion of the \(A\)-trace of a \(p\)-sentence \(B\), notated by \([[B]]_A\). The \(A\)-trace maps modal sentences to sets of natural numbers, and is defined recursively as follows:

• \([[\bot]]_A = \emptyset\)

• \([[B\to C]]_A = (\mathbb{N} \setminus [[B]]_A)\cup [[C]]_A\)

• \([[\square D]]_A=\{m:\forall i < m i\in [[D]]_A\}\)

• \([[p]]_A=[[A]]_A\)

Lemma: Let \(M\) be a finite, transitive and irreflexive Kripke model in which \((p\leftrightarrow A) is valid, and \)B$ a \(p\)-sentence. Then \(M,w\models B\) iff \(\rho(w)\in [[B]]_A\).

Lemma: The \(A\)-trace of a \(p\)-sentence \(B\) is either finite or cofinite, and furthermore either it has less than \(n\) elements or lacks less than \(n\) elements, where \(n\) is the number of \(\square\)s in \(A\).

Those two lemmas allow us to express the truth value of \(A\) in terms of world ranks for models in which \(p\leftrightarrow A\) is valid. Then the fixed point \(H\) will be either the union or the negation of the union of a finite number of sentences \(\square^{n+1}\bot\wedge \square^n \bot\) noteSuch a sentence is only true in worlds of rank \(n\)

In the following section we work through an example, and demonstrate how can we easily compute those fixed points using a Kripke chain.

Applications

For an example, we will compute the fixed point for the modal Gödel sentence \(p\leftrightarrow \neg\square p\) and analyze its significance.

We start by examining the truth value of \(\neg\square p\) in the \(0\)th rank worlds. Since the only letter is \(p\) and it is modalized, this can be done without problem (remember that \(\square B\) is always true in the rank \(0\) worlds, no mater what \(B\) is). Now we apply to \(p\) the constraint of having the same truth value as \(\neg\square p\).

We iterate the procedure for the next world ranks.

Since there is only one \(\square\) in the formula, the chain is guaranteed to stabilize in the first world and there is no need for going further. We have shown the truth values in world \(2\) to show that this is indeed the case.

From the table we have just constructed it becomes evident that \([[p]]_{\neg\square p} = \mathbb{N}\setminus \{0\}\). Thus \(H = \square^{0+1}\bot \wedge \square^0\bot = \neg\square\bot\).

Therefore, \(GL\vdash \square [p\leftrightarrow \neg\square p]\leftrightarrow \square[p\leftrightarrow \neg\square \bot]\). Thus, the fixed point for the modal Gödel sentence is the consistency of arithmetic!

By employing the arithmetical soundness of GL, we can translate this result to \(PA\) and show that \(PA\vdash \square_{PA} [G\leftrightarrow \neg\square_{PA} G]\leftrightarrow \square_{PA}[G\leftrightarrow \neg\square_{PA} \bot]\) for every sentence \(G\) of arithmetic.

Since in \(PA\) we can construct \(G\) by the diagonal lemma such that \(PA\vdash G\leftrightarrow \neg\square_{PA} G\), by necessitation we have that for such a \(G\) then \(PA\vdash \square_PA[ G\leftrightarrow \neg\square_{PA} G]\). By the theorem we just proved using the fixed point, then \(PA\vdash \square_{PA}[G\leftrightarrow \neg\square_{PA} \bot]\). SInce everything \(PA\) proves is true then \(PA\vdash G\leftrightarrow \neg\square_{PA} \bot\).

Surprisingly enough, the Gödel sentence is equivalent to the consistency of arithmetic! This makes more evident that \(G\) is not provable unless \(PA\) is inconsistent, and that it is not disprovable unless it is \(\omega\)-inconsistent.

Exercise: Find the fixed point for the Henkin sentence \(H\leftrightarrow\square H\).

General case

The first generalization we make to the theorem is allowing the appearance of sentence letters other than the one we are fixing. The concrete statement is as follows:

Let \(\phi(p, q_1,...,q_n)\) be a modal sentence modalized in p. Then \(\phi\) has a fixed point on \(p\).%%.

There are several constructive procedures for finding the fixed point in the general case.

One particularly simple procedure is based on k-decomposition.

K-decomposition

Let \(\phi\) be as in the hypothesis of the fixed point theorem. Then we can express \(\phi\) as \(B(\square D_1(p), ..., \square D_{k}(p))\), since every \(p\) occurs within the scope of a \(\square\) (The \(q_i\)s are omitted for simplicity, but they may appear scattered between \(B\) and the \(D_i\)s). This is called a \(k\)-decomposition of \(\phi\).

If \(\phi\) is \(0\)-decomposable, then it is already a fixed point, since \(p\) does not appear.

Otherwise, consider \(B_i = B(\square D_1(p), ..., \square D_{i-1}(p),\top, \square D_{i+1}(p),...,\square D_k(p))\), which is \(k-1\)-decomposable.

Assuming that the procedure works for \(k-1\) decomposable formulas, we can use it to compute a fixed point \(H_i\) for each \(B_i\). Now, \(H=B(\square D_1(H_1),...,\square D_k(H_k))\) is the desired fixed point for \(\phi\).

This procedure constructs fixed points with structural similarity to the original sentence.

Example

Let’s compute the fixed point of \(p\leftrightarrow \neg\square(q\to p)\).

We can 1-decompose the formula in \(B(d)=\neg d\), \(D_1(p)=q\to p\).

Then \(B_1(p)=\neg \top = \bot\), which is its own fixed point. Thus the desired fixed point is \(H=B(\square D_1(\bot))=\neg\square \neg q\).

Exercise: Compute the fixed point of \(p\leftrightarrow \square [\square(p\wedge q)\wedge \square(p\wedge r)]\).

Now we compute the fixed point of \(B(\top)\), which is simply \(\top\).

Therefore the fixed point of the whole expression is \(B(\square D_1(p=\top))=\square[\square(\top\wedge q)\wedge \square(\top\wedge r)]=\square[\square(q)\wedge \square(r)]\) <div><div>

Generalized fixed point theorem

Suppose that \(A_i(p_1,...,p_n)\) are \(n\) modal sentences such that \(A_i\) is modalized in \(p_n\) (possibly containing sentence letters other than \(p_js\)).

Then there exists \(H_1, ...,H_n\) in which no \(p_j\) appears such that \(GL\vdash \wedge_{i\le n} \{\boxdot (p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow \wedge_{i\le n} \{\boxdot(p_i\leftrightarrow H_i)\}\).

For the base step, we know by the fixed point theorem that there is \(H\) such that \(GL\vdash \boxdot(p_1\leftrightarrow A_i(p_1,...,p_n)) \leftrightarrow \boxdot(p_1\leftrightarrow H(p_2,...,p_n))\)

Now suppose that for \(j\) we have \(H_1,...,H_j\) such that \(GL\vdash \wedge_{i\le j} \{\boxdot(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow \wedge_{i\le j} \{\boxdot(p_i\leftrightarrow H_i(p_{j+1},...,p_n))\}\).

By the second substitution theorem, \(GL\vdash \boxdot(A\leftrightarrow B)\rightarrow [F(A)\leftrightarrow F(B)]\). Therefore we have that \(GL\vdash \boxdot(p_i\leftrightarrow H_i(p_{j+1},...,p_n)\rightarrow [\boxdot(p_{j+1}\leftrightarrow A_{j+1}(p_{1},...,p_n))\leftrightarrow \boxdot(p_{j+1}\leftrightarrow A_{j+1}(p_{1},...,p_{i-1},H_i(p_{j+1},...,p_n),p_{i+1},...,p_n))]\).

If we iterate the replacements, we finally end up with \(GL\vdash \wedge_{i\le j} \{\boxdot(p_i\leftrightarrow A_i(p_1,...,p_n)\}\rightarrow \boxdot(p_{j+1}\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n))\).

Again by the fixed point theorem, there is \(H_{j+1}'\) such that \(GL\vdash \boxdot(p_{j+1}\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n)) \leftrightarrow \boxdot[p_{j+1}\leftrightarrow H_{j+1}'(p_{j+2},...,p_n)]\).

But as before, by the second substitution theorem, \(GL\vdash \boxdot[p_{j+1}\leftrightarrow H_{j+1}'(p_{j+2},...,p_n)]\rightarrow [\boxdot(p_i\leftrightarrow H_i(p_{j+1},...,p_n)) \leftrightarrow \boxdot(p_i\leftrightarrow H_i(H_{j+1}',...,p_n))\).

Let \(H_{i}'\) stand for \(H_i(H_{j+1}',...,p_n)\), and by combining the previous lines we find that \(GL\vdash \wedge_{i\le j+1} \{\boxdot(p_i\leftrightarrow A_i(p_1,...,p_n)\}\rightarrow \wedge_{i\le j+1} \{\boxdot(p_i\leftrightarrow H_i'(p_{j+2},...,p_n))\}\).

By Goldfarb’s lemma, we do not need to check the other direction, so \(GL\vdash \wedge_{i\le j+1} \{\boxdot(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow \wedge_{i\le j+1} \{\boxdot(p_i\leftrightarrow H_i'(p_{j+2},...,p_n))\}\) and the proof is finished \(\square\)

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

<div><div>

An immediate consequence of the theorem is that for those fixed points \(H_i\) and every \(A_i\), \(GL\vdash H_i\leftrightarrow A_i(H_1,...,H_n)\).

Indeed, since \(GL\) is closed under substitution, we can make the change \(p_i\) for \(H_i\) in the theorem to get that \(GL\vdash \wedge_{i\le n} \{\boxdot (H_i\leftrightarrow A_i(H_1,...,H_n)\}\leftrightarrow \wedge_{i\le n} \{\boxdot(H_i\leftrightarrow H_i)\}\).

Since the righthand side is trivially a theorem of \(GL\), we get the desired result.