Algebraic Proof Theory for Infinitary Action Logic

TL;DR

This paper introduces a uniform algebraic proof system for a broad class of action algebras, including both wellfounded and non-wellfounded cases, using a novel combination of proof theory techniques.

Contribution

It provides a new, general method for constructing cut-free sequent systems for *-continuous action algebras based on analytic quasiequations.

Findings

Established soundness and completeness for the proof systems.

Unified approach applicable to various classes of action algebras.

Extended non-wellfounded proof theory to algebraic structures.

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.