[summary:

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

This result can be used to give us insight about self-referent sentences of arithmetic. ]

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]$ %%note: Notation: $\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.

%%hidden(Proof): 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)]$. %%

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

%%hidden(Proof): 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)$. %%

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 [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 [godelsecondincompletenesstheorm unless $PA$ is inconsistent], and that it is not disprovable unless it is [omegainconsistency $\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 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 [\square(p\wedge 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))=\square[\square(\top\wedge q)\wedge \square(\top\wedge r)]=\square[\square(q)\wedge \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(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.

%%

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.