# 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 = \un­der­brace{\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$$-sen­tence. Then $$M,w\models B$$ iff $$\rho(w)\in [[B]]_A$$.

Com­ing soon proof

Lemma: The $$A$$-trace of a $$p$$-sen­tence $$B$$ is ei­ther finite or cofinite, and fur­ther­more ei­ther it has less than $$n$$ el­e­ments or lacks less than $$n$$ el­e­ments, where $$n$$ is the num­ber of $$\square$$s in $$A$$.

Com­ing soon proof

Those two lem­mas al­low us to ex­press the truth value of $$A$$ in terms of world ranks for mod­els in which $$p\leftrightarrow A$$ is valid. Then the fixed point $$H$$ will be ei­ther the union or the nega­tion of the union of a finite num­ber of sen­tences $$\square^{n+1}\bot\wedge \square^n \bot$$ noteSuch a sen­tence is only true in wor­lds of rank $$n$$

In the fol­low­ing sec­tion we work through an ex­am­ple, and demon­strate how can we eas­ily com­pute those fixed points us­ing a Kripke chain.

## Applications

For an ex­am­ple, we will com­pute the fixed point for the modal Gödel sen­tence $$p\leftrightarrow \neg\square p$$ and an­a­lyze its sig­nifi­cance.

We start by ex­am­in­ing the truth value of $$\neg\square p$$ in the $$0$$th rank wor­lds. Since the only let­ter is $$p$$ and it is modal­ized, this can be done with­out prob­lem (re­mem­ber that $$\square B$$ is always true in the rank $$0$$ wor­lds, no mater what $$B$$ is). Now we ap­ply to $$p$$ the con­straint of hav­ing the same truth value as $$\neg\square p$$.

We iter­ate the pro­ce­dure 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 for­mula, the chain is guaran­teed to sta­bi­lize in the first world and there is no need for go­ing fur­ther. We have shown the truth val­ues in world $$2$$ to show that this is in­deed the case.

From the table we have just con­structed it be­comes ev­i­dent that $$[[p]]_{\neg\square p} = \mathbb{N}\setminus \{0\}$$. Thus $$H = \square^{0+1}\bot \wedge \square^0\bot = \neg\square\bot$$.

There­fore, $$GL\vdash \square [p\leftrightarrow \neg\square p]\leftrightarrow \square[p\leftrightarrow \neg\square \bot]$$. Thus, the fixed point for the modal Gödel sen­tence is the con­sis­tency of ar­ith­metic!

By em­ploy­ing the ar­ith­meti­cal sound­ness of GL, we can trans­late this re­sult 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 ev­ery sen­tence $$G$$ of ar­ith­metic.

Since in $$PA$$ we can con­struct $$G$$ by the di­ag­o­nal lemma such that $$PA\vdash G\leftrightarrow \neg\square_{PA} G$$, by ne­ces­si­ta­tion we have that for such a $$G$$ then $$PA\vdash \square_PA[ G\leftrightarrow \neg\square_{PA} G]$$. By the the­o­rem we just proved us­ing the fixed point, then $$PA\vdash \square_{PA}[G\leftrightarrow \neg\square_{PA} \bot]$$. SInce ev­ery­thing $$PA$$ proves is true then $$PA\vdash G\leftrightarrow \neg\square_{PA} \bot$$.

Sur­pris­ingly enough, the Gödel sen­tence is equiv­a­lent to the con­sis­tency of ar­ith­metic! This makes more ev­i­dent that $$G$$ is not prov­able un­less $$PA$$ is in­con­sis­tent, and that it is not dis­prov­able un­less it is $$\omega$$-in­con­sis­tent.

Ex­er­cise: Find the fixed point for the Henkin sen­tence $$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 sim­ply $$\top$$.

# Gen­eral case

The first gen­er­al­iza­tion we make to the the­o­rem is al­low­ing the ap­pear­ance of sen­tence let­ters other than the one we are fix­ing. The con­crete state­ment is as fol­lows:

Let $$\phi(p, q_1,...,q_n)$$ be a modal sen­tence modal­ized in p. Then $$\phi$$ has a fixed point on $$p$$.%%.

There are sev­eral con­struc­tive pro­ce­dures for find­ing the fixed point in the gen­eral case.

One par­tic­u­larly sim­ple pro­ce­dure is based on k-de­com­po­si­tion.

## K-decomposition

Let $$\phi$$ be as in the hy­poth­e­sis of the fixed point the­o­rem. Then we can ex­press $$\phi$$ as $$B(\square D_1(p), ..., \square D_{k}(p))$$, since ev­ery $$p$$ oc­curs within the scope of a $$\square$$ (The $$q_i$$s are omit­ted for sim­plic­ity, but they may ap­pear scat­tered be­tween $$B$$ and the $$D_i$$s). This is called a $$k$$-de­com­po­si­tion of $$\phi$$.

If $$\phi$$ is $$0$$-de­com­pos­able, then it is already a fixed point, since $$p$$ does not ap­pear.

Other­wise, con­sider $$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$$-de­com­pos­able.

As­sum­ing that the pro­ce­dure works for $$k-1$$ de­com­pos­able for­mu­las, we can use it to com­pute a fixed point $$H_i$$ for each $$B_i$$. Now, $$H=B(\square D_1(H_1),...,\square D_k(H_k))$$ is the de­sired fixed point for $$\phi$$.

proof There is a nice se­man­tic proof in Com­putabil­ity and Logic, by Boolos et al.

This pro­ce­dure con­structs fixed points with struc­tural similar­ity to the origi­nal sen­tence.

### Example

Let’s com­pute the fixed point of $$p\leftrightarrow \neg\square(q\to p)$$.

We can 1-de­com­pose the for­mula 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 de­sired fixed point is $$H=B(\square D_1(\bot))=\neg\square \neg q$$.

Ex­er­cise: Com­pute the fixed point of $$p\leftrightarrow \square [\square(p\wedge q)\wedge \square(p\wedge r)]$$.

One pos­si­ble de­com­po­si­tion of the the for­mula at hand is $$B(a)=a$$, $$D_1(p)=\square(p\wedge q)\wedge \square(p\wedge r)$$.

Now we com­pute the fixed point of $$B(\top)$$, which is sim­ply $$\top$$.

There­fore the fixed point of the whole ex­pres­sion 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>

# Gen­er­al­ized fixed point theorem

Sup­pose that $$A_i(p_1,...,p_n)$$ are $$n$$ modal sen­tences such that $$A_i$$ is modal­ized in $$p_n$$ (pos­si­bly con­tain­ing sen­tence let­ters other than $$p_js$$).

Then there ex­ists $$H_1, ...,H_n$$ in which no $$p_j$$ ap­pears 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 in­duc­tion.

For the base step, we know by the fixed point the­o­rem 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 sup­pose 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 sec­ond sub­sti­tu­tion the­o­rem, $$GL\vdash \boxdot(A\leftrightarrow B)\rightarrow [F(A)\leftrightarrow F(B)]$$. There­fore 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 iter­ate the re­place­ments, we fi­nally 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 the­o­rem, 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 be­fore, by the sec­ond sub­sti­tu­tion the­o­rem, $$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 com­bin­ing the pre­vi­ous 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 Gold­farb’s lemma, we do not need to check the other di­rec­tion, 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 re­mark: the proof is wholly con­struc­tive. You can iter­ate the con­struc­tion of fixed point fol­low­ing the pro­ce­dure im­plied by the con­struc­tion of the $$H_i'$$ to com­pute fixed points.

<div><div>

An im­me­di­ate con­se­quence of the the­o­rem is that for those fixed points $$H_i$$ and ev­ery $$A_i$$, $$GL\vdash H_i\leftrightarrow A_i(H_1,...,H_n)$$.

In­deed, since $$GL$$ is closed un­der sub­sti­tu­tion, we can make the change $$p_i$$ for $$H_i$$ in the the­o­rem 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 right­hand side is triv­ially a the­o­rem of $$GL$$, we get the de­sired re­sult.

Parents: