Abstract
We first show that a labelled sequent calculus \(\mathbf {G3PAL}\) for Public Announcement Logic (PAL) by Maffezioli and Negri (2011) has been lacking rules for deriving an axiom of Hilbert-style axiomatization of PAL. Then, we provide our revised calculus \(\mathbf {GPAL}\) to show that all the formulas provable in Hilbert-style axiomatization of PAL are also provable in \(\mathbf {GPAL}\) together with the cut rule. We also establish that our calculus enjoys cut elimination theorem. Moreover, we show the soundness of our calculus for Kripke semantics with the notion of surviveness of possible worlds in a restricted domain. Finally, we provide a direct proof of the semantic completeness of \(\mathbf {GPAL}\) for the link-cutting semantics of PAL.
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
Notes
- 1.
They stated that there are some valid formulas such as \([A\wedge A]B\leftrightarrow [A]B\) which may be unprovable in \(\mathbf {G3PAL}\).
- 2.
G3-style sequent calculus for modal logic \(\mathbf {K}\) named \(\mathbf {G3K}\) has been introduced in Negri [8]. And G3-style sequent calculus is a calculus that does not have any structural rules and the most outstanding feature of this calculus is that the contraction rules are admissible. The specific introduction of G3-style sequent calculus (or G3-system) itself can be found in Negri and Plato [9] and Troelstra and Schwichtenberg [13].
- 3.
The notion of surviveness will be referred in Sect. 7.5 more specifically.
- 4.
Of course, there might still exist a possibility to keep G3-style with the additional rules for relational atoms.
- 5.
The following rules are also derivable in \(\mathbf {GPAL}^{+}\).
.
- 6.
We note that t-validity is close to the validity in the tableaux method of PALÂ [2].
- 7.
Thanks to a comment from Makoto Kanazawa in the annual meeting of MLG2014, we noticed that link-cutting semantics may be suitable for our labelled sequent calculus of PAL.
References
Balbiani, P., Demange, V., Galmiche, D.: A sequent calculus with labels for PAL. Presented in Advances in Modal Logic, 2014
Balbiani, P., van Ditmarsch, H., Herzig, A., de Lima, T.: Taleaux for public announcement logic. J. Logic Comput. 20, 55–76 (2010)
Baltag, A., Moss, L., Solecki, S.: The logic of public announcements, common knowledge and private suspicions. In: Proceedings of TARK, pp. 43–56. Morgan Kaufmann Publishers, Los Altos (1989)
Gentzen, G.: Untersuchungen Über das logische Schließen. I. Mathematische Zeitschrift 39, (1934)
Hansen, J.U.: A logic toolbox for modeling knowledge and information in multi-agent systems and social epistemology. PhD thesis, Roskilde University (2011)
Kashima, R.: Mathematical Logic. Asakura Publishing Co., Ltd (2009). (in Japanese)
Maffezioli, P., Negri, S.: A Gentzen-style analysis of public announcement logic. In: Proceedings of the International Workshop on Logic and Philosophy of Knowledge, Communication and Action, pp. 293–313 (2010)
Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34, 507–544 (2005)
Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press (2001)
Negri, S., von Plato, J.: Proof Analysis. Cambridge University Press (2011)
Ono, H., Komori, Y.: Logics without contraction rule. J. Symbolic Logic 50(1), 169–201 (1985)
Plaza, J.: Logic of public communications. In: Proceedings of the 4th International Symposium on Methodologies for Intellingent Systems: Poster Session Program, pp. 201–216 (1989)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, 2 edn (2000)
van Benthem, J., Liu, F.: Dynamic logic of preference upgrade. J. Appl. Non-Classical Logics 17, 157–182 (2007)
van Ditmarsch, H., Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Springer Verlag Gmbh (2008)
Acknowledgments
We would like to thank an anonymous reviewer for his/her constructive comments to our manuscript. We also would like to thank the audiences in the Second Taiwan Philosophical Logic Colloquium (TPLC 2014) in Taiwan and the 49th MLG meeting at Kaga, Japan, particularly Makoto Kanazawa for a helpful comment on the link-cutting semantics at the MLG meeting. The second author would like to thank Didier Galmiche for a discussion on the topic of this paper. Finally, we are grateful to Sean Arn for his proofreading of the final version of the paper. This work of the first author was supported by Grant-in-Aid for JSPS Fellows, and that of the second author was supported by JSPS KAKENHI, Grant-in-Aid for Young Scientists (B) 24700146 and 15K21025. This work was conducted also by JSPS Core-to-Core Program (A. Advanced Research Networks).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Nomura, S., Sano, K., Tojo, S. (2016). Revising a Labelled Sequent Calculus for Public Announcement Logic. In: Yang, SM., Deng, DM., Lin, H. (eds) Structural Analysis of Non-Classical Logics. Logic in Asia: Studia Logica Library. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48357-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-48357-2_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48356-5
Online ISBN: 978-3-662-48357-2
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)