__
TR03-034 | 17th March 2003 00:00
__

#### Height restricted constant depth LK

**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.