Abstract
The logic S4LP combines the modal logic S4 with the justification logic LP, both axiomatically and semantically. We introduce a simple restriction on the behavior of constants in S4LP, having no effect on the LP sublogic. Under this restriction some powerful derived rules are established. Then these are used to show completeness relative to a semantics having what we call the local realizability property: at each world and for each formula true at that world there is a realization also true at that world, where a realization is the result of replacing all modal operators with explicit justification terms. This is a part of a project to understand the deeper aspects of Artemov’s Realization Theorem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Hintikka, J.: Knowledge and Belief. Cornell University Press (1962)
Artemov, S.: Explicit provability and constructive semantics. The Bulletin for Symbolic Logic 7(1), 1–36 (2001)
Artemov, S., Nogina, E.: Logic of knowledge with justifications from the provability perspective. Technical report, Technical Report TR-2004011, CUNY Ph. D. Program in Computer Science, 2004 (2004)
Artemov, S., Nogina, E.: Introducing Justification into Epistemic Logic. Journal of Logic and Computation 15(6), 1059–1073 (2005)
Fitting, M.C.: A semantics for the logic of proofs. Technical Report TR-2003012, CUNY Ph.D. Program in Computer Science (2003), http://www.cs.gc.cuny.edu/tr/
Fitting, M.C.: The logic of proofs, semantically. Annals of Pure and Applied Logic 132, 1–25 (2005)
Mkrtychev, A.: Models for the logic of proofs. In: Adian, S., Nerode, A. (eds.) LFCS 1997. LNCS, vol. 1234, pp. 266–275. Springer, Heidelberg (1997)
Fitting, M.C.: Semantics and tableaus for LPS4. Technical Report TR-2004016, CUNY Ph.D. Program in Computer Science (2004), http://www.cs.gc.cuny.edu/tr/
Artemov, S.: Evidence-based common knowledge. Technical report, Technical Report TR-2004018, CUNY Ph. D. Program in Computer Science, 2004 (2004)
Artemov, S.: Justified common knowledge. Theoretical Computer Science 357(1-3), 4–22 (2006)
Fitting, M.C.: Reasoning with justifications. Studia Logica (Forthcoming, 2008)
Rubtsova, N.: Evidence-based knowledge for S5. The Bulletin of Symbolic Logic 12(2), 344 (2006)
Rubtsova, N.: Semantics for Logic of explicit knowledge corresponding to S5. In: Proceedings of the Workshop on Rationality and Knowledge, ESSLLI, Malaga, pp. 124–131 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fitting, M. (2008). S4LP and Local Realizability. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds) Computer Science – Theory and Applications. CSR 2008. Lecture Notes in Computer Science, vol 5010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79709-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-79709-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79708-1
Online ISBN: 978-3-540-79709-8
eBook Packages: Computer ScienceComputer Science (R0)