Abstract:
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.