Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics

TL;DR

This paper establishes polynomial-time translations between display and labeled sequent calculi for tense logics, demonstrating their polynomial simulation and extending the formalism for primitive tense logics.

Contribution

It introduces a new formulation of labeled sequent calculi with rule templates and primitive tense rules, bridging the gap with display calculi for tense logics.

Findings

Polynomial translations between display and labeled proofs.

Display proofs are shorter when translated to labeled proofs.

Labeled proofs can become larger when translated into display proofs.

Abstract

We define and study translations between the maximal class of analytic display calculi for tense logics and labeled sequent calculi, thus solving an open problem about the translatability of proofs between the two formalisms. In particular, we provide PTIME translations that map cut-free display proofs to and from special cut-free labeled proofs, which we dub 'strict' labeled proofs. This identifies the space of cut-free display proofs with a polynomially equivalent subspace of labeled proofs, showing how calculi within the two formalisms polynomially simulate one another. We analyze the relative sizes of proofs under this translation, finding that display proofs become polynomially shorter when translated to strict labeled proofs, though with a potential increase in the length of sequents; in the reverse translation, strict labeled proofs may become polynomially larger when translated into display proofs. In order to achieve our results, we formulate labeled sequent calculi in a new way that views rules as 'templates', which are instantiated with substitutions to obtain rule applications; we also provide the first definition of primitive tense structural rules within the labeled sequent formalism. Therefore, our formulation of labeled calculi more closely resembles how display calculi are defined for tense logics, which permits a more fine-grained analysis of rules, substitutions, and translations. This work establishes that every analytic display calculus for a tense logic can be viewed as a labeled sequent calculus, showing conclusively that the labeled formalism subsumes and extends the display formalism in the setting of primitive tense logics.