Intuitionistic BV (Extended version)

TL;DR

The paper develops two intuitionistic non-commutative logics, $\mathsf{IBV}$ and $\mathsf{INML}$, as intuitionistic counterparts to $\mathsf{BV}$ and $\mathsf{NML}$. It introduces a deep-inference proof system for $\mathsf{IBV}$ with a splitting lemma that yields cut elimination, and proves $\mathsf{IBV}$ conservatively extends $\mathsf{IMLL}$ while relating to the unit-free BV via $\mathsf{IBV^-}$. It then defines $\mathsf{INML}$ (non-associative $\lseq$) with a cut-free sequent calculus and shows $\mathsf{INML}$ conservatively extends $\mathsf{IMLL}$; $\mathsf{IBV}$ is recovered from $\mathsf{INML}$ by adding associative cut rules, linking the associative and non-associative frameworks. A flat translation connects unit-free variants of $\mathsf{IBV}$ and $\mathsf{BV}$, establishing conservative equivalences and clarifying how these systems extend $\mathsf{IMLL}$ and relate to $\mathsf{NML}$. Overall, the work provides a rigorous framework for intuitionistic, non-commutative logics with robust proof-theoretic properties and potential typing applications for imperative languages.

Abstract

We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.

Figures (11)

• Figure 1: Proof systems discussed in this paper. The ones in the boxes are new.
• Figure 2: Inference rules for system $\mathsf{IBV}$
• Figure 3: Additional rules for $\mathsf{SIBV}$.
• Figure 4: Derivability of $\mathsf{i}_\downarrow^\circ$ in $\mathsf{IBV}$.
• Figure 5: Using $\mathsf{i}_\uparrow^\bullet$ to derive $\mathsf{q}_\uparrow^\circ$ and $\mathsf{q}_\uparrow^\bullet$

Theorems & Definitions (72)

• remark 1
• lemma 1
• proof
• lemma 2
• proof
• theorem 1: Deduction Theorem
• proof
• corollary 1
• proof
• corollary 2: Modus Ponens