a few questions about modal analogs to Kahlmar's theorem and also natural deduction systems for nonmonotonic logics

One of the great things I've been doing this summer is work through Alex Simpson's dissertation, which treats modal logics from a proper natural deduction standpoint (with intro and elim rules for each operator, and demands like harmony and conservative extension requirements). It's really beautiful stuff, translates into a Fitch style natural deduction system really well (Simpson uses a Prawitz style tree system), and also raises a number of interesting philosophical questions.

One of the things I've been messing with for the last hour is trying to come up with meta-logical proof theory for the way Kripke style counterexamples work. I think if you have a non-monotonic logic you can do this pretty elegantly. So consider the following.

1. a: ~P
2. b: P
3. aRb
4. a: []P                    3/2 [] intro
5. | a: []P --> P         assumption for ~ introduction
6. | a: P        4,5       --> elimination
7. | a: #        1,6       ~ elimination
8. a: ~([]P --> P)        5-7 ~ introduction

The lower case letter to the left of the colon is the world at which the proposition to the right of the colon is true. The first three premises describe a K model that counterexemplifies the T axiom. They say that P is true at world b, that world b is accessible from a, and that ~P is true at a. The proof shows that the axiom is false in this K model and hence not a theorem of K.

There is one really important thing about this though. The [] intro rule has to be read in a really specific way. The only reason []P follows from b: P and aRb is because we know that premise 3 gives all of the accessibility relations in question. But this makes the provability relation in question non-monotonic. Consider the following.

All we do is add two premises to the previous three, making the accessibility relation reflexive, so that we have a T model now (the previous three were a K model and, given that premise 3 stated the only accessibility relation in question, not a T model).

1. a: ~P
2. b: P
3. aRb
4. aRa
5. bRb

Since a is accessible from itself, and P is false at a, it would not follow that []P is true at a (there is a world accessible from a where P is false).

It's not hard to actually write out a box introduction rule that takes this into account- if you are inferring box P at world a, then every line where some world is accessible from a needs to be cited, and one needs to cite premisses where P is true at every one of those worlds. And clearly with such a rule the system is non-monotonic. We add the premise that a is accessible from itself, and the proof is no longer valid.

From a presentation I went to fifteen years ago I know that at least some non-monotonic logics work this way, with a presumption that the premises give a complete description of the relevant states of affairs. So I have two questions: (1) Has anyone done the kind of thing Simpson has done for modal logic with non-monotonic logic? Presenting them in a proper natural deduction system with introduction and elimination rules for each operator, and where you can raise questions of harmony and conservativity? (2) Has anyone done anything like what I've done above with the proof theory of Kripke models? It's so obvious that I'd think someone has. (3) There are a set of theorems in the neighborhood of Kahlmar's theorem about propositional logics (for any row of a truth table, if the sentence is true on that table one can prove in intuitionistic logic the sentence from the set of atoms and negated atoms correspondint to the Ts or Fs assigned by that row, and one can prove the negation of the sentence from the same if the sentence is false on that row) sitting around here. I don't know how interesting these are, since they probably follow pretty directly from the finite model property and decision procedures involving tree systems (not Prawitz trees, the other kind that yield easy decision procedures). Any intuitions? (4) The way I've got it above it probably will work for any propositional modal logic with the finite model property. Is the prospect for something analogous hopeless with respect to modal predicate logic? There are analogues to Kahlmar's theorem for predicate logic, which show for any non-logical truth there exist a set of sentences all below some threshold in the hierarchy that prove the negation of that sentence. Would these same analogues apply directly to modal predicate logics? (5) My intuition is that the proof question in system works if you just take Simpson's K rules and buttress them with additional box intro and diamond elim rules of the kind that impose non-monotonicity, and would not need to add extra rules for the different modal systems (given that we're forced to make the accessibility relations right to get the kind of model in question in any case). I haven't tested this yet, but the way the T axiom works above seems right. You can counterexemplify it with a K model, and can't with a T model. And you can prove it in Simpson's T. I think this kind of thing should probably work for all the Simpson logics.

[The philosophical interest of this kind of thing follows from a neglected article by Neil Tennant, which I discussed HERE. The above proofs do what Tennant demands that proof theoretic replacements of countermodels do. At some point I'm going to do a companion post to the earlier post. If by completeness one means the intuitionistically strong claim that there is either a countermodel or a proof, then (given the validity of the disjunction property) one can produce a much quicker argument that undecidable theories are incomplete for intuitionists. If I had thought of that with the previous post, the discussion would have been clearer. I also should have been clearer that I thought the fact that Tennant's proposal entailed incompleteness was evidence for Tennant's proposal. Given the thing about the disjunction property, this is considerably clearer.]