This work studies Craig interpolation for the logic \(\texttt{SkNMILL}\) , a substructural logic supporting only directed versions of the structural rules of associativity and unitality. In this setting, Craig interpolation cannot be proved by directly employing standard proof-theoretic methods, such as Maehara’s method, a situation that \(\texttt{SkNMILL}\) shares with other logical systems such as the product-free Lambek calculus and the implicational fragment of intuitionistic logic. We show how to overcome this issue and appropriately modify Maehara’s method for recovering Craig interpolation. We take one step further and, following the category-theoretic perspective of Čubrić, we produce a proof-relevant version of the interpolation theorem, in which we show that our interpolation procedures are right inverses of the admissible cut rules. All our results have been formalized in the proof assistant Agda.
