Kleene Algebras, Regular Languages and Substructural Logics

TL;DR

This paper introduces two substructural propositional logics, KL and KL+, and proves their strong completeness with respect to Kleene algebra interpretations, along with decidability and cut rule admissibility.

Contribution

It presents the first complete axiomatizations of KL and KL+ with respect to Kleene algebra models and language models, establishing their logical properties.

Findings

Strong completeness of KL and KL+ with respect to Kleene algebra models

Decidability of the consequence relations in both logics

Admissibility of the cut rule in KL and KL+

Abstract

We introduce the two substructural propositional logics KL, KL+, which use disjunction, fusion and a unary, (quasi-)exponential connective. For both we prove strong completeness with respect to the interpretation in Kleene algebras and a variant thereof. We also prove strong completeness for language models, where each logic comes with a different interpretation. We show that for both logics the cut rule is admissible and both have a decidable consequence relation.