Realization for justification logics via nested sequents: Modularity through embedding
Autor: | Remo Goetschi, Roman Kuznets |
---|---|
Rok vydání: | 2012 |
Předmět: |
Discrete mathematics
Normal modal logic Logic Modal logic 010102 general mathematics Realization theorem Multimodal logic 0102 computer and information sciences 01 natural sciences Constructive S5 Nested sequents TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Justification logic Computer Science::Logic in Computer Science Accessibility relation Calculus Sequent 0101 mathematics Realization (systems) Embedding Mathematics |
Zdroj: | Annals of Pure and Applied Logic |
Popis: | Justification logics are refinements of modal logics, where justification terms replace modalities. Modal and justification logics are connected via the so-called realization theorems. We develop a general constructive method of proving the realization of a modal logic in an appropriate justification logic by means of cut-free modal nested sequent systems. We prove a constructive realization theorem that uniformly connects every normal modal logic formed from the axioms d , t , b , 4 , and 5 with one of its justification counterparts. We then generalize the notion of embedding introduced by Fitting for justification logics, which enables us to extend our realization theorem to all natural justification counterparts. As a result, we obtain a modular realization theorem that provides several justification counterparts based on various axiomatizations of a modal logic. We also prove that these justification counterparts realize the same modal logic if and only if they belong to the same equivalence class induced by our embedding relation, thereby demonstrating that the embedding provides the right level of granularity among justification logics. |
Databáze: | OpenAIRE |
Externí odkaz: |