One-step modal logics, intuitionistic and classical. II (Q2240543)

This paper is the last part of the author's two-parts laborious articles with the same title, that is, the sequel of [the author, J. Philos. Log. 50, No. 5, 837--872 (2021; Zbl 1497.03039)]. In [loc. cit.], the author introduces marked formulas which are the result of prefixing a formula in a propositional modal language with a step-marker, for this paper either 0 or 1. The step-marker 1 is thought of as indicating the taking as one step away from 0. In [loc. cit.], natural deduction sytems of classical modal logic \(\mathbf{CK}\) and its intuitionistic version \(\mathbf{IK}\) are constructed using marked formulas. This paper continues that project (that of one-step systems), addressing some familiar classical strengthenings of \(\mathbf{K}\) (\(\mathbf{D}\), \(\mathbf{T}\), \(\mathbf{K4}\), \(\mathbf{KB}\), \(\mathbf{K5}\), \(\mathbf{Dio}\) (the Diodorian strengthening of \(\mathbf{K}\)) and \(\mathbf{GL}\)), and their intuitionistic counterparts (see [\textit{G. Plotkin} and \textit{C. Stirling}, ``A framework for intuitionistic modal logics'', in: Proceedings of the first conference on theoretical aspects of reasoning about knowledge, Monterey, CA, USA, 1986. Los Altos, CA: Morgan Kaufmann Publishers. 399--406 (1986; \url{doi:10.1016/B978-0-934613-04-0.50032-6})] for some of these counterparts). This paper is heavily due to the model-theoretic concepts proposed in [loc. cit.]. This paper is, \textit{in a sense}, a proof-theoretic working-out version of Plotkin and Stirling's paper from a point of view of marked formulas and corresponding deductions with step-makers 0 and 1. Their (weak) completeness theorems are proved. And their consequence relations are considered.