David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 89 (3):343 - 363 (2008)
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.
|Keywords||Philosophy Computational Linguistics Mathematical Logic and Foundations Logic|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Kai Brünnler & Thomas Studer (2009). Syntactic Cut-Elimination for Common Knowledge. Annals of Pure and Applied Logic 160 (1):82-95.
Dexter Kozen (1988). A Finite Model Theorem for the Propositional Μ-Calculus. Studia Logica 47 (3):233 - 241.
Citations of this work BETA
No citations found.
Similar books and articles
Luca Alberucci & Vincenzo Salipante (2004). On Modal Μ-Calculus and Non-Well-Founded Set Theory. Journal of Philosophical Logic 33 (4):343-360.
Gerard Renardel de Lavalette, Barteld Kooi & Rineke Verbrugge (2008). Strong Completeness and Limited Canonicity for PDL. Journal of Logic, Language and Information 17 (1):291-292.
Maria Luisa Bonet & Samuel R. Buss (1993). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (2):688-709.
Paolo Gentilini (1993). Syntactical Results on the Arithmetical Completeness of Modal Logic. Studia Logica 52 (4):549 - 564.
Kooi, Barteld, Renardel de Lavalette, Gerard & Verbrugge, Rineke, Hybrid Logics with Infinitary Proof Systems.
Jan Krajíček (2004). Implicit Proofs. Journal of Symbolic Logic 69 (2):387 - 397.
Rineke Verbrugge, Gerard Renardel de Lavalette & Barteld Kooi, Hybrid Logics with Infinitary Proof Systems.
Paolo Gentilini (1999). Proof-Theoretic Modal Pa-Completeness I: A System-Sequent Metric. Studia Logica 63 (1):27-48.
G. Sambin & S. Valentini (1980). A Modal Sequent Calculus for a Fragment of Arithmetic. Studia Logica 39 (2-3):245-256.
Sara Negri (2011). Proof Analysis: A Contribution to Hilbert's Last Problem. Cambridge University Press.
Added to index2009-01-28
Total downloads37 ( #127,800 of 1,940,864 )
Recent downloads (6 months)3 ( #272,622 of 1,940,864 )
How can I increase my downloads?