rzach
commented
6 years ago See Chris Menzel's comment at http://openlogicproject.org/2018/02/22/modal-logic-propositional-logic-tableaux/#comment-6295
I have a question about the simplified S5 tableaux rules (though I’m pretty sure it generalizes). I could well be confused or missing something, since (to my embarrassment) I’ve never really looked seriously at modal tableaux before about three weeks ago, but it seems that the rules as stated can generate infinite trees for satisfiable sets when simple finite trees will do. For instance, consider {□◇p}. Taken at face value, the rules seem to generate the following infinite tree since, in particular, the rule ◇T requires a conclusion with a new prefix and the notion of a complete branch requires a conclusion to □T for every prefix (I’m going to suppress the T’s since no negations are involved): 1 □◇p 1 ◇p 2 p 2 ◇p 3 p 3 ◇p 4 p 4 ◇p … Intuitively, though, we should just be able to stop after the fourth line here — that’s clearly all you need to construct a model for {□◇p}. Of course, if all we’re concerned with is that our rules be complete, the simplified rules are fine as they are. But it seems that they could also yield a simple decision procedure if, e.g., the rule for ◇T were modified along the following lines: n T ◇φ ——— m T φ where m is new, unless there is some k such that “k T φ ” is already on the branch. Analogously, of course, for the rule □F. This rule would permit us to terminate the above tableau after the fourth line. The effect of this, I think, is simply to recreate the decision procedure for S5 in Hughes and Cresswell, which only forces us to introduce a new world for (true) ◇φ when there isn’t one already in which φ is true. The revised rule also seems compatible with the relevant clause in the definition of a complete branch on pp. 597-8 of the OLP text, although a slight revision might be called for: 3. at least one possible conclusion in the case of modal rules that require (when necessary) a new prefix. Of course, the idea of a “possible conclusion” would have to be clarified so that a prior occurrence of “k T φ” on a branch would count as one.
The systems discussed in the modal tableaux chapter all have the fmp, but some systems produce infinite tableaux if the assumptions are satisfiable. These yield infinite counterexamples, so no problem for completeness. It would be nice if the systems could be refined to yield decision procedures.