I am working through Blackburn et al.'s Modal Logic (ML), and I am currently on the fourth chapter, i.e. Completeness. The idea of completeness is reduced to saying that consistency implies satisfiability. In propositional logic (PL), we have seen a similar notion, namely that of maximally consistent extensions.
In PL, the idea was:
- Start with a consistent set of formulae $\Gamma$, want to show $\Gamma$ is satisfiable
- Extend $\Gamma$ to its maximally consistent extension, $\Gamma'$.
- Turns out that $\Gamma'$ is satisfiable, hence so is $\Gamma$. In PL, this is pretty simple to digest because valuations are all we care about and there are no modalities in the picture.
However, I'm very confused about the working process to achieve something similar in ML. The author introduces maximally consistent sets (calls them MCSs), and then brings up a canonical model. The canonical model is defined as follows, the motivation behind which I strongly lack:
- $W^\Lambda$ is the set of all MCSs.
- $R^\Lambda$ is the binary relation on $W^\Lambda$ defined by $R^\Lambda wu$ if for all formulas $\psi$, $\psi\in u\implies \diamond\psi \in w$.
- $V^\Lambda$ is given by $V^\Lambda(p) = \{w\in W^\Lambda:p\in w\}$
I understand the construction, but why are we doing this? I did see the author proving the Existence Lemma and the Truth Lemma right after this construction, and stating the Canonical Model Theorem, i.e. "Any normal modal logic is strongly complete with respect to its canonical model."
What does this mean? I'd appreciate it if someone can help me understand the bigger picture here since I do understand the tiny details (and that's it). Thank you so much for reading so far!
Best Answer
So, you want to prove the completeness of a modal logic ($\mathit{K}$, $S5$, etc. ), which is formally can be stated as follows:
Completeness: For all $\varphi \in \mathcal{K}$, if $\varphi$ is valid, then $\varphi$ is derivable in the proof system $\mathbb{K}$.
In the above, $\mathcal{K}$ is the language of $K$, and $\mathbb{K}$ is the axiomatisation of $K$. Validity means that for all pointed models $M_s$ we have $M_s \models \varphi$.
The classic way to prove Completeness is by proving the contrapositive:
Completeness (Contraposition): For all $\varphi \in \mathcal{K}$, if $\varphi$ is not derivable, then, then $\varphi$ is not valid.
The trick here is, similar to your PL example, to establish the connection between the notion of satisfiability, and the set theoretic notion of membership. In particular, again, similar to your PL example, we provide deductively closed maximal consistent sets that, intuitively, depict all possible consistent valuations of all formulas of your logic. Naturally, there are infinitely many ways to satisfy formulas of $\mathcal{K}$, and, hence, there are infinitely many maximal consistent sets.
The canonical model is that crucial link in the construction that allows us to go back and forth between formula belonging to a MCS $x$, and being true in a model, where $x$ is one of the states. Having this in mind, it is, hopefully, a bit more clear why $V^\Lambda$ and $R^\Lambda$ are defined that way (we mimic the semantics of modal logic with the set-theoretic membership).
After having established this, the proof is usually straightforward. You assume that $\varphi$ is not derivable, and hence $\{\lnot \varphi\}$ is a consistent set, then you extend the set to a MCS (Lindenbaum) $x$ such that $\lnot \varphi \in x$, then 'jump' to modal logic semantics $M^\Lambda_x \models \lnot \varphi$, and get the result.
Going to your question about the meaning of "Any normal modal logic is strongly complete with respect to its canonical model", remember that some modal logics require models to have certain properties (e.g. relations in $S5$ should be equivalences). Hence, there is usually an additional step of showing that your canonical model satisfies this properties.
Of course, there are also other interesting questions that could be asked about the canonical model. For example, does it have to be infinite? And I think it is answered in further chapters of Modal Logic.