Linear reasoning in modal logic

In [1] Craig introduced a proof procedure for first order classical logic called linear reasoning. In it, a proof of P ⊃ Q consists of a sequence of formulas, each of which implies the next, beginning with P and ending with Q. And one of the formulas in the sequence will be an interpolation formula for P ⊃ Q. Indeed, this was the first proof of the Craig interpolation theorem, some of whose important consequences were demonstrated in a companion paper [2]. In this paper we present systems of linear reasoning for several standard modal logics: K, T, K4, S4, D, D4, and GL. Similar systems can be constructed for several regular, nonnormal modal logics too, though we do not do so here. And just as in the classical case, interpolation theorems are easy consequences. Such theorems are well known for the logics considered here. There is a model theoretic argument in [6], an argument using Gentzen systems in [8], an argument using consistency properties in [4] and [5], and an argument using symmetric Gentzen systems in [5]. This paper presents what seems to be the first modal proof that follows Craig's original methods. We note that if the modal rules given here are dropped, a classical linear reasoning system results, which is related to, but not the same as those in [1] and [10].Since the basic linear reasoning ideas are fully illustrated by the propositional case, we present that first, to keep the clutter down. Later we show how the techniques can generally be extended to encompass quantifiers. We do not follow [1] in making heavy use of prenex form, since it is not generally available in modal logics. Fortunately, it plays no essential role.