On non-monotonous properties of some classical and nonclassical propositional proof systems

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for the Frege systems, the sequent systems with cut rule and the systems of natural deductions of classical and nonclassical logics. We show that for these systems there are sequences of tautologies $\psi_n$, every one of which has unique minimal tautologies $\varphi_n$ such that for each $n$ the minimal proof lines of $\varphi_n$ are an order more than the minimal proof lines of $\psi_n$.