Extending Action Logic with Omega Iteration

TL;DR

This paper introduces an extension to action logic incorporating omega iteration, providing a proof system with proven cut admissibility and complexity bounds for the provability predicate.

Contribution

It extends action logic with omega iteration as an infinitary conjunction, and establishes foundational proof-theoretic properties.

Findings

Proves cut admissibility for the extended logic

Establishes complexity bounds for provability

Defines omega iteration as an infinitary conjunction

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.