Cyclic Proofs for Linear Temporal Logic
Ioannis Kokkinis, Thomas Studer · 2016
Annotated sequents provide an elegant approach for the design of deductive systems for temporal logics.Their proof theory, however, is notoriously difficult.It is not even clear how to syntactically show the admissibility of weakening.In this paper, we establish weakening by purely proof-theoretic methods, thus solving an open problem by Brünnler and Lange.We also investigate the role of cut in annotated sequent systems.In this paper we provide a solution to this open problem and establish the admissibility of weakening by proof-theoretic means.Moreover, we present a series of examples that explain the design of Brünnler and Lange's system.Their system is based on annotations that are sets of sets of formulas and it uses several rules to unfold greatest fixed points.Our examples show that these features are necessary in order to have completeness, that means their system is as simple as a cut-free system can be.However, we also show that if we add a cut-rule, then the system can be made much simpler.That is, we can have fewer rules and annotations of a simpler form.This provides a very nice and instructive example on the role of cut in proofs of induction statements.