On the Proof Theory of the Modal mu-Calculus

Studia Logica 89 (3):343-363 (2008)
  Copy   BIBTEX

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Power and weakness of the modal display calculus.Marcus Kracht - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers. pp. 93--121.
Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
The modal object calculus and its interpretation.Edward N. Zalta - 1997 - In M. de Rijke (ed.), Advances in Intensional Logic. Kluwer Academic Publishers. pp. 249--279.
Proof theory of modal logic.Heinrich Wansing (ed.) - 1996 - Boston: Kluwer Academic Publishers.
On modal μ-calculus and non-well-founded set theory.Luca Alberucci & Vincenzo Salipante - 2004 - Journal of Philosophical Logic 33 (4):343-360.
A contraction-free sequent calculus for S4.Jörg Hudelmaier - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers. pp. 3--15.
Fitch-style natural deduction for modal paralogics.Hans Lycke - 2009 - Logique Et Analyse 52 (207):193-218.

Analytics

Added to PP
2009-01-28

Downloads
80 (#190,806)

6 months
5 (#246,492)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Syntactic cut-elimination for common knowledge.Kai Brünnler & Thomas Studer - 2009 - Annals of Pure and Applied Logic 160 (1):82-95.
Cut-free common knowledge.Gerhard Jäger, Mathis Kretz & Thomas Studer - 2007 - Journal of Applied Logic 5 (4):681-689.

Add more references