Height restricted constant depth LK is a natural restriction of
Gentzen's propositional proof system LK. A sequence of LK-formulas
has polylogarithmic-height restricted depth-d-LK proofs iff the
n-th formula in the sequence possesses LK-proofs where cut-formulas
are of depth d+1 with small bottom fanin
and of size quasi-polynomial in n, and the height of
the proof tree is bounded polylogarithmic in n. We will proof a
separation of polylogarithmic-height restricted depth-d-LK proofs
from quasi-polynomial-size tree-like depth-d-LK proofs using the
order induction principle. Our lower bounds technique utilizes
Hastad's Switching Lemmas to obtain so called "cut-reduction
by switching".

We will further explain the connection of height restricted constant
depth LK to theories of relativized bounded arithmetic. Separations
of height restricted constant depth LK in turn yield separations of
relativized bounded arithmetic.