# Fixed point theorem of provability logic

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.

Since $$H$$ is a fixed point, $$GL\vdash \boxdot[p\leftrightarrow\psi(p, q_1,...,q_n)] \leftrightarrow \boxdot[p_i\leftrightarrow H(q_1,...,q_n)]$$. Since $$GL$$ is normal, it is closed under substitution. By substituing $$p$$ for $$H$$, we find that $$GL\vdash \boxdot[H(q_1,...,q_n)\leftrightarrow\psi(H(q_1,...,q_n), q_1,...,q_n)] \leftrightarrow \boxdot[H(q_1,...,q_n)\leftrightarrow H(q_1,...,q_n)]$$.

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.

Let $$H$$ be a fixed point on $$p$$ of $$\phi(p)$$; that is, $$GL\vdash \boxdot(p\leftrightarrow \phi(p))\leftrightarrow (p\leftrightarrow H)$$.

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$$.

Coming soon proof

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$$.

Coming soon proof

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.

$$\begin{array}{cccc} \text{world= } & p & \square (p) & \neg \square (p) \\ 0 & \bot & \top & \bot \\ 1 & \top & \bot & \top \\ 2 & \top & \bot & \top \\ \end{array}$$

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$$.

$$\begin{array}{ccc} \text{world= } & p & \square (p) \\ 0 & \top & \top \\ 1 & \top & \top \\ \end{array}$$
Thus the fixed point is simply $$\top$$.

# 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$$.

proof There is a nice semantic proof in Computability and Logic, by Boolos et al.

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)]$$.

One possible decomposition of the the formula at hand is $$B(a)=a$$, $$D_1(p)=\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)\}$$.

We will prove it by induction.

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.

Parents: