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


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.


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.


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.


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.


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.