Tableau Calculus for Reflexive Frames

Question

How would you create a tableau calculus for modal logics that have reflexive frames? What rules would need to be added to the existing system K?

My attempt is to refer to the axiom scheme for reflexive frames and use it to devise rules that reflect the semantics of the scheme. There are typically two rules - one positive and one negative.

Positive rule: if a node $n$ has a formula $\Box p$ in it, then we can add $p$ to node $n$. Negative rule: if a node $n$ has a formula $\neg p$ in it, then we can add $\neg \Box p$ to node $n$. The intuition behind the positive rule is that if $p$ is necessarily true, then it must be true in all accessible worlds, including the actual world. Therefore, we can add $p$ to the current node. The negative rule, on the other hand, states that if $p$ is not true in the actual world, then there must be a possible world where $p$ is false. Therefore, we can add $\neg \Box p$ to the current node.

Does that seem correct? How can I prove a $\Box (\Box A \supset A)$ using this calculus?

Answer 1

Your rule, the way you have written it does not work.

Suppose you start with the negated conclusion $\lozenge(\square A \land \lnot A)$. None of your rules directly target $\lozenge$, so we're stuck.

Suppose we negate the conclusion by just adding $\lnot$ to the beginning. We're now start with $\lnot \square(\lnot \square A \lor A)$. I replaced the $\bigcirc \to \bigcirc$ with $\lnot\!\bigcirc \mathop\lor \bigcirc$ to make the resulting tableau easier to follow.

In this case as well, we are stuck and unable to make progress.

¬□(¬□A∨A)
|
¬□□(¬□A∨A)
|
¬□□□(¬□A∨A)
|
and so on

---

Your system has a deeper problem, though; it doesn't contain any machinery for working with possible worlds and keeping track of them.

Some explicit machinery for keeping track of worlds is necessary. $\lozenge (A \land B) \implies \lozenge A \land \lozenge B$ is valid, but $\lozenge A \land \lozenge B \implies \lozenge (A \land B)$ is invalid even in strong systems like the logic S5.

---

Here's how to prove it using a tableau calculus with labeled worlds. This is a tableau calculus that works for a variety of modal logics by choosing different rules for the accessibility relation. If the accessibility relation is reflexive, then we can conclude $wRw$ for any world $w$.

The negation of $\square (\square A \to A)$ is $\lozenge ( \square A \land \lnot A)$

OR1, 1R1

0:◇(□A∧¬A)
|
1:□A∧¬A
|
1:□A
|
1:¬A
|
1:A (contradiction)