We investigate the problem how to lift the non - $\forall \Sigma^b_1(\alpha)$ - conservativity of $T^2_2(\alpha)$ over $S^2_2(\alpha)$ to the expected non - $\forall \Sigma^b_i(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $S^{i+1}_2(\alpha)$ , for $i > 1$ . We give a non-trivial refinement of the “lifting method” developed in [4,8], and we prove a sufficient condition on a $\forall \Sigma^b_1(f)$ -consequence of $T_2(f)$ to yield the non-conservation result. Further we prove that Ramsey's theorem, a $\forall \Sigma^b_1(\alpha)$ - formula, is not provable (...) in $T^1_2(\alpha)$ , and that $\forall \Sigma^b_j(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $T^{i}_2(\alpha)$ implies $\forall \Sigma^b_j(\alpha)$ - conservativity of the whole $T_2(\alpha)$ over $T^{i}_2(\alpha)$ , for any $j \geq 2$. (shrink)

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...) principle. (shrink)