A Syntactic Approach to Maksimova's Principle of Variable Separation for Some Substructural Logics
H. Naruse, H. Ono, Bayu Surarso · Notre Dame Journal of Formal Logic · 1998
Maksimova's principle of variable separation says that if propositional formulas $A_1 \supset A_2$ and $B_1 \supset B_2$ have no propositional variables in common and if a formula $A_1\wedge B_1 \supset A_2\vee B_2$ is provable, then either $A_1 \supset A_2$ or $B_1 \supset B_2$ is provable. Results on Maksimova's principle until now are obtained mostly by using semantical arguments. In the present paper, a proof-theoretic approach to this principle in some substructural logics is given, which analyzes a given cut-free proof of the formula $A_1\wedge B_1 \supset A_2\vee B_2$ and examines how the formula is derived. This analysis will make clear why Maksimova's principle holds for these logics.