logicandlanguage.net

See
http://www.ucalgary.ca/~rzach/logblog/2005/04/modal-logic-textbooks.html

I've used F&M, and I like it a lot. it does use tableaux as the primary proof system, though, and as the title suggests, it focusses on first-order stuff. So less discussion of various systems for epistemic, deontic, etc., logic; more on possible objects, de re and de dicto quantification, definite descriptions, etc.

Speaking as one who also loves and respects the
same logicians (I'm one of JC's students), I can sympathize with your desire to use an axiomatic system.

A colleague
of mine recommended James Garson's recent book,

Modal Logic for Philosophers (2006). Its main approach is to define on the various modal logics by axioms. E.g. T is K plus []A -> A. However, it does much much more. It covers natural deduction, tableaux, a bit on the model theory of the various versions of modal logic, soundness and completeness, lambda asbstraction, definite descriptions, various semantics for QML, coverting between tableaux and natural deduction, etc.
It's been helpful to dip into the book when I had questions about QML.

So it might do the trick for you. However, I must say that I'm glad I worked through JC's book first before I dipped into this one, mainly because JC's book was great at helping me figure out why a model works the way it does, so that certain inferences turn out valid.

PS: What's wrong with tableaux? I mean, to prove things, axiomatic systems aren't exactly convenient.

I used to sort of (kind of) like the Fitting & Mendelsohn book, but no longer. Even if you wanted to do QML I would still recommend Chellas' "Modal Logic: An Introduction", and then use supplementary material for QML, like Garson's excellent "Quantification in Modal Logic" (1984) in the Handbook of Philosophical Logic.

As already mentioned, the Fitting & Mendelsohn book is geared toward metaphysics, and though it introduces axiomatic systems, it does so just barely. Tableaux take centre stage, which is no surprise since Fitting is the author.

There's nothing cool like modalities reductions (in H&C) or classical modal logic (i.e. those weaker than K--Chellas), filtration, etc...I feel like I got way more out of Chellas than F&M in terms of learning modal logic (rather than its philosophy).

Who wants to buy my F&M book? $8? Like new. Just burned around the center.

Thanks for your comments everyone. What do I have against tableaux proof systems? It's not that I think that axiomatic systems are convenient to use - obviously they're not. But I think it's important for students to understand them (and that means at least doing one or two simple proofs using them) because they're so often used to characterise proof systems (e.g. S4, arrow-fragments of propositional logics, etc.) As a result they get used a lot in the research literature, and so you need to have a decent grasp of axiomatic systems to read logic research papers. And of course, sometimes there are logics for which we only have axiomatic proof systems.

I'm also sympathetic to having natural deduction proof systems as the central proof method in logic textbooks, since I think that good natural deduction systems are much easier to use and come much closer to characterising rules of proof that we use pretheoretically. So I think it's useful for my students to have a good grasp of those two styles of proof system.

But right now - and I'm willing to be convinced otherwise - I don't really care if they never learn how to use tableaux. The problem with tableaux is that they don't have either of the advantages of the other two methods. The advantage that people usually cite, of course, is that they make completeness proofs easier. Completeness is important, of course, but ease of that one metatheoretic proof isn't important enough to me to want to make my students learn another style of formal proof.