A \(\Pi^0_1\)-bounded fragment of infinitary action logic with exponential
Infinitary action logic is an extension of the multiplicative-additive Lambek calculus with Kleene iteration, axiomatized by an 𝜔-rule. Buszkowski and Palka (2007) show that this logic is \(\Pi^0_1\)-complete. As shown recently by Kuznetsov and Speranski, the extension of infinitary action logic with the exponential modality is much harder: \(\Pi^1_1\)-complete. The raise of complexity is of course due to the contraction rule. We investigate fragments of infinitary action logic with exponential, which still include contraction, but have lower (e.g., arithmetically bounded) complexity. In this paper, we show an upper \(\Pi^0_1\) bound for the fragment of infinitary action logic, in which the exponential can be applied only to formulae of implication depth 0 or 1.