# Fixed point theorem of provability logic

The fixed point the­o­rem of prov­abil­ity logic is a key re­sult that gives a ex­plicit pro­ce­dure to find equiv­alences for sen­tences such as the ones pro­duced by the di­ag­o­nal lemma.

In its most sim­ple for­mu­la­tion, it states that:

Let $$\phi(p)$$ be a modal sen­tence modal­ized in $$p$$. Then there ex­ists a let­ter­less $$H$$ such that $$GL\vdash \boxdot[p\leftrightarrow \phi(p)] \leftrightarrow \boxdot[p\leftrightarrow H]$$ noteNo­ta­tion: $$\boxdot A = A\wedge \square A$$.

This re­sult can be gen­er­al­ized for cases in which let­ter sen­tences other than $$p$$ ap­pear in the origi­nal for­mula, and the case where mul­ti­ple for­mu­las are pre­sent.

# Fixed points

The $$H$$ that ap­pears in the state­ment of the the­o­rem is called a fixed point of $$\phi(p)$$ on $$p$$.

In gen­eral, a fixed point of a for­mula $$\psi(p, q_1...,q_n)$$ on $$p$$ will be a modal for­mula $$H(q_1,...,q_n)$$ in which $$p$$ does not ap­pear 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 the­o­rem gives a suffi­cient con­di­tion for the ex­is­tence of fixed points, namely that $$\psi$$ is modal­ized in $$\psi$$. It is an open prob­lem to de­ter­mine a nec­es­sary con­di­tion for the ex­is­tence of fixed points.

Fixed points satisfy some im­por­tant prop­er­ties:

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 co­in­cides with our in­tu­ition of what a fixed point is, since this can be seen as an ar­gu­ment that when fed to $$\phi$$ it re­turns some­thing equiv­a­lent to it­self.

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 nor­mal, it is closed un­der sub­sti­tu­tion. By sub­sti­tu­ing $$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 triv­ially $$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 unique­ness 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)$$.

Sup­pose $$I$$ is such that $$GL\vdash H\leftrightarrow I$$. Then by the first sub­sti­tu­tion the­o­rem, $$GL\vdash F(I)\leftrightarrow F(H)$$ for ev­ery for­mula $$F(q)$$. If $$F(q)=\boxdot(p\leftrightarrow q)$$, then $$GL\vdash \boxdot(p\leftrightarrow H)\leftrightarrow \boxdot(p\leftrightarrow I)$$, from which it fol­lows that $$GL\vdash \boxdot(p\leftrightarrow \phi(p))\leftrightarrow (p\leftrightarrow I)$$.

Con­versely, if $$H$$ and $$I$$ are fixed points, then $$GL\vdash \boxdot (p\leftrightarrow H)\leftrightarrow \boxdot (p\leftrightarrow I)$$, so since $$GL$$ is closed un­der sub­sti­tu­tion, $$GL\vdash\boxdot (H\leftrightarrow H)\leftrightarrow \boxdot (H\leftrightarrow I)$$. Since $$GL\vdash \boxdot (H\leftrightarrow H)$$, it fol­lows that $$GL\vdash (H\leftrightarrow I)$$. <div><div>

# Spe­cial case fixed point theorem

The spe­cial case of the fixed point the­o­rem is what we stated at the be­gin­ning of the page. Namely:

Let $$\phi(p)$$ be a modal sen­tence modal­ized in p. Then there ex­ists a let­ter­less $$H$$ such that $$GL\vdash \boxdot[p\leftrightarrow \phi(p)] \leftrightarrow \boxdot[p\leftrightarrow H]$$.

There is a nice se­man­ti­cal pro­ce­dure based on Kripke mod­els that al­lows to com­pute $$H$$ as a truth func­tional com­pound of sen­tences $$\square^n \bot$$ note$$\square^n A = \underbrace{\square,\square,\ldots,\square}_{n\text{-times}} A$$ . (ie, $$H$$ is in nor­mal form).

## $$A$$-traces

Let $$A$$ be a modal sen­tence modal­ized in $$p$$ in which no other sen­tence let­ter ap­pears (we call such a sen­tence a $$p$$-sen­tence). We want to calcu­late $$A$$’s fixed point on $$p$$. This pro­ce­dure bears a re­sem­blance to the trace method for eval­u­at­ing let­ter­less modal sen­tences.

We are go­ing to in­tro­duce the no­tion of the $$A$$-trace of a $$p$$-sen­tence $$B$$, no­tated by $$[[B]]_A$$. The $$A$$-trace maps modal sen­tences to sets of nat­u­ral num­bers, and is defined re­cur­sively as fol­lows:

• $$[[\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, tran­si­tive and ir­reflex­ive Kripke model in which $$(p\leftrightarrow A) is valid, and$$B$$a$$p$$-sentence. Then$$M,w\mod­els 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\leftrightar­row 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\leftrightar­row \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}\set­minus {0}$$. Thus$$H = \square^{0+1}\bot \wedge \square^0\bot = \neg\square\bot$$. Therefore,$$GL\vdash \square \neg\square p\leftrightar­row \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>\leftrightar­row \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\leftrightar­row \neg\square{PA} G$$, by necessitation we have that for such a$$G$$then$$PA\vdash \squarePAG\leftrightar­row \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\leftrightar­row \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\leftrightar­row\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, q1,…,qn)$$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 D1(p), …, \square D{k}(p))$$, since every$$p$$occurs within the scope of a$$\square­$$(The$$qi$$s are omitted for simplicity, but they may appear scattered between$$B$$and the$$Di$$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$$Bi = B(\square D1(p), …, \square D{i-1}(p),\top, \square D{i+1}(p),…,\square Dk(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$$Hi$$for each$$Bi$$. Now,$$H=B(\square D1(H1),…,\square Dk(Hk))$$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\leftrightar­row \neg\square(q\to p)$$. We can 1-decompose the formula in$$B(d)=\neg d$$,$$D1(p)=q\to p$$. Then$$B1(p)=\neg \top = \bot$$, which is its own fixed point. Thus the desired fixed point is$$H=B(\square D1(\bot))=\neg\square \neg q$$. **Exercise:** Compute the fixed point of$$p\leftrightar­row \square q)\wedge \square(p\wedge r)$$. %%hidden(Show solution): One possible decomposition of the the formula at hand is$$B(a)=a$$,$$D1(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 D1(p=\top))=\squareq)\wedge \square(\top\wedge r)=\square\square(r)$$%% #Generalized fixed point theorem >Suppose that$$Ai(p1,…,pn)$$are$$n$$modal sentences such that$$Ai$$is modalized in$$$$(possibly containing sentence letters other than$$pjs$$). >Then there exists$$H1, …,H$$in which no$$pj$$appears such that$$GL\vdash \wedge{i\le n} {\box­dot (pi\leftrightar­row Ai(p1,…,pn)}\leftrightar­row \wedge{i\le n} {\box­dot(pi\leftrightar­row Hi)}$$. %%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 \box­dot(p1\leftrightar­row Ai(p1,…,pn)) \leftrightar­row \box­dot(p1\leftrightar­row H(p2,…,pn))$$Now suppose that for$$j$$we have$$H1,…,Hj$$such that$$GL\vdash \wedge{i\le j} {\box­dot(pi\leftrightar­row Ai(p1,…,pn)}\leftrightar­row \wedge{i\le j} {\box­dot(pi\leftrightar­row Hi(p{j+1},…,pn))}$$. By the [ second substitution theorem],$$GL\vdash \box­dot(A\leftrightar­row B)\rightar­row F(B)$$. Therefore we have that$$GL\vdash \box­dot(pi\leftrightar­row Hi(p{j+1},…,pn)\rightar­row A{j+1}(p{1},…,pn))\leftrightar­row \box­dot(p{j+1}\leftrightar­row A{j+1}(p{1},…,p{i-1},Hi(p{j+1},…,pn),p{i+1},…,pn))$$. If we iterate the replacements, we finally end up with$$GL\vdash \wedge{i\le j} {\box­dot(pi\leftrightar­row Ai(p1,…,pn)}\rightar­row \box­dot(p{j+1}\leftrightar­row A{j+1}(H1,…,Hj,p{j+1},…,pn))$$. Again by the fixed point theorem, there is$$H{j+1}‘$$such that$$GL\vdash \box­dot(p{j+1}\leftrightar­row A{j+1}(H1,…,Hj,p{j+1},…,pn)) \leftrightar­row \box­dotH{j+1}‘(p{j+2},…,pn)$$. But as before, by the second substitution theorem,$$GL\vdash \box­dotH<em>{j+1}‘(p{j+2},…,pn)\rightar­row [\box­dot(pi\leftrightar­row Hi(p{j+1},…,pn)) \leftrightar­row \box­dot(pi\leftrightar­row Hi(H{j+1}‘,…,pn))$$. Let$$H{i}‘$$stand for$$Hi(H{j+1}‘,…,pn)$$, and by combining the previous lines we find that$$GL\vdash \wedge{i\le j+1} {\box­dot(pi\leftrightar­row Ai(p1,…,pn)}\rightar­row \wedge{i\le j+1} {\box­dot(pi\leftrightar­row Hi’(p{j+2},…,pn))}$$. By [ Goldfarb's lemma], we do not need to check the other direction, so$$GL\vdash \wedge{i\le j+1} {\box­dot(pi\leftrightar­row Ai(p1,…,pn)}\leftrightar­row \wedge{i\le j+1} {\box­dot(pi\leftrightar­row Hi’(p{j+2},…,pn))}$$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$$Hi’$$to compute fixed points. %% An immediate consequence of the theorem is that for those fixed points$$Hi$$and every$$Ai$$,$$GL\vdash Hi\leftrightar­row Ai(H1,…,Hn)$$. Indeed, since$$GL$$is closed under substitution, we can make the change$$pi$$for$$Hi$$in the theorem to get that$$GL\vdash \wedge{i\le n} {\box­dot (Hi\leftrightar­row Ai(H1,…,Hn)}\leftrightar­row \wedge{i\le n} {\box­dot(Hi\leftrightar­row H_i)}$$. Since the righthand side is trivially a theorem of$$GL\$, we get the de­sired re­sult.

Parents: