Abstract
We study the proof-theoretic relationship between two deductive systems for the modal mu-calculus. First we recall an infinitary system which contains an omega rule allowing to derive the truth of a greatest fixed point from the truth of each of its (infinitely many) approximations. Then we recall a second infinitary calculus which is based on non-well-founded trees. In this system proofs are finitely branching but may contain infinite branches as long as some greatest fixed point is unfolded infinitely often along every branch. The main contribution of our paper is a translation from proofs in the first system to proofs in the second system. Completeness of the second system then follows from completeness of the first, and a new proof of the finite model property also follows as a corollary.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Aldwinckle, John, and Robin Cockett, ‘The proof theory of modal μ logics’, in Proc. Fixed Points in Computer Science, 2001.
Bradfield, Julian, and Colin Stirling, ‘Modal mu-calculi’, in Patrick Blackburn, Johan van Benthem, and Frank Wolter, (eds.), Handbook of Modal Logic, Elsevier, 2007, pp. 721–756.
Brotherston, James, Sequent Calculus Proof Systems for Inductive Definitions, Ph.D. thesis, University of Edinburgh, 2006.
Brotherston, James, and Alex Simpson, ‘Complete sequent calculi for induction and infinite descent’, in Proceedings of LICS-22, 2007, pp. 51–60.
Brünnler, Kai, and Martin Lange, ‘Cut-free sequent systems for temporal logics’, Journal of Logic and Algebraic Programming, (to appear).
Brünnler, Kai, and Thomas Studer, ‘Syntactic cut-elimination for common knowledge’, in Methods for Modalities 5, 2007.
Dax, Christian, Martin Hofmann, and Martin Lange, ‘A proof system for the linear time μ-calculus’, in Proc. 26th Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’06, vol. 4337 of LNCS, Springer, 2006, pp. 274–285.
Emerson, E. Allen, and Charanjit S. Jutla, ‘The complexity of tree automata and logics of programs’, in 29th Annual Symposium on Foundations of Computer Science FOCS, IEEE, 1988, pp. 328–337.
Fischer Michael J., Richard E. Ladner (1979) ‘Propositional dynamic logic of regular programs’. Journal of Computing and System Science 18(2): 194–211
Gaintzarain, Joxe, Montserrat Hermo, Paqui Lucio, Marisa Navarro, and Fernando Orejas, ‘A cut-free and invariant-free sequent calculus for PLTL’, in Jacques Duparc, and Thomas A. Henzinger, (eds.), Computer Science Logic CSL 2007, Springer, 2007, pp. 481–495.
Jäger Gerhard, Mathis Kretz, Thomas Studer (2007) ‘Cut-free common knowledge’. Journal of Applied Logic 5: 681–689
Jäger, Gerhard, Mathis Kretz, and Thomas Studer, ‘Canonical completeness of infinitary mu’, Journal of Logic and Algebraic Programming, (to appear).
Kozen Dexter (1983) ‘Results on the propositional modal μ–calculus’. Theoretical Computer Science 27: 333–354
Kozen Dexter (1988) ‘A finite model theorem for the propositional μ–calculus’. Studia Logica 47(3): 233–241
Leivant, Daniel, ‘A proof theoretic methodology for propositional dynamic logic’, in Proceedings of the International Colloquium on Formalization of Programming Concepts, Springer LNCS, 1981, pp. 356–373.
Niwinski Damian, Igor Walukiewicz (1996) ‘Games for the mu-calculus’. Theoretical Computer Science 163(1&2): 99–116
Santocanale, Luigi, ‘A calculus of circular proofs and its categorical semantics’, in FoSSaCS ’02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, Springer, 2002, pp. 357–371.
Sprenger, Christoph, and Mads Dam, ‘On the structure of inductive reasoning: Circular and tree-shaped proofs in the mu-calculus’, in Proc. FOSSACS’03, Springer LNCS, 2003, pp. 425–440.
Walukiewicz, Igor, ‘A complete deductive system for the μ–calculus’, in Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Science Press, 1993, pp. 136–147.
Walukiewicz Igor (2000) ‘Completeness of Kozen’s axiomatization of the propositional μ–calculus’. Information and Computation 157: 142–182
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Studer, T. On the Proof Theory of the Modal mu-Calculus. Stud Logica 89, 343–363 (2008). https://doi.org/10.1007/s11225-008-9133-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-008-9133-6