Minimal Modal Logic and the Class of all Kripke Models

It's well known that minimal modal logic (i.e. propositional tautologies and axiom $K$ together with modus ponens and necessitation rule) captures the validities of the semantic class of all Kripke models. Looking for the proof.

• – Thiago Nascimento Nov 16 '17 at 13:22
• @ThiagoNascimento Thanks. It's a different question, but reminded me of what I was missing. – LoMaPh Nov 16 '17 at 21:19

The proof is basically proof of soundness and completeness of Minimal Modal Logic with respect to the class of all Kripke models. I mention it here in simple terms.

Let $K$ be the minimal modal logic (We drop the subscript $K$ in consequence relations for simplicity).

Soundness: If $\ \vdash\phi\$ then $\ \vDash\phi\$

Proof is straightforward. We just need to prove that axioms are valid and rules (modus ponens and Necessitaion) preserve validity.

Completeness: If $\ \vDash\phi\$ then $\ \vdash\phi\$.

Proof: We prove the contrapositive; i.e. if $\ \nvdash\phi\$ then $\ \nvDash\phi\$.

Lemma 1. If $\ \nvdash\phi\$ then $\neg\phi$ is consistent.

Lemma 2. Any consistent set of formulas has a satisfying model (i.e. there is a model $M$ and world $w$ such that for every formula $\phi$ in the set we have $M,w\vDash \phi$).

Suppose $\nvdash\phi$. From Lemma 1 and 2 it follows that $\neg\phi$ has a satisfying model. So there exist $M$ and $w$ such that $M,w\nvDash \phi$. So $\ \nvDash\phi.\qquad$ QED.

Proof of Lemma 1. (source) For the sake of obtaining a contradiction assume that $\neg\phi$ is inconsistent. So for any $\psi$ we have $\neg\phi\vdash \psi$. In particular this holds for negation of a theorem $\tau$ (theorem means $\vdash \tau$), $\neg\phi\vdash \neg \tau$. By deduction theorem we get $\vdash \neg\phi\rightarrow \neg\tau$. Since $\tau$ is a theorem we have $\vdash\neg \neg\tau$. From these two, we get $\vdash\neg\neg\phi$ and then $\vdash\phi$ which contradicts the premis. $\qquad$ QED.

Definition 1. A maximally consistent set is a consistent set that every proper superset of it is inconsistent (equivalently, for every formula $\phi$, either $\phi$ is in the set or $\neg\phi$).

Definition 2. The canonical model for $K$ is the model $M^c=\langle W^c,R^c,V^c\rangle$ where

• $W^c=\{\Gamma \ |\ \Gamma \text{ is a maximally consistent set}\}$
• $\Gamma R^c\Delta \ \text{ iff }\ \{\phi\ |\ \square\phi\in\Gamma \}\subseteq\Delta$
• $V^c(p) = \{\Gamma \ |\ p\in\Gamma \}$

Proof of Lemma 2: (source)
Lemma 3. Every consistent set of formulas can be extended to a maximally consistent set.
Lemma 4. For every formula $\phi$ we have $\ M^c,\Gamma\vDash \phi \ \$ iff $\ \ \phi\in \Gamma$.

Let $\Sigma$ be a consistent set. By Lemma 3 we can extend it to a maximally consistent set $\Sigma'$ (note that $\Sigma\subseteq \Sigma'$). By Lemma 4 (right to left), for every formula $\phi\in \Sigma'$ we have $\ M^c,\Sigma'\vDash \phi$. Since $\Sigma\subseteq \Sigma'$ we can say for every formula $\phi\in \Sigma$ we have $\ M^c,\Sigma'\vDash \phi$. This means that $\Sigma$ is satisfiable. $\qquad$ QED.

Proof Sketch of Lemma 3. (source)
Let $\Sigma$ be a consistent set. "Enumerating all (countably many) formulas of the modal language: $\phi_1, \phi_2, \ldots$ and then, starting from $\Sigma$, working stage by stage, adding the currently scheduled formula if it is still consistent with those already chosen. In the countable limit, the result of this is still consistent, since by our definition, an inconsistency can only involve finitely many formulas, and hence it would already have shown up at some finite stage. It is easy to see that the preceding construction yields a maximally consistent set."

Proof of Lemma 4. (see page 4 of this file)