The size of linear derivations in deep inference


In unit-free deep inference it is known that derivations comprising of just the logical rules (switch and medial) are polynomial in size. When units are thrown in this picture changes drastically, as exhibited here. Nonetheless we show that such derivations can always be converted to ones of polynomial size, preserving the premiss and conclusion, without using structural rules.

NB: This note has been superseded by the article Rewriting with linear inferences in propositional logic.