Lots of new stuff in the Open Logic repository! I’m teaching modal logic this term, and my ambitious goal is to have, by the end of term or soon thereafter, another nicely organized and typeset open textbook on modal logic. The working title is *Boxes and Diamonds*, and you can check out what’s there so far on the builds site.

This project of course required new material on modal logic. So far this consists in revised and expanded notes by our dear late colleague Aldo Antonelli. These now live in `content/normal-modal-logic`

and cover relational models for normal modal logics, frame correspondence, derivations, canonical models, and filtrations. So that’s one big exciting addition.

Since the OLP didn’t cover propositional logic separately, I just now added that part as well so I can include it as review chapters. There’s a short chapter on truth-value semantics in `propositional-logic/syntax-and-semantics`

. However, all the proof systems and completeness for them are covered as well. I didn’t write anything new for those, but rather made the respective sections for first-order logic flexible. OLP now has an `FOL`

“tag”: if `FOL`

is set to true, and you compile the chapter on the sequent calculus, say, you get the full first-order version with soundness proved relative to first-order structures. If `FOL`

is set to false, the rules for the quantifiers and identity are omitted, and soundness is proved relative to propositional valuations. The same goes for the completeness theorem: with `FOL`

set to false, it leaves out the Henkin construction and constructs a valuation from a complete consistent set rather than a term model from a saturated complete consistent set. This works fine if you need only one or the other; if you want both, you’ll currently get a lot of repetition. I hope to add code so that you can first compile without `FOL`

then with, and the second pass will refer to the text produced by the first pass rather than do everything from scratch. You can compare the two versions in the complete PDF.

Proofs systems for modal logics are tricky; and many systems don’t have nice, say, natural deduction systems. The tableau method, however, works very nicely and uniformly. The OLP didn’t have a chapter on tableaux, so this motivated me to add that as well. Tableaux are also often covered in intro logic courses (often called “truth trees”), so having them as a proof system included has the added advantage of tying in better with introductory logic material. I opted for prefixed tableaux (true and false are explicitly labelled, rather than implicit in negated and unnegated formulas), since that lends itself more easily to a comparison with the sequent calculus, but also because it extends directly to many-valued logics. The material on tableaux lives in `first-order-logic/tableaux`

.

Thanks to Clea Rees for the the `prooftrees`

package, which made it much easier to typeset the tableaux, and to Alex Kocurek for his tips on doing modal diagrams in Tikz.

Richard, the use of prefixes for modal tableaux is really nice! I’ve found it really helpful for teaching basic modal logic in an intermediate course. One question: why do you prefer using signed formulas rather than just expressing the tableaux rules in terms of negation?

Two reasons: a) it makes the parallel with the sequent calculus clear(er). b) It generalizes to many-valued logics. (b) isn’t so much an issue for modal logic unless you want to do many-valued modal logic, but I wanted to keep the same structure for the modal and non-modal case and to generalize the non-modal case to many-valued logics — as I plan to do eventually — the straightforward way to do it is to allow a sign for every truth value.)

Right, thanks, I suspected that might be the reason — a good one overall, of course. Perhaps it might be useful to mention the possibility of using non-signed alternatives for folks just interested classical logic and want to base their presentations on the texts? (I’m planning to do this when I teach my intermediate undergrad logic course again next spring.) The signs do seem to me to add a bit of needless clutter for those cases and perhaps complicate things a bit conceptually for students who’ve only had an intro course.

I’ll see if I can make it configurable … https://github.com/OpenLogicProject/OpenLogic/issues/176

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.

Am I confused here? Or am I perhaps trying to get the tableaux system to do more than it’s designed for by insisting it yield a decision procedure? (Though of course that’s exactly what we get in the non-modal propositional case.)

Very good point: https://github.com/OpenLogicProject/OpenLogic/issues/178