Skip to main content
SpringerLink
Log in

A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alberucci Luca, Gerhard Jäger: ‘About cut elimination for logics of common knowledge’. Annals of Pure and Applied Logic 133, 1–3 (2005) 73–99

    Article  Google Scholar 

  2. Blackburn Patrick, Maarten de Rijke, Yde Venema: Modal Logic. Cambridge University Press, Cambridge (2001)

    Google Scholar 

  3. Engeler Erwin: ‘Algorithmic properties of structures’. Mathematical Systems Theory 1, 183–195 (1967)

    Article  Google Scholar 

  4. Harel David, Dexter Kozen, Jerzy Tiuryn: Dynamic Logic. MIT Press, Cambridge (2000)

    Google Scholar 

  5. Hoare Charles, Anthony Richard: ‘An axiomatic basis for computer programming’. Communications of the ACM 12, 576–580 (1969)

    Article  Google Scholar 

  6. Jäger Gerhard, Mathis Kretz, Thomas Studer: ‘Cut-free common knowledge’. Journal of Applied Logic 5(4), 681–689 (2007)

    Article  Google Scholar 

  7. Knijnenburg Peter M.W., Jan van Leeuwen: ‘On models for propositional dynamic logic’. Theoretical Computer Science 91, 181–203 (1991)

    Article  Google Scholar 

  8. Nishimura Hirokazu, ‘Sequential method in propositional dynamic logic’. Acta Informatica 12, 377–400 (1979)

    Article  Google Scholar 

  9. Poggiolesi, Francesca, Sequent Calculi for Modal Logic, Ph.D Thesis, Florence, 2008.

  10. Poggiolesi, Francesca, ‘The method of tree-hypersequent for modal propositional logic’, in D. Makinson, J. Malinowski, and H. Wansing, (eds.), Trends in logic: Towards mathematical philosophy, Springer, 2009, pp. 31–51.

  11. Poggiolesi, Francesca, Reflecting the semantic features of S5 at the syntactic level, SILFS conference proceedings, Forthcoming, 2010.

  12. Troelstra Anne Sjerp, Helmut Schwichtenberg: Basic Proof Theory. Cambridge University Press, Cambridge (1996)

    Google Scholar 

  13. Wansing Heinrich: Displaying Modal Logic. Kluwer Academic Publisher, Dordrecht/Boston/London (1998)

    Google Scholar 

  14. Yanov Joseph: ‘On equivalence of operator schemes’. Problems of Cybernetic 1, 1–100 (1959)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Center of Logic and Philosophy of Science (CLFW), Vrije Universiteit Brussel, Pleinaan 2, 1050, Brussels, Belgium

    Francesca Poggiolesi

  2. HEC Paris and IHPST (CNRS / Paris 1 / ENS), 1 rue de la Libération, 78351, Jouy-en-Josas, France

    Brian Hill

Authors
  1. Brian Hill
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesca Poggiolesi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesca Poggiolesi.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hill, B., Poggiolesi, F. A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic. Stud Logica 94, 47–72 (2010). https://doi.org/10.1007/s11225-010-9224-z

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11225-010-9224-z

Keywords

Search

Navigation