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 .

In its most simple formulation, it states that:

Let be a modal sentence in $p$ . Then there exists a letterless $H$ such that $G L ⊢ ⊡ [p \leftrightarrow ϕ (p)] \leftrightarrow ⊡ [p \leftrightarrow H]$ ^[1].

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 $ϕ (p)$ on $p$ .

In general, a fixed point of a formula $ψ (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 $G L ⊢ ⊡ [p \leftrightarrow ψ (p, q_{1}, . . ., q_{n})] \leftrightarrow ⊡ [p_{i} \leftrightarrow H (q_{1}, . . ., q_{n})]$ .

The fixed point theorem gives a sufficient condition for the existence of fixed points, namely that $ψ$ is modalized in $ψ$ . 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 $ϕ$ on $p$ , then $G L ⊢ H (q_{1}, . . ., q_{n}) \leftrightarrow ϕ (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 $ϕ$ it returns something equivalent to itself.

Proof

Since $H$ is a fixed point, $G L ⊢ ⊡ [p \leftrightarrow ψ (p, q_{1}, . . ., q_{n})] \leftrightarrow ⊡ [p_{i} \leftrightarrow H (q_{1}, . . ., q_{n})]$ . Since $G L$ is , it is closed under substitution. By substituing $p$ for $H$ , we find that $G L ⊢ ⊡ [H (q_{1}, . . ., q_{n}) \leftrightarrow ψ (H (q_{1}, . . ., q_{n}), q_{1}, . . ., q_{n})] \leftrightarrow ⊡ [H (q_{1}, . . ., q_{n}) \leftrightarrow H (q_{1}, . . ., q_{n})]$ .

But trivially $G L ⊢ ⊡ [H (q_{1}, . . ., q_{n}) \leftrightarrow H (q_{1}, . . ., q_{n})$ , so $G L ⊢ ⊡ [H (q_{1}, . . ., q_{n}) \leftrightarrow ψ (H (q_{1}, . . ., q_{n}), q_{1}, . . ., q_{n})]$ .

$H$ and $I$ are fixed points of $ϕ$ if and only if $G L ⊢ H \leftrightarrow I$ . This is knows as the uniqueness of fixed points.

Proof

Let $H$ be a fixed point on $p$ of $ϕ (p)$ ; that is, $G L ⊢ ⊡ (p \leftrightarrow ϕ (p)) \leftrightarrow (p \leftrightarrow H)$ .

Suppose $I$ is such that $G L ⊢ H \leftrightarrow I$ . Then by the first substitution theorem, $G L ⊢ F (I) \leftrightarrow F (H)$ for every formula $F (q)$ . If $F (q) = ⊡ (p \leftrightarrow q)$ , then $G L ⊢ ⊡ (p \leftrightarrow H) \leftrightarrow ⊡ (p \leftrightarrow I)$ , from which it follows that $G L ⊢ ⊡ (p \leftrightarrow ϕ (p)) \leftrightarrow (p \leftrightarrow I)$ .

Conversely, if $H$ and $I$ are fixed points, then $G L ⊢ ⊡ (p \leftrightarrow H) \leftrightarrow ⊡ (p \leftrightarrow I)$ , so since $G L$ is closed under substitution, $G L ⊢ ⊡ (H \leftrightarrow H) \leftrightarrow ⊡ (H \leftrightarrow I)$ . Since $G L ⊢ ⊡ (H \leftrightarrow H)$ , it follows that $G L ⊢ (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 $ϕ (p)$ be a modal sentence in p. Then there exists a letterless $H$ such that $G L ⊢ ⊡ [p \leftrightarrow ϕ (p)] \leftrightarrow ⊡ [p \leftrightarrow H]$ .

There is a nice semantical procedure based on that allows to compute $H$ as a truth functional compound of sentences $□^{n} ⊥$ ^[2]. (ie, $H$ is in ).

$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 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 , and is defined recursively as follows:

$[[⊥]]_{A} = \emptyset$

$[[B \to C]]_{A} = (N ∖ [[B]]_{A}) \cup [[C]]_{A}$

$[[□ D]]_{A} = {m : \forall i < m i \in [[D]]_{A}}$

$[[p]]_{A} = [[A]]_{A}$

Lemma: Let $M$ be a finite, transitive and irreflexive Kripke model in which $(p \leftrightarrow A) i s v a l i d, a n d$ B$ a $p$ -sentence. Then $M, w ⊨ B$ iff $ρ (w) \in [[B]]_{A}$ .

Proof

Coming soon

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 $□$ s in $A$ .

Proof

Coming soon

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 $□^{n + 1} ⊥ \land □^{n} ⊥$ ^[3]

In the following section we work through an example, and demonstrate how can we easily compute those fixed points using a .

Applications

For an example, we will compute the fixed point for the modal $p \leftrightarrow \neg □ p$ and analyze its significance.

We start by examining the truth value of $\neg □ 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 $□ 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 □ p$ .

We iterate the procedure for the next world ranks.

$\begin{matrix} world= & p & □ (p) & \neg □ (p) 0 & ⊥ & ⊤ & ⊥ 1 & ⊤ & ⊥ & ⊤ 2 & ⊤ & ⊥ & ⊤ \end{matrix}$

Since there is only one $□$ 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 □ p} = N ∖ {0}$ . Thus $H = □^{0 + 1} ⊥ \land □^{0} ⊥ = \neg □ ⊥$ .

Therefore, $G L ⊢ □ [p \leftrightarrow \neg □ p] \leftrightarrow □ [p \leftrightarrow \neg □ ⊥]$ . Thus, the fixed point for the modal Gödel sentence is the of arithmetic!

By employing the , we can translate this result to $P A$ and show that $P A ⊢ □_{P A} [G \leftrightarrow \neg □_{P A} G] \leftrightarrow □_{P A} [G \leftrightarrow \neg □_{P A} ⊥]$ for every sentence $G$ of arithmetic.

Since in $P A$ we can construct $G$ by the such that $P A ⊢ G \leftrightarrow \neg □_{P A} G$ , by necessitation we have that for such a $G$ then $P A ⊢ □_{P} A [G \leftrightarrow \neg □_{P A} G]$ . By the theorem we just proved using the fixed point, then $P A ⊢ □_{P A} [G \leftrightarrow \neg □_{P A} ⊥]$ . SInce then $P A ⊢ G \leftrightarrow \neg □_{P A} ⊥$ .

Surprisingly enough, the Gödel sentence is equivalent to the consistency of arithmetic! This makes more evident that $G$ is not provable , and that it is not disprovable unless it is .

Exercise: Find the fixed point for the $H \leftrightarrow □ H$ .

Show solution

$\begin{matrix} world= & p & □ (p) 0 & ⊤ & ⊤ 1 & ⊤ & ⊤ \end{matrix}$ Thus the fixed point is simply $⊤$ .

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 $ϕ (p, q_{1}, . . ., q_{n})$ be a modal sentence in p. Then $ϕ$ 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 $ϕ$ be as in the hypothesis of the fixed point theorem. Then we can express $ϕ$ as $B (□ D_{1} (p), . . ., □ D_{k} (p))$ , since every $p$ occurs within the scope of a $□$ (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 $ϕ$ .

If $ϕ$ is $0$ -decomposable, then it is already a fixed point, since $p$ does not appear.

Otherwise, consider $B_{i} = B (□ D_{1} (p), . . ., □ D_{i - 1} (p), ⊤, □ D_{i + 1} (p), . . ., □ 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 (□ D_{1} (H_{1}), . . ., □ D_{k} (H_{k}))$ is the desired fixed point for $ϕ$ .

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 □ (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 ⊤ = ⊥$ , which is its own fixed point. Thus the desired fixed point is $H = B (□ D_{1} (⊥)) = \neg □ \neg q$ .

Exercise: Compute the fixed point of $p \leftrightarrow □ [□ (p \land q) \land □ (p \land r)]$ .

Show solution

One possible decomposition of the the formula at hand is $B (a) = a$ , $D_{1} (p) = □ (p \land q) \land □ (p \land r)$ .

Now we compute the fixed point of $B (⊤)$ , which is simply $⊤$ .

Therefore the fixed point of the whole expression is $B (□ D_{1} (p = ⊤)) = □ [□ (⊤ \land q) \land □ (⊤ \land r)] = □ [□ (q) \land □ (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_{j} s$ ).

Then there exists $H_{1}, . . ., H_{n}$ in which no $p_{j}$ appears such that $G L ⊢ \land_{i \leq n} {⊡ (p_{i} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})} \leftrightarrow \land_{i \leq n} {⊡ (p_{i} \leftrightarrow H_{i})}$ .

Proof

We will prove it by induction.

For the base step, we know by the fixed point theorem that there is $H$ such that $G L ⊢ ⊡ (p_{1} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})) \leftrightarrow ⊡ (p_{1} \leftrightarrow H (p_{2}, . . ., p_{n}))$

Now suppose that for $j$ we have $H_{1}, . . ., H_{j}$ such that $G L ⊢ \land_{i \leq j} {⊡ (p_{i} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})} \leftrightarrow \land_{i \leq j} {⊡ (p_{i} \leftrightarrow H_{i} (p_{j + 1}, . . ., p_{n}))}$ .

By the , $G L ⊢ ⊡ (A \leftrightarrow B) \to [F (A) \leftrightarrow F (B)]$ . Therefore we have that $G L ⊢ ⊡ (p_{i} \leftrightarrow H_{i} (p_{j + 1}, . . ., p_{n}) \to [⊡ (p_{j + 1} \leftrightarrow A_{j + 1} (p_{1}, . . ., p_{n})) \leftrightarrow ⊡ (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 $G L ⊢ \land_{i \leq j} {⊡ (p_{i} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})} \to ⊡ (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 $G L ⊢ ⊡ (p_{j + 1} \leftrightarrow A_{j + 1} (H_{1}, . . ., H_{j}, p_{j + 1}, . . ., p_{n})) \leftrightarrow ⊡ [p_{j + 1} \leftrightarrow H_{j + 1}^{'} (p_{j + 2}, . . ., p_{n})]$ .

But as before, by the second substitution theorem, $G L ⊢ ⊡ [p_{j + 1} \leftrightarrow H_{j + 1}^{'} (p_{j + 2}, . . ., p_{n})] \to [⊡ (p_{i} \leftrightarrow H_{i} (p_{j + 1}, . . ., p_{n})) \leftrightarrow ⊡ (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 $G L ⊢ \land_{i \leq j + 1} {⊡ (p_{i} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})} \to \land_{i \leq j + 1} {⊡ (p_{i} \leftrightarrow H_{i}^{'} (p_{j + 2}, . . ., p_{n}))}$ .

By , we do not need to check the other direction, so $G L ⊢ \land_{i \leq j + 1} {⊡ (p_{i} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})} \leftrightarrow \land_{i \leq j + 1} {⊡ (p_{i} \leftrightarrow H_{i}^{'} (p_{j + 2}, . . ., p_{n}))}$ and the proof is finished $□$

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}$ , $G L ⊢ H_{i} \leftrightarrow A_{i} (H_{1}, . . ., H_{n})$ .

Indeed, since $G L$ is closed under substitution, we can make the change $p_{i}$ for $H_{i}$ in the theorem to get that $G L ⊢ \land_{i \leq n} {⊡ (H_{i} \leftrightarrow A_{i} (H_{1}, . . ., H_{n})} \leftrightarrow \land_{i \leq n} {⊡ (H_{i} \leftrightarrow H_{i})}$ .

Since the righthand side is trivially a theorem of $G L$ , we get the desired result.

^{^︎}
Notation: $⊡ A = A \land □ A$
^{^︎}
~D\square^n A = \underbrace{\square,\square,\ldots,\square}_{n\text{-times}} A~D
^{^︎}
Such a sentence is only true in worlds of rank $n$

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 .

In its most simple formulation, it states that:

Let be a modal sentence in $p$ . Then there exists a letterless $H$ such that $G L ⊢ ⊡ [p \leftrightarrow ϕ (p)] \leftrightarrow ⊡ [p \leftrightarrow H]$ ^[1].

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 $ϕ (p)$ on $p$ .

Fixed points satisfy some important properties:

Proof

$H$ and $I$ are fixed points of $ϕ$ if and only if $G L ⊢ H \leftrightarrow I$ . This is knows as the uniqueness of fixed points.

Proof

Let $H$ be a fixed point on $p$ of $ϕ (p)$ ; that is, $G L ⊢ ⊡ (p \leftrightarrow ϕ (p)) \leftrightarrow (p \leftrightarrow H)$ .

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 $ϕ (p)$ be a modal sentence in p. Then there exists a letterless $H$ such that $G L ⊢ ⊡ [p \leftrightarrow ϕ (p)] \leftrightarrow ⊡ [p \leftrightarrow H]$ .

There is a nice semantical procedure based on that allows to compute $H$ as a truth functional compound of sentences $□^{n} ⊥$ ^[2]. (ie, $H$ is in ).

$A$ -traces

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 , and is defined recursively as follows:

$[[⊥]]_{A} = \emptyset$

$[[B \to C]]_{A} = (N ∖ [[B]]_{A}) \cup [[C]]_{A}$

$[[□ D]]_{A} = {m : \forall i < m i \in [[D]]_{A}}$

$[[p]]_{A} = [[A]]_{A}$

Lemma: Let $M$ be a finite, transitive and irreflexive Kripke model in which $(p \leftrightarrow A) i s v a l i d, a n d$ B$ a $p$ -sentence. Then $M, w ⊨ B$ iff $ρ (w) \in [[B]]_{A}$ .

Proof

Coming soon

Proof

Coming soon

In the following section we work through an example, and demonstrate how can we easily compute those fixed points using a .

Applications

For an example, we will compute the fixed point for the modal $p \leftrightarrow \neg □ p$ and analyze its significance.

We iterate the procedure for the next world ranks.

$\begin{matrix} world= & p & □ (p) & \neg □ (p) 0 & ⊥ & ⊤ & ⊥ 1 & ⊤ & ⊥ & ⊤ 2 & ⊤ & ⊥ & ⊤ \end{matrix}$

From the table we have just constructed it becomes evident that $[[p]]_{\neg □ p} = N ∖ {0}$ . Thus $H = □^{0 + 1} ⊥ \land □^{0} ⊥ = \neg □ ⊥$ .

Therefore, $G L ⊢ □ [p \leftrightarrow \neg □ p] \leftrightarrow □ [p \leftrightarrow \neg □ ⊥]$ . Thus, the fixed point for the modal Gödel sentence is the of arithmetic!

Surprisingly enough, the Gödel sentence is equivalent to the consistency of arithmetic! This makes more evident that $G$ is not provable , and that it is not disprovable unless it is .

Exercise: Find the fixed point for the $H \leftrightarrow □ H$ .

Show solution

$\begin{matrix} world= & p & □ (p) 0 & ⊤ & ⊤ 1 & ⊤ & ⊤ \end{matrix}$ Thus the fixed point is simply $⊤$ .

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 $ϕ (p, q_{1}, . . ., q_{n})$ be a modal sentence in p. Then $ϕ$ 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

If $ϕ$ is $0$ -decomposable, then it is already a fixed point, since $p$ does not appear.

Otherwise, consider $B_{i} = B (□ D_{1} (p), . . ., □ D_{i - 1} (p), ⊤, □ D_{i + 1} (p), . . ., □ D_{k} (p))$ , which is $k - 1$ -decomposable.

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 □ (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 ⊤ = ⊥$ , which is its own fixed point. Thus the desired fixed point is $H = B (□ D_{1} (⊥)) = \neg □ \neg q$ .

Exercise: Compute the fixed point of $p \leftrightarrow □ [□ (p \land q) \land □ (p \land r)]$ .

Show solution

One possible decomposition of the the formula at hand is $B (a) = a$ , $D_{1} (p) = □ (p \land q) \land □ (p \land r)$ .

Now we compute the fixed point of $B (⊤)$ , which is simply $⊤$ .

Therefore the fixed point of the whole expression is $B (□ D_{1} (p = ⊤)) = □ [□ (⊤ \land q) \land □ (⊤ \land r)] = □ [□ (q) \land □ (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_{j} s$ ).

Then there exists $H_{1}, . . ., H_{n}$ in which no $p_{j}$ appears such that $G L ⊢ \land_{i \leq n} {⊡ (p_{i} \leftrightarrow A_{i} (p_{1}, . . ., p_{n})} \leftrightarrow \land_{i \leq n} {⊡ (p_{i} \leftrightarrow H_{i})}$ .

Proof

We will prove it by induction.

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}$ , $G L ⊢ H_{i} \leftrightarrow A_{i} (H_{1}, . . ., H_{n})$ .

Since the righthand side is trivially a theorem of $G L$ , we get the desired result.

^{^︎}
Notation: $⊡ A = A \land □ A$
^{^︎}
~D\square^n A = \underbrace{\square,\square,\ldots,\square}_{n\text{-times}} A~D
^{^︎}
Such a sentence is only true in worlds of rank $n$

LESSWRONG
LW

Fixed point theorem of provability logic

Fixed points

Special case fixed point theorem

$A$ -traces

Applications

General case

K-decomposition

Example

Generalized fixed point theorem

LESSWRONG
LW

Fixed point theorem of provability logic

Fixed points

Special case fixed point theorem

$A$ -traces

Applications

General case

K-decomposition

Example

Generalized fixed point theorem

Fixed point theorem of provability logic

Fixed points

Special case fixed point theorem

A-traces

Applications

General case

K-decomposition

Example

Generalized fixed point theorem

Fixed point theorem of provability logic

Fixed points

Special case fixed point theorem

A-traces

Applications

General case

K-decomposition

Example

Generalized fixed point theorem

$A$ -traces

$A$ -traces