Finitary proof systems for Kozen’s μ.

Loading...
Thumbnail Image
Date
2016
Volume
2016-26
Issue
Journal
Series Titel
Oberwolfach Preprints (OWP)
Book Title
Publisher
Oberwolfach : Mathematisches Forschungsinstitut Oberwolfach
Link to publishers version
Abstract

We present three finitary cut-free sequent calculi for the modal [my]-calculus. Two of these derive annotated sequents in the style of Stirling’s ‘tableau proof system with names’ (4236) and feature special inferences that discharge open assumptions. The third system is a variant of Kozen’s axiomatisation in which cut is replaced by a strengthening of the v-induction inference rule. Soundness and completeness for the three systems is proved by establishing a sequence of embeddings between the calculi, starting at Stirling’s tableau-proofs and ending at the original axiomatisation of the [my]-calculus due to Kozen. As a corollary we obtain a completeness proof for Kozen’s axiomatisation which avoids the usual detour through automata or games.

Description
Keywords
License
This document may be downloaded, read, stored and printed for your own use within the limits of § 53 UrhG but it may not be distributed via the internet or passed on to external parties.
Dieses Dokument darf im Rahmen von § 53 UrhG zum eigenen Gebrauch kostenfrei heruntergeladen, gelesen, gespeichert und ausgedruckt, aber nicht im Internet bereitgestellt oder an Außenstehende weitergegeben werden.