The general construction of the proof

The general philosophy to a modal completeness result is always the same. In order to show the completeness of some logic L w.r.t. its class of characteristic frames $\mathcal{K}$ one has to prove that

$$\forall \mathrm{A} \ [ \ \forall \mathcal{M} \in \mathcal{K}... ...M} \models \mathrm{ A} \longrightarrow L \vdash \mathrm{ A}\ ]$$

or equivalently

$$\forall \mathrm{A} \ [ \ L \nvdash \mathrm{A} \longrightarrow... ...cal{M} \in \mathcal{K} \ \ \mathcal{M} \nvDash \mathrm{A}\ ].$$

Thus the main approach is clear: given a modal sentence ${\mathcal A}$that is not derivable in L, one has to provide a model $\mathcal{M}$and a node m that forces $\neg \mathcal{A}$, that is, ${\mathcal M},m\Vdash \neg {\mathcal A}$. Moreover one wants the frame of this model to be in the class of characteristic frames. We reserve the symbol ${\mathcal A}$ to designate a formula that is not derivable over $\mathit{ILM}$. (The font of the symbol ${\mathcal A}$ is a little unusual in the modal setting, but we want to have the A free to use in the course of this chapter.) In all completeness proofs the basic material for the construction of a countermodel consists of maximal consistent sets of sentences. So a world of such a countermodel will comprise a copy of a maximal consistent set of sentences. One combines these sets in such a way that eventually one obtains a so-called truth lemma, correlating membership of a sentence to a set, to the forcing of that sentence in that particular world/set. In our approach presented below we will do exactly this. Distinctions though can be found in the way the countermodel is provided and the material that is used.
In modal completeness results one often wants, in addition, to prove the decidability of that logic. If an r.e. axiomatizable logic has the finite model property it automatically is decidable. For this reason one always looks for a finite countermodel in the completeness proof. One essential ingredient for obtaining finiteness in provability logic is to not work with full maximal consistent sets of modal sentences, but with sufficiently large truncated parts of them instead. These truncated parts are maximal consistent subsets of a so-called adequate set of sentences. In choosing the adequate set one is driven by two opposite motives. One does not want the adequate set too large, because of the finiteness and hence the decidability. It is generally speaking also more difficult to match the consistent sets in a proper way if they contain more sentences. Nor does one wants the adequate set too small because one wants to have the truth lemma for sufficiently many sentences, which therefore must be in the set. Once the adequate set is chosen, the relations between the maximal consistent subsets of the adequate set are defined. By doing so, one obtains the so-called canonical model for which you prove the truth lemma.

In our approach we will not define in one blow the canonical model but instead we will inductively build up a model. Further we will adhere to the method of ``adequate set abuse''. This means that your adequate set is very large but we only want the truth lemma for a finite set of so-called relevant sentences. We also use a different finite set for ensuring that our R-relation is conversely well-founded. In the old method one single set had to take care of all the jobs that are here done by three different sets. Our model $\langle M , R , S , \Vdash \rangle$ will be built up in stages out of copies of maximal $\mathit{ILM}$-consistent sets of modal sentences in such a way that eventually the following truth lemma holds:

$$\forall \mathrm{A}\in \mathit{R} \ \ \forall m \in M \ \ [ m \Vdash \mathrm{A} \Leftrightarrow \mathrm{A} \in m ].$$

$\mathit{R}$ is the set of relevant sentences. It is the minimal set containing $\neg \mathcal{A}$ that is closed under taking subformulas and single negation. Since $\mathit{ILM}\nvdash \mathcal{A}$ there is a maximal $\mathit{ILM}$-consistent set m₀ with $\neg \mathcal{A} \in m_0$. By building an $\mathit{ILM}$-model ``containing'' m₀ we obtain a countermodel to ${\mathcal A}$.
The proof of the truth lemma will run as follows:

• $\mathcal{M},m \Vdash P \Leftrightarrow P \in m$ by definition of $\Vdash$ for propositional variables P.
• $\mathcal{M},m \Vdash \neg \mathrm{A} \Leftrightarrow \mathcal{M},m \nVdash \mathrm{A} \Leftrightarrow \mathrm{A} \notin m \Leftrightarrow \neg \mathrm{A} \in m$.
• $\mathcal{M},m \Vdash \mathrm{A} \wedge \mathrm{B} \Leftrightarrow \mathcal{M}... ... \mbox{,} \mathrm{B} \in m \Leftrightarrow \mathrm{A} \wedge \mathrm{B} \in m$.
• $\mathcal{M},m \Vdash \mathrm{A} \rhd \mathrm{B} \Leftrightarrow \mathrm{A} \rhd \mathrm{B} \in m$ by the construction of $\mathcal{M}$ . Actually the two directions are separately taken care of in the construction.
  `` $\Leftarrow$'' If $\mathrm{A} \rhd \mathrm{B} \in m$ then we will have constructed the model so that indeed $\mathcal{M},m \Vdash \mathrm{A} \rhd \mathrm{B}$.
  `` $\Rightarrow$'' If $A \rhd B \notin m$ then by the maximality of m we have that $\neg ( A \rhd B ) \in m$. This is also a relevant formula. Therefore the construction is such that one has $\mathcal{M},m \Vdash \neg ( A \rhd B )$.

The countermodel must be an $\mathit{ILM}$-model. The M axiom states $A\rhd B\rightarrow A\wedge \Box C\rhd B\wedge \Box C$ and it demands the characteristic $\mathit{ILM}$-frames to satisfy the following condition: $x S y R z \rightarrow x R z$. Thus in the construction of our model we want that every possible R-successor of such a world y, can consistently be taken to be an R-successor of x. This can be done if we demand $x \subset_{\Box} y$. (This means $\Box A \in x \rightarrow \Box A \in y$.) We will prove a lemma that guarantees one can always incorporate this condition. It is now time to prepare for the construction and develop some tools.