One-step modal logics, intuitionistic and classical. I (Q2240542)

This paper is the first part of the author's two-parts laborious articles with the same title. 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. Natural deduction sytems of classical modal logic $\mathbf{CK}$ and its intuitionistic version $\mathbf{IK}$ are constructed using marked formulas. Their completeness theorems are proved. Their consequence relations are also considered. This paper is heavily due to the model-theoretic concepts proposed in [\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})]. 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. In this proof-theoretic systems, simply speaking, 0-prefixed formulas are thought of as axioms. 1-prefixed formulas are the deduced ones by rules. It seems to me that this labeling system is too simple and superfluous in a technical sense. However, I think that those step-makers have some philosophical meanings that 0 is corresponded to actual (real) state and so is 1 to subjective one as analogies. Although the author of this paper for examples takes 0$\bot$ and 1$\bot$ as false, I, in this sense, think the truth value of 1$\bot$ may be recognized as one having more variety of different meanings. Similarly thought to 1$\top$. The author of this paper foretells that Part 2 will investigate one-step proof-theoretic systems formalizing intuitionistic and classical one-step versions of some familiar logics stronger than $\mathbf{K}$.