Algebraic Proof Theory for Infinitary Action Logic

TL;DR

The paper tackles the problem of obtaining cut-free, sound and complete sequent systems for classes of $*$-continuous action lattices defined by analytic quasiequations. It develops two mutually interpretable proof systems—wellfounded $\mathrm{G}^\omega\mathsf{ACT}^*$ and non-wellfounded $\mathrm{G}^\infty\mathsf{ACT}^*$—and uses corecursive translations to establish equivalence and to prove cut-free completeness via residuated-frame semantics and algebraic proof theory. Central contributions include the main equivalence theorem, an algebraic completeness theorem, and the demonstration that analytic quasiequations are preserved under MacNeille completions. The approach integrates non-wellfounded proof theory with residuated-frame methods, enabling modular analytic proof theory for action lattices and paving the way for interpolation tools and extensions beyond Kleene algebras.

Abstract

We exhibit a uniform method for obtaining (wellfounded and non-wellfounded) cut-free sequent-style proof systems that are sound and complete for various classes of action algebras, i.e., Kleene algebras enriched with meets and residuals. Our method applies to any class of *-continuous action algebras that is defined, relative to the class of all *-continuous action algebras, by analytic quasiequations. The latter make up an expansive class of conditions encompassing the algebraic analogues of most well-known structural rules. These results are achieved by wedding existing work on non-wellfounded proof theory for action algebras with tools from algebraic proof theory.

Figures (4)

• Figure 1: Principal rules
• Figure 2: Structural rules
• Figure 3: Gentzen rules
• Figure 4: $*$-Gentzen rules

Theorems & Definitions (49)

• Definition 3.1
• Definition 3.2
• Definition 3.3
• Definition 3.4
• Definition 3.5
• Lemma 3.6
• proof
• Definition 3.7
• Definition 3.8
• Lemma 3.9