I'm trying to come up with a tableau method similar to the ones described here, but without deleting formulas, explicitly naming worlds, or spawning new tableaux as subproblems. I think the tableau calculus described in this question is similar to (and possibly identical to) the set-labeled tableau entry in the linked article.
I'm wondering whether it's okay to introduce fresh predicates to distinguish between different worlds when breaking down
LAxy into syntactically simpler subexpressions. In both of those cases, I'm introducing a fresh variable
w to reify how some "choice" is made across worlds and then showing that it can't be made consistently. Does this operation preserve satisfiability when
w is fresh?
I have some rules inherited from classical logic✱ and the following rules for eliminating toplevel modal connectives.
I'm intentionally being vague about which system of modal logic I'm working with. I'd like to be able to exhibit calculi for S4 and S5, for instance, that are mostly the same except for which literals form "self-annihilating pairs".
p and possibly
q is unsatifisiable if and only if
q are both unsatisfiable.
MApq ◇(p∨q) / \ / \ Mp Mq ◇p ◇q
distribution of necessity over conjunction
LKpq ◻(p∧q) | | Lp,Lq ◻p,◻q
These other two potential rules are where I'm unsure. Here I'm getting rid of a toplevel necessity+disjunction by introducing a fresh world-splitting variable
w. The argument is that if it was possible before to "cover" all of the possible worlds with at least one of
q, chosen independently for each world, then we can come up with a "choice function" of sorts that picks
q by returning
false. If both
q hold at some particular world, then
w is unconstrained, but still has to pick something.
LApq ◻(p∨q) | | Cwp,CNwq w→p,(¬w)→q
A similar argument holds, potentially, for breaking down
MK. But this time I want my world-splitter
w to pick out at least one world in which
q are both true, and have that be the only thing it does. Also,
w can't always be false.
MKpq ◇(p∧q) | | Cwp,Cwq,Mw w→p,w→q,◇w
Here is a tableau proof (assuming the system I've sketched works) of the distributive law
NCLCpqCLpLq | LCpq,NCLpLq | LCpq,Lp,NLq | LANpq,Lp,NLq | CwNp,CNwq,Lp,NLq / \ Nw,CNwq,Lp,NLq [[Np]], CNwq, [[Lp]], NLq / \ / \ [[Nw]],[[w]],Lp,NLq Nw,[[q]],Lp,[[NLq]]
✱ I'm using rules for
NC, so the original formula doesn't need to be written in negative normal form.