A Syntactic Realization Theorem for Justification Logics

TitleA Syntactic Realization Theorem for Justification Logics
Publication TypeConference Paper
Year of Publication2010
AuthorsBrünnler, K, Goetschi, R, Kuznets, R
EditorBeklemishev, L, Goranko, V, Shehtman, V
Conference NameAdvances in Modal Logic, Volume 8
PublisherCollege Publications
Keywordsrealization theorem
AbstractJustification 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 $\mathsf{d}$, $\mathsf{t}$, $\mathsf{b}$, $\mathsf{4}$, and $\mathsf{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 $\mathsf{KB5}$ and $\mathsf{S5}$ by showing that the positive introspection operator is superfluous.