Extending Action Logic with Omega Iteration
Tikhon Pshenitsyn
TL;DR
Extends action logic with omega iteration by interpreting $A^\omega$ as infinitary multiplicative conjunction within a two-sort Lambek-style calculus. Introduces $\mathrm{MALC}^\ast_\omega$, proves cut admissibility via a generalized mix rule and an infinitary left rule, and analyzes the structure of infinite derivations. Establishes completeness for omega-regular expressions, showing $\alpha \subseteq \beta$ iff $\alpha \vdash \beta$, while identifying a boundary when residuals $\backslash$ and $/$ are included. Determines provability complexity as $\Pi^2_1$ with $\Pi^1_2$-hardness, via a reduction from Pi^1_2-complete problems using context-free grammars, thus situating MALC^*_\omega within high analytical complexity.
Abstract
We present a proof system that extends action logic by omega iteration, which is viewed as infinitary multiplicative conjunction. We prove cut admissibility and establish complexity bounds for the provability predicate.