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

Brian Hill (1) , Francesca Poggiolesi (2)

1 GREGH - Groupement de Recherche et d'Etudes en Gestion à HEC
2 VUB - Vrije Universiteit Brussel

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.

Keywords: Contraction-free; Cut-free; Propositional Dynamic Logic; Tree-hypersequent; Proof theory

Domains: Economy and decision science

Brian Hill, Francesca Poggiolesi. A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic. Studia Logica, 2010, 94 (1), pp.47-72. ⟨10.1007/s11225-010-9224-z⟩. ⟨hal-00521802⟩