Fdtxjr

How do you decide whether a potential rule is allowed or not for a tableaux calculus for a given modal logic such as system K?

In particular, I'm curious whether this rule:

$$ fracsquare A_1; square A_2; dots; square A_n; lozenge BA_1; A_2; dots A_n; B tagK $$

Can be replaced with a different one that leaves all statements headed by a modal operator except for $D$ untouched.

$$ fraclozenge A_1cdotslozenge A_n ; square B_1 cdots square B_n; C_1 cdots C_n ; lozenge Dlozenge A_1 cdots lozenge A_n; square B_1 cdots square B_n; D tagFAKE-K $$

And, moreover, I'm curious if there's a way to think about the rules in this sort of proof calculus so that they fall directly out of the presentation of a given modal logic.

I'm trying to get a better understanding of set-labeled tableau calculi. Most of the diagrams in the Wikipedia article on the method of analytic tableaux show non-set-labelled calculi, which are more compact because nodes "above you" in the tree are accessible for forming contradictions.

Here's a proof of the consequentia mirabilis in propositional logic (101), written in a modified form of Polish notation with ! as negation instead of N.

Figure 101
Tableau for consequentia mirabilis

 Goal: CC!aaa
 Goal: A!A!!aaa
 Goal: A!Aaaa
 Goal: AK!a!aa
Negated Goal: KAaa!a

 KAaa!a
 |
 Aaa,!a
 / 
 a,!a a,!a
 | |
 ⊥ ⊥

I then tried to create a tableau for the distribution axiom of system K (102).

I deliberately avoided using rule K to eliminate the possibility operator at (103) and instead retained the outermost connectives as is permitted by (FAKE-K). At 104 and 105, I used a statement headed by necessity to get a fact about the current world.

Figure 102
Tableau for distribution axiom in system K

 Goal: CLCpqCLpLq
 Goal: A!LA!pqA!LpLq
 Goal: AMKp!qA!LpLq
 Goal: AMKp!qAM!pLq
Negated Goal: KLA!pqKLpM!q

 KLA!pqKLpM!q
 |
 LA!pq,KLpM!q
 |
 LA!pq,Lp,M!q
 |
 LA!pq,Lp,q (103)
 |
 LA!pq,A!pq,Lp,q (104)
 |
 LA!pq,A!pq,Lp,p,q (105)
 / 
 LA!pq,!p,Lp,p,q LA!pq,q,Lp,p,q
 | |
 ⊥ ⊥

There's a helpful rule for dealing with the possibly operator (M) written schematically in the section of the same article on set-labeling tableau for modal logic. Even though the article calls this kind of tableau set-labeling and the verbose kind of tableau for propositional logic set-labeled, I think it's reasonable to consider them the same kind of proof calculus.

The rule K looks like this (K). It's immediately clear what the rule means intuitively: you're entering a possible world. You are allowed to strip away one possibility operator ... for a price. The other conditions in your set must all have $square$/L as their top-level connective, this connective is then removed when entering the possible world.

$$ fracsquare A_1; square A_2; dots; square A_n; lozenge BA_1; A_2; dots A_n; B tagK $$

However, there's an alternative way to formulate this rule (FAKE-K). In FAKE-K, you get to remove one possibility operator when entering a possible world, but you don't impose any preconditions on the other elements of the set. Instead, you drop any expressions that are not headed by a modal operator. Expressions headed by a modal operator are retained regardless of whether that modal operator is $lozenge$ or $square$.

$$ fraclozenge A_1cdotslozenge A_n ; square B_1 cdots square B_n; C_1 cdots C_n ; lozenge Dlozenge A_1 cdots lozenge A_n; square B_1 cdots square B_n; D tagFAKE-K $$

I'm curious whether (FAKE-K) results in a more powerful system and therefore results in something that isn't a proof calculus for system K. The intuition behind it is that resolving a possibility operator removes all of the statements that refer to the currently focused world, but all of the statements that do not make reference to the currently focused world untouched except for $D$. Since $D$'s possibility operator is removed, repeatedly applying rule (FAKE-K) does not allow us to enter a world where multiple expressions governed by possibility are satisfied simultaneously.