Modal tableau calculi and interpolation (Q798647)

The paper shows that all the propositional modal calculi over the language whose connectives are \(\neg\), \(\wedge\), \(\square\) and \(\bigcirc\) (falsum) and which possess a complete tableau system have the interpolation property, provided that the tableau rules satisfy certain conditions. These conditions include a wide class of normal modal calculi. The author also presents tableau systems for several modal calculi (including B, K4, G, Gr and extensions) and proves by constructive methods the completeness of those tableau systems with respect to appropriate Kripke semantics. It is shown, specifically, that the finite model property holds for those systems, which also satisfy the remaining conditions for the interpolation property. The problem of the existence of the interpolation property is discussed for various other examples, in particular for some classes of extensions of K4, G and Gr.