Non-tableau calculi for system K

Question

What proof calculi are there besides the method of analytic tableaux for System K?

The method of analytic tableaux is tricky to typeset and takes a lot of space, especially for modal logic.

I'm especially interested in alternatives that are more compact or easier to typeset. I'm also interested in alternatives that are worse by these criteria because it's nice to know what the options are.

---

I'm attempting to prove the following inference rule, which holds in system $K$.

$$ \frac{\square(A \to B) \;\; \text{and}\;\; \square(A)}{\square(B)}$$

By the truth conditions of negation in system K, this is equivalent to the following

$$ \frac{\square(A \to B) \;\; \text{and} \;\; \square(A) \;\; \text{and} \;\; \lnot\square(B)}{\bot} $$

Proving it using a world-labeled tableau is possible, but takes up a lot of space. I keep track of the accessibility graph of the worlds named so far with a list of accessibility assumptions up at the top.

accessibility assumptions:
⟨w,w'⟩ ∈ R


  w:□(A→B)
  w:□(¬A∨B)
    |
  w:□A
    |
  w:¬□B
  w:◊¬B
    |
  w':¬B
    |
 w':¬A∨B
    |
   w':A
  /    \
w':¬A   w':B     
  |        |
contra    contra

This particular tableau calculus allows elimination of $\lozenge$ by creating a fresh world and allows inferring $\varphi$ in any accessible destination world if $\square \varphi$ holds in the source world. Every proposition is explicitly labeled with the world where it holds. This is the method described here.

Answer 1

Historically, the first proof systems for normal modal logics were, not surprisingly, Hilbert systems. They are still heavily used in mathematical modal logic, because much work there is done in a model-theoretic vein and Hilbert systems come in handy for these purposes. That said, there are of course also natural deduction and sequent systems, but in the modal case these tend to get quite complicated and modal proof theory is still in its infancy. For a start on these non Hilbert systems I would suggest Heinrich Wansing's monograph 'Displaying Modal Logic', Dordrecht 1998.

In what follows I will outline the standard development of Hilbert systems for $K$ as found in the standard textbooks (Blackburn et al. 2000, Goldblatt 1990) and show how to justify the inference rule of interest.

Let a modal logic be a set of formulas containing all propositional tautologies and which is closed under modus ponens. A normal modal logic is a modal logic $\Phi$ that contains all instances of the $K$-axiom:

$\Box (\varphi \rightarrow \psi) \rightarrow (\Box \varphi \rightarrow \Box \psi),$

all instances of the duality-axiom:

$\neg \Diamond \varphi \leftrightarrow \Box \neg \varphi$

and is closed under boxing:

$\varphi \in \Phi \Rightarrow \Box \varphi \in \Phi$.

Obviously, for every set of formulas there is a smallest normal modal logic extending that set (the normal logic generated by the set). $K$ is then the normal logic generated by the empty set.

Finally, we can introduce a notion of derivability. For a normal modal logic $\Phi$, and a set of formulas $ \Psi \cup \{ \psi\}$ let $\psi$ be derivable from $\Psi$ in the logic $\Phi$, written $\Psi \vdash_{\Phi} \psi$, if $\psi \in \Phi \cup \Psi$.

It holds that $\{\Box(\varphi \rightarrow \psi), \Box \varphi\} \vdash_K \Box \psi$, since $\Box \psi$ is a member of $\Gamma:= K \cup \{ \Box(\varphi \rightarrow \psi), \Box \varphi \}$ which can be shown by the following sequence:

1. $\Box(\varphi \rightarrow \psi) \rightarrow (\Box \varphi \rightarrow \Box \psi) \in \Gamma $
2. $\Box (\varphi \rightarrow \psi) \in \Gamma$
3. $\Box \varphi \rightarrow \Box \psi \in \Gamma$ 1,2
4. $\Box \varphi \in \Gamma$
5. $\Box \psi \in \Gamma$ 3,4.