Realization using the model existence theorem

Justification logics refine modal logics by replacing the usual necessity operator with a family of justification terms that embody reasons for the necessity of a formula, rather than simply recording the fact of necessity. Many common modal logics have justification counterparts. The connection between a modal logic and its justification counterpart is through a Realization Theorem, which says that modal operators can be replaced in a precise way with justification terms so that modal theorems turn into justification logic theorems. In this paper we present a new proof of Realization. We use the familiar machinery of consistency properties to prove a weak version, we call it Quasi-Realization. Then we show how to convert Quasi-Realizations into Realizations proper. Unlike most other treatments in the literature, the work here is not propositional, but firstorder. Only one modal/justification logic is discussed, but the methods easily extend to other standard systems.

• Type: Journal
• Year: 2016
• Where: LOGCOM
• Authors: Melvin Fitting
• Keywords: LOGCOM 2016, Programming Languages