×

Realization theorems for justification logics: full modularity. (English) Zbl 1471.03084

De Nivelle, Hans (ed.), Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9323, 221-236 (2015).
Summary: Justification logics were introduced by Artemov in 1995 to provide intuitionistic logic with a classical provability semantics, a problem originally posed by Gödel. Justification logics are refinements of modal logics and formally connected to them by so-called realization theorems. A constructive proof of a realization theorem typically relies on a cut-free sequent-style proof system for the corresponding modal logic. A uniform realization theorem for all the modal logics of the so-called modal cube, i.e., for the extensions of the basic modal logic K with any subset of the axioms d, t, b, 4, and 5, has been proven using nested sequents. However, the proof was not modular in that some realization theorems required postprocessing in the form of translation on the justification logic side. This translation relied on additional restrictions on the language of the justification logic in question, thus, narrowing the scope of realization theorems. We present a fully modular proof of the realization theorems for the modal cube that is based on modular nested sequents introduced by Marin and Straßburger.
For the entire collection see [Zbl 1325.68016].

MSC:

03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03B45 Modal logic (including the logic of norms)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arisaka, R., Das, A., Straßburger, L.: On nested sequents for constructive modal logics. E-print 1505.06896, arXiv, May 2015 · Zbl 1347.03038
[2] Artemov, S.N.: Explicit provability and constructive semantics. Bulletin of Symbolic Logic 7(1), 1–36 (2001) · Zbl 0980.03059 · doi:10.2307/2687821
[3] Artemov, S.N., Fitting, M.: Justification logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Fall 2012 edn. (2012), http://plato.stanford.edu/archives/fall2012/entries/logic-justification/
[4] Artemov, S.N., Kazakov, E.L., Shapiro, D.: Logic of knowledge with justifications. Tech. Rep. CFIS 99–12, Cornell University (1999)
[5] Brezhnev, V.N.: On explicit counterparts of modal logics. Tech. Rep. CFIS 2000–05, Cornell University (2000)
[6] Brezhnev, V.N., Kuznets, R.: Making knowledge explicit: How hard it is. Theoretical Computer Science 357(1–3), 23–34 (2006) · Zbl 1094.03006 · doi:10.1016/j.tcs.2006.03.010
[7] Brünnler, K.: Deep sequent systems for modal logic. Archive for Mathematical Logic 48(6), 551–577 (2009) · Zbl 1180.03023 · doi:10.1007/s00153-009-0137-3
[8] Bucheli, S., Kuznets, R., Studer, T.: Realizing public announcements by justifications. Journal of Computer and System Sciences 80(6), 1046–1066 (2014) · Zbl 1327.03011 · doi:10.1016/j.jcss.2014.04.001
[9] Fitting, M.: The logic of proofs, semantically. Annals of Pure and Applied Logic 132(1), 1–25 (2005) · Zbl 1066.03059 · doi:10.1016/j.apal.2004.04.009
[10] Fitting, M.: Realizations and LP. Annals of Pure and Applied Logic 161(3), 368–387 (2009) · Zbl 1221.03020 · doi:10.1016/j.apal.2009.07.010
[11] Fitting, M.: Realization using the model existence theorem. Journal of Logic and Computation Advance Access, July 2013, http://dx.doi.org/10.1093/logcom/ext025 · Zbl 1403.03030 · doi:10.1093/logcom/ext025
[12] Fitting, M.: Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic 55(1), 41–61 (2014) · Zbl 1327.03006 · doi:10.1215/00294527-2377869
[13] Fitting, M., Kuznets, R.: Modal interpolation via nested sequents. Annals of Pure and Applied Logic 166(3), 274–305 (2015) · Zbl 1369.03103 · doi:10.1016/j.apal.2014.11.002
[14] Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic, Synthese Library, vol. 277. Kluwer Academic Publishers (1998) · Zbl 1025.03001 · doi:10.1007/978-94-011-5292-1
[15] Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Summer 2014 edn. (2014), http://plato.stanford.edu/archives/sum2014/entries/logic-modal/
[16] Goetschi, R., Kuznets, R.: Realization for justification logics via nested sequents: Modularity through embedding. Annals of Pure and Applied Logic 163(9), 1271–1298 (2012) · Zbl 1276.03020 · doi:10.1016/j.apal.2012.02.002
[17] Hakli, R., Negri, S.: Does the deduction theorem fail for modal logic? Synthese 187(3), 849–867 (2012) · Zbl 1275.03091 · doi:10.1007/s11229-011-9905-9
[18] Kuznets, R.: Self-referential justifications in epistemic logic. Theory of Computing Systems 46(4), 636–661 (2010) · Zbl 1216.03037 · doi:10.1007/s00224-009-9209-3
[19] Marin, S., Straßburger, L.: Label-free modular systems for classical and intuitionistic modal logics. In: Advances in Modal Logic, vol. 10, pp. 387–406. College Publications (2014) · Zbl 1385.03023
[20] Mints, G.E.: Lewis’ systems and system T (1965–1973). In: Selected Papers in Proof Theory, Studies in Proof Theory, vol. 3, pp. 221–294. Bibliopolis and North-Holland (1992)
[21] Rubtsova, N.M.: On realization of S5-modality by evidence terms. Journal of Logic and Computation 16(5), 671–684 (2006) · Zbl 1118.03011 · doi:10.1093/logcom/exl030
[22] Yu, J.: Self-referentiality of Brouwer–Heyting–Kolmogorov semantics. Annals of Pure and Applied Logic 165(1), 371–388 (2014) · Zbl 1348.03012 · doi:10.1016/j.apal.2013.07.019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.