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

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\(.
%%hidden(Proof):
Coming soon [todo: 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\(.
%%hidden(Proof):
Coming soon [todo: 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\( %%note:Such 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 \neg\square p\leftrightarrow \square\neg\square \bot\(. Thus, the fixed point for the modal Gödel sentence is the [-5km] of arithmetic!
By employing the [ arithmetical soundness of GL], we can translate this result to \)PA\( and show that \)PA\vdash \square*{PA} \neg\square*{PA} G<span>\leftrightarrow \square*{PA}\neg\square*{PA} \bot<span>\( for every sentence \)G\( of arithmetic.
Since in \)PA\( we can construct \)G\( by the [-59c] such that \)PA\vdash G\leftrightarrow \neg\square*{PA} G\(, by necessitation we have that for such a \)G\( then \)PA\vdash \square*PAG\leftrightarrow \neg\square*{PA} G*\(. By the theorem we just proved using the fixed point, then \)PA\vdash \square<em>{PA}\neg\square*{PA} \bot*\(. SInce [ everything \)PA\( proves is true] then \)PA\vdash G\leftrightarrow \neg\square<em>{PA} \bot\(.
Surprisingly enough, the Gödel sentence is equivalent to the consistency of arithmetic! This makes more evident that \)G\( is not provable [godel_second_incompleteness_theorm unless \)PA\( is inconsistent], and that it is not disprovable unless it is [omega_inconsistency \)\omega\(-inconsistent].
**Exercise:** Find the fixed point for the [ Henkin sentence] \)H\leftrightarrow\square H\(.
%%hidden(Show solution):
\)\(
\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 [5m4 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\(.
%%hidden(Proof):
[todo: 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 q)\wedge \square(p\wedge r)\(.
%%hidden(Show solution):
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))=\squareq)\wedge \square(\top\wedge r)=\square\square(r)\(
%%
#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)}\(.
%%hidden(Proof):
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(B)\(. Therefore we have that \)GL\vdash \boxdot(p*i\leftrightarrow H*i(p*{j+1},…,p*n)\rightarrow 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 \boxdotH*{j+1}‘(p*{j+2},…,p*n)*\(.
But as before, by the second substitution theorem, \)GL\vdash \boxdotH<em>{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.
%%
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:

- Provability logic
Learn how to reason about provability!