A syntactic realization theorem for justification logics
Kai Brünnler, Remo Goetschi, Roman Kuznets · BORIS (University Library Bern) · 2010
Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms d, t, b, 4, and 5 with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting’s realization merging technique. We further strengthen the realization theorem for KB5 and S5 by showing that the positive introspection operator is superfluous. Keywords: justification logic, modal logic, realization theorem, nested sequents, positive introspection