Bull's theorem by the method of diagrams (Q1288961)

The method of finite diagrams, which is actually an adaptation of the original Kripke semantic tableau method, is applied to propositional modal logics -- normal extensions of K4.3, i.e. to logics of transitive linear Kripke frames. The completeness results for K4.3 and some of its extensions and Bull's Theorem (every normal extension of S4.3 has the fmp) are proved by this method. Reviewer's remark. Some proofs are slightly inaccurate. E.g. in the proof of Theorem 1.7, the last item of the construction of \(\Delta ^{k+1}\) should be replaced by the following two: \(= \Delta^k + \langle v_k , \neg \alpha_k \rangle\) if \(\Delta^k + \langle v_k , \neg \alpha_k \rangle\) is \(L\)-coherent, and \(= \Delta^k\) otherwise. The case (ii) in the proof of Lemma 2.1 should be corrected since \(\square \gamma \in [\square \delta_i ]\) for the only one \(i \leq n\). The argument in the case (i) in this proof is also not quite precise, but it can be clarified easily. The last occurrences of \(\rightarrow\) in formulas \((Dum)\) and \((Grz)\) should be replaced by \(\wedge\).