This paper studies modal logics whose extensions all have the finite model property, those whose extensions are all recursively axiomatizable, and those whose extensions are all finitely axiomatizable. We call such logics FMP-ensuring, RA-ensuring and FA-ensuring respectively, and prove necessary and sufficient conditions of such logics in $$\mathsf {NExtK4.3}$$. Two infinite descending chains $$\{{\textbf{S}}_{k}\}_{k\in \omega }$$ and $$\{{\textbf{S}} _{k}^{*}\}_{k\in \omega }$$ of logics are presented, in terms of which the necessary and sufficient conditions are formulated as follows: A logic in (...) $$\mathsf {NExtK4.3}$$ is FMP-ensuring iff it extends $${\textbf{S}}_{k}$$ for some $$k\in \omega $$, it is RA-ensuring iff it extends $${\textbf{S}}_{k}^{*}$$ for some $$k\in \omega $$, and it is FA-ensuring iff it is finitely axiomatizable and extends $${\textbf{S}}_{k}^{*}$$ for some $$k\in \omega $$. (shrink)

We generalize the theory of canonical formulas for K4, the logic of transitive frames, to wK4, the logic of weakly transitive frames. Our main result establishes that each logic over wK4 is axiomatizable by canonical formulas, thus generalizing Zakharyaschev’s theorem for logics over K4. The key new ingredients include the concepts of transitive and strongly cofinal subframes of weakly transitive spaces. This yields, along with the standard notions of subframe and cofinal subframe logics, the new notions of transitive subframe and (...) strongly cofinal subframe logics over wK4. We obtain axiomatizations of all four kinds of subframe logics over wK4. We conclude by giving a number of examples of different kinds of subframe logics over wK4. (shrink)

We prove that all finitely axiomatizable tense logics with temporal operators for ‘always in the future’ and ‘always in the past’ and determined by linear fows time are coNP-complete. It follows, for example, that all tense logics containing a density axiom of the form ■n+1F p → nF p, for some n ≥ 0, are coNP-complete. Additionally, we prove coNP-completeness of all ∩-irreducible tense logics. As these classes of tense logics contain many Kripke incomplete bimodal logics, we obtain many natural (...) examples of Kripke incomplete normal bimodal logics which are nevertheless coNP-complete. (shrink)