Modal logics, justification logics, and realization (Q286591)

Justification logics are modal-like logics where justification terms replace modalities. The correspondence between modal and justification logics is established by the so-called ``realization theorem'', which specifies how occurrences of modalities in a modal formula are replaced by justification terms so that modal theorems are transformed into justification logic theorems. The first realization theorem was proved by \textit{S. N. Artemov} [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059)] and connects the modal logic S4 with its justification counterpart the logic of proofs. Later Artemov's realization theorem [loc. cit.] has been extended to all logics in the modal cube, i.e. modal logics between K and S5 (see, e.g. [\textit{R. Goetschi and R. Kuznets}, Ann. Pure Appl. Logic 163, No. 9, 1271--1298 (2012; Zbl 1276.03020)]), and it is shown that there are 24 justification logics that correspond to a logic from the modal cube. The method used by Artemov [loc. cit.], and also by Goetschi and Kuznets [loc. cit.], is a constructive syntactic method which makes use of cut-free sequent calculi for modal logics.NEWLINENEWLINEIn the paper under review, the author extends the picture and proves a realization theorem for the infinite family of Geach modal logics. This extends the formerly known realization results of logics from the modal cube. After presenting a concise background on justification logics through their axiomatic presentations and their possible world semantics (also known as Fitting models), the paper introduces justification counterparts of all Geach logics. The author presents axiom systems and semantics for all justification counterparts of Geach logics, and establishes soundness, completeness, and realization. Completeness of these logics is shown by the method of canonical models. The main focus of the paper is the presentation of a general method of establishing realization theorems. The author gives a non-constructive semantic method for proving the realization theorem, a proof which is originated in [the author, Ann. Pure Appl. Logic 132, No. 1, 1--25 (2005; Zbl 1066.03059)] with a modification and correction supplied in [the author, J. Appl. Log. 8, No. 4, 356--370 (2010; Zbl 1215.03032)]. As the author points out: ``The present paper is the first full presentation of the ideas that have been developed''. In order to prove the realization theorem, a two-stage process is given: At the first stage, a quasi-realization of a given modal formula is produced non-constructively. At the second stage, an algorithm is given that converts quasi-realizations to realizations. The central result of the paper is a realization theorem that connects a normal modal logic that is characterized by a class of frames \(\mathcal{F}\) to a justification logic whose canonical Fitting model is based on a frame in \(\mathcal{F}\). Finally, it is shown that the range of applications of the aforementioned realization theorem is not restricted to Geach logics.