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: