Lithuanian Mathematical Journal

, Volume 49, Issue 2, pp 123–139 | Cite as

Cut elimination for S4 n and K4 n with the central agent axiom



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.


S4n K4n modal logic interaction axiom cut elimination central agent 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Andrikonis and R. Pliuškevičius, Cut elimination for knowledge logic with interaction, Liet. Mat. Rink., 47(spec. nr.):346–350, 2007.Google Scholar
  2. 2.
    R. Fagin, J.Y. Halpern, Y. Moses, and M.Y. Vardi, Reasoning about Knowledge, The MIT Press, 2003.Google Scholar
  3. 3.
    R. Feys, Modal Logics, Louvain, 1965.Google Scholar
  4. 4.
    M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Reidel Publishing Company, Dordrecht, 1983.MATHGoogle Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    L. Goble, Gentzen systems for modal logic, Notre Dame J. Formal Logic, 15(3):455–461, 1974.MATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.MATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    G.E. Hughes and M.J. Cresswell, An Introduction to Modal Logic, Methuen and Co., London, 1972.Google Scholar
  10. 10.
    A. Indrzejczak, Cut-free double sequent calculus for S5, Log. J.IGPL, 6(3):505–516, 1998.MATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    S. Kanger, Provability in Logic, Almgvist & Wiksell, Stockholm, 1957.Google Scholar
  12. 12.
    S.K. Kleene, Introduction to Metamathematics, D. van Nostrand Company Inc., Princeton, New Jersey, 1950.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    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.CrossRefGoogle Scholar
  16. 16.
    G. Mints, A Short Introduction to Modal Logic, Center for the Study of Language and Information Publications, Stanford, 1992.MATHGoogle Scholar
  17. 17.
    M. Ohnishi and K. Matsumoto, Gentzen method in modal calculi, Osaka J. Math., 9(2):113–130, 1957.MATHMathSciNetGoogle Scholar
  18. 18.
    F. Poggiolesi, A cut-free simple sequent calculus for modal logic S5, Rev. Symb. Log., 1(1):3–15, 2008.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    F. Stouppa, The Design of Modal Proof Theories: The Case of S5, Master’s thesis, Technische Universitat Dresden, 2004.Google Scholar
  21. 21.
    G. Takeuti, Proof Theory, North Holland Publishing Company, New York, 1975.Google Scholar
  22. 22.
    H. Wansing, Proof Theory of Modal Logic, Kluwer Academic Publishers, Dordrecht, 1996.MATHGoogle Scholar

Copyright information

© Springer Science+Business Media, Inc. 2009

Authors and Affiliations

  1. 1.Institute of Mathematics and InformaticsVilniusLithuania

Personalised recommendations