Arithmetical completeness theorems for monotonic modal logics (Q6040616)

Since the well-known arithmentical completeness of the normal modal logic GL has been established by Solovay, the formal analysis of provability predicates by means of modality is developing in many directions so rapidly. It may be worth noting that the provability predicates considered for GL there are formalized uniformly, so that the completeness result enjoys the canonicity as well. In other words, the provability predicates to be discussed are required to satisfy the so-called `canonical' derivability conditions D1--D3; D1; the principal condition such that any provability predicate should satisfy (or necessitation rule in the modal counterpart): D2; the distributivity of provability predicate with respect to implication (or K-axiom in the modal counterpart); D3; the provability of provable sentences (or 4-axiom in the modal counterpart). Obviously the basic modal logic to support the analysis must be the normal modal logic K4. This is important because, for example, consistency statements given by some modal axioms might be shown to be equivalent according to the normality. In other words, the modal analysis of such consistencies are not possible in this framework. On the other hand, by the development of a finer study of provability predicates by many authors such as Bernardy, Montagna, Arai, and so on, the non-canoical ones are found, which sometimes provide the second incompleteness theorem as well. Among others, the Rosser provability predicate is one of them. It satisfies the monotone rule in place of the stronger condition D2. The authors of this paper focus on this characteristics of Rosser provability predicates, and then enlarge the framework of modal analysis to the monotone. On the basic logic MN, not only the 4-axiom but also two more additional modal axioms denoted by P and D are considered, where P and D express the consistency repectively but they are shown to be equivalent in a normal modal setting. Thus, the main objective of this paper is to establish the arithmetical completeness of these MN-logics. For monotone modal logics, a Kripke-type relational sematics has been established by \textit{M. C. Fitting} et al. [J. Log. Comput. 2, No. 3, 349--373 (1992; Zbl 0819.03011)], so that the authors first prove that each of these logics enjoys a finite model property. Then Solovay's proof method of arithmetrical completeness is essentially applied on the obtained finite model. Thus, the two consistency statements P and D which cannot be analyzed by normal modality have been done so in the framework of monotone modal logics. This would naturally lead us to expect other analyses as well. As a future work, the authors suggest the study of the modal analysis of provability predicates along this line with neighbourhood semantics which provides still larger and finer framework.