Modal Logic - The Proof System $\mathbf K$
The proof system $\mathbf K$ has the following axioms:
- $T$ - All the (substitution instances of) validities of propositional logic.
- $\mathbf K$ - $\square(\phi\implies\psi)\implies(\square\phi\implies\square\psi)$.
and the following two rules:
- MP - If you have derived $\phi$ as well as $\phi\implies\psi$, then derive $\psi$.
- Necc - If you have derived $\phi$, then derive $\square\phi$.
We write: if $\phi$ is derivable in $\mathbf K$, we write $\vdash_K\phi$.
Example of a Proof in $\mathbf K$
We want to show: $\vdash_K\square(p\wedge q)\implies\square p$
| Step | Expression | Justification |
|---|---|---|
| 1 | $(p\wedge q)\implies p$ | $T$ |
| 2 | $\square((p\wedge q)\implies p)$ | Necc(1) |
| 3 | $\square((p\wedge q)\implies p)\implies(\square(p\wedge q)\implies\square p)$ | $\mathbf K$ |
| 4 | $\square(p\wedge q)\implies\square p$ | MP(2, 3) |
Reasoning: Allowed because it is obtained from 2 and 3 using the rule MP.
Abbreviations & Conveniences
As $\lozenge\phi$ is an abbreviation for $\neg\square\neg\phi$, we can switch between writing $\lozenge$ and $\neg\square\neg$ at will.
We don’t need a justification to do this.
Additionally, as proofs in $\mathbf K$ tend to contain very long formulas, we can substitute line numbers instead of expressions:
| Step | Expression | Justification |
|---|---|---|
| 1 | $(p\wedge q)\implies p$ | $T$ |
| 2 | $\square(1)$ | Necc(1) |
| 3 | $(2)\implies(\square(p\wedge q)\implies\square p)$ | $\mathbf K$ |
| 4 | $\square(p\wedge q)\implies\square p$ | MP(2, 3) |
You should keep this to a minimum in order to keep the proof readable.
Soundness & Completeness
The system $\mathbf K$ is well-designed:
- If $\vdash_k\phi$ then $\vDash\phi$
- So $\mathbf K$ is sound.
- If $\vDash\phi$ then $vdash_K\phi$
- So $\mathbf K$ is complete.
We don’t have to prove any questions like this in the exam.
Strategies for Finding Proofs in $\mathbf K$
If your expression can’t be proven using an axiom or rule, then the following rules can be helpful:
Suppose you want to show that $\vdash_K\phi$, and that $\phi$ cannot be derived using $T,K$ or Necc. Therefore you must prove $\phi$ using MP.
This means we must:
- Choose a formula $\psi$
- Derive $\psi$.
- Derive $\psi\implies\phi$.
It may help to work backwards in a situation like this.
Completing a lot of examples is the best way to gain an understanding of how to derive $\psi$. However, the following can also help:
- $\psi\implies\phi$ is often an instance of $T$.
- $\psi$ tends to have lots of $\square$ and $\implies$, few $\lozenge$ and $\neg\square$.
Additional Example of a Proof in $\mathbf K$
Show $\vdash_K\lozenge p\implies\lozenge(p\vee q)$:
| Step | Expression | Justification |
|---|---|---|
| $n$ | $\neg\square\neg p\implies\neg\square\neg(p\vee q)$ | MP($n-2, n-1$) |
| $n-1$ | $(n-1)\implies(n)$ | $T$ |
| $n-2$ | $\square\neg(p\vee q)\implies\square\neg p$ | MP($n-3, n-4$) |
| $n-3$ | $(n-4)\implies(n-2)$ | $\mathbf K$ |
| $n-4$ | $\square(\neg(p\vee q)\implies\neg p)$ | Necc($n-5$) |
| $n-5$ | $\neg(p\vee q)\implies\neg p$ | $T$ |
This is proven in reverse and hence the steps are in reverse. We will have to renumber the table for this to be a valid proof.