Abstract
We analyze the multimodal logic S4 n with the central agent axiom. We present a Hilbert-type calculus, then derive a Gentzen-type calculus with cut, and prove a cut-elimination theorem. The work shows that it is possible to construct a cut-free Gentzen-type calculus for this logic. Moreover, it also provides analogous results for the multimodal logic K4 n with the central agent axiom.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
J. Andrikonis and R. Pliuškevičius, Cut elimination for knowledge logic with interaction, Liet. Mat. Rink., 47(spec. nr.):346–350, 2007.
R. Fagin, J.Y. Halpern, Y. Moses, and M.Y. Vardi, Reasoning about Knowledge, The MIT Press, 2003.
R. Feys, Modal Logics, Louvain, 1965.
M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Reidel Publishing Company, Dordrecht, 1983.
M. Fitting, Basic modal logic, in D.M. Gabbay, C.J. Hogger, and J.A. Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1, Oxford University Press, New York, 1993, pp. 365–448.
L. Goble, Gentzen systems for modal logic, Notre Dame J. Formal Logic, 15(3):455–461, 1974.
R. Gore, Chapter 6: Tableau methods for modal and temporal logics, in M. D’Agostino, D. Gabbay, R. Hähnle, and J. Posegga (Eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht, 1999, pp. 297–396.
J.Y. Halpern and Y. Moses, A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence, 54(3):319–379, 1992.
G.E. Hughes and M.J. Cresswell, An Introduction to Modal Logic, Methuen and Co., London, 1972.
A. Indrzejczak, Cut-free double sequent calculus for S5, Log. J.IGPL, 6(3):505–516, 1998.
S. Kanger, Provability in Logic, Almgvist & Wiksell, Stockholm, 1957.
S.K. Kleene, Introduction to Metamathematics, D. van Nostrand Company Inc., Princeton, New Jersey, 1950.
A. Lomuscio and M. Ryan, Ideal agents sharing (some!) knowledge, in Proceedings of 13th European Conference on Artificial Intelligence ECAI-98, John Wiley & Sons, Brighton, 1998, pp. 557–561.
A. Lomuscio and M. Ryan, A spectrum of modes of knowledge sharing between agents, in M.J. Wooldridge and N.R. Jennings (Eds.), Intelligent Agents VI | Proceedings of the Sixth International Workshop on Agent Theories, Architectures, and Languages (ATAL-99), Lecture Notes in Artificial Intelligence, Springer-Verlag, Heidelberg, 1999, pp. 13–26.
A. Lomuscio, Ron van der Meyden, and M. Ryan, Knowledge in multiagent systems: Initial configurations and broadcast, ACM Trans. Comput. Log., 1(2):246–282, 2000.
G. Mints, A Short Introduction to Modal Logic, Center for the Study of Language and Information Publications, Stanford, 1992.
M. Ohnishi and K. Matsumoto, Gentzen method in modal calculi, Osaka J. Math., 9(2):113–130, 1957.
F. Poggiolesi, A cut-free simple sequent calculus for modal logic S5, Rev. Symb. Log., 1(1):3–15, 2008.
G.F. Shvarts, Gentzen style systems for K45 and K45D, in A.R. Meyer and M.A. Taitslin (Eds.), Logic at Botic ’89, Lecture Notes in Computer Science, Springer-Verlag, Pereslavl-Zalessky, 1989, pp. 245–256.
F. Stouppa, The Design of Modal Proof Theories: The Case of S5, Master’s thesis, Technische Universitat Dresden, 2004.
G. Takeuti, Proof Theory, North Holland Publishing Company, New York, 1975.
H. Wansing, Proof Theory of Modal Logic, Kluwer Academic Publishers, Dordrecht, 1996.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Andrikonis, J. Cut elimination for S4 n and K4 n with the central agent axiom. Lith Math J 49, 123–139 (2009). https://doi.org/10.1007/s10986-009-9048-6
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10986-009-9048-6