Fixed point theorem of provability logic

fixed_point_theorem_provability_logic.json

https://arbital.com/p/fixed_point_theorem_provability_logic

by Jaime Sevilla Molina Jul 27 2016 updated Mar 2 2017

Deal with those pesky self-referential sentences!

[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:

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.