Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Tim S. Lyon

TL;DR

The paper resolves an open problem by proving that every analytic display calculus for primitive tense logics can be polynomially simulated by a corresponding labeled sequent calculus, and vice versa for a specific, well-behaved subspace of labeled proofs called strict labeled polytree proofs. It achieves this via new recipe-style formulations of labeled calculi as rule templates and a canonical translation of display sequents into labeled polytree sequents, along with PTIME translations in both directions. It shows that translating display proofs to strict labeled proofs preserves or reduces the number of sequents (though it may increase sequent width), while translating back may inflate the proof size by a polynomial bound, thereby identifying a tight complexity relation between the two formalisms. The results establish that the labeled framework subsumes and extends display calculi in the setting of primitive tense logics, and they provide a concrete, computational bridge between proof systems that can inform automated reasoning and formal verification in tense logics. The work also opens avenues for deeper exploration of the relationship between strict and non-strict (potentially non-polytrees) labeled proofs and their translations to 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.

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

TL;DR

The paper resolves an open problem by proving that every analytic display calculus for primitive tense logics can be polynomially simulated by a corresponding labeled sequent calculus, and vice versa for a specific, well-behaved subspace of labeled proofs called strict labeled polytree proofs. It achieves this via new recipe-style formulations of labeled calculi as rule templates and a canonical translation of display sequents into labeled polytree sequents, along with PTIME translations in both directions. It shows that translating display proofs to strict labeled proofs preserves or reduces the number of sequents (though it may increase sequent width), while translating back may inflate the proof size by a polynomial bound, thereby identifying a tight complexity relation between the two formalisms. The results establish that the labeled framework subsumes and extends display calculi in the setting of primitive tense logics, and they provide a concrete, computational bridge between proof systems that can inform automated reasoning and formal verification in tense logics. The work also opens avenues for deeper exploration of the relationship between strict and non-strict (potentially non-polytrees) labeled proofs and their translations to 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.
Paper Structure (3 sections, 1 theorem, 7 equations, 2 figures)

This paper contains 3 sections, 1 theorem, 7 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Tense Logics and Primitive Axioms
  3. Display Calculi for Tense Logics

Key Result

proposition thmcounterproposition

We define the language $\mathcal{L}_{\land,\langle\mathsf{F}\rangle,\langle\mathsf{P}\rangle}$ to be the smallest set of formulae generated by the following grammar: Let $A$, each $A_{i}$, and each $B_{i,j}$ be in $\mathcal{L}_{\land,\langle\mathsf{F}\rangle,\langle\mathsf{P}\rangle}$ with $A$ and each $A_{i}$ containing at most one occurrence of each atom. Every primitive tense axiom can be put

Figures (2)

  • Figure 1: The logical rules for the display calculus $\mathsf{DK_{t}}$Kra96.
  • Figure 2: The display rules for the display calculus $\mathsf{DK_{t}}$Kra96.

Theorems & Definitions (12)

  • definition thmcounterdefinition: The Language $\mathcal{L}$
  • definition thmcounterdefinition: Relational Frame/Model
  • definition thmcounterdefinition: Semantic Clauses
  • definition thmcounterdefinition: $\mathsf{H}\mathsf{K_{t}}$, $\mathsf{K_{t}}$
  • definition thmcounterdefinition: Primitive Tense Axiom Kra96
  • proposition thmcounterproposition: Primitive Tense Normal Form
  • definition thmcounterdefinition: Formula Translation $\tau$ Kra96
  • definition thmcounterdefinition: Substructure
  • definition thmcounterdefinition: Substitution $\sigma$
  • definition thmcounterdefinition: Quantity, Width, Size
  • ...and 2 more