Unpublished report:
Samuel R. Buss and Rosalie Iemhoff.
"The Depth of Intuitionistic Cut Free Proofs."
Unpublished manuscript, 2003.
Download preliminary article: postscript or PDF.
Abstract: We prove a quadratic upper bound for the depth of cut free proofs in propositional intuitionistic logic formalized with Gentzen's sequent calculus. We discuss bounds on the necessary number of reuses of left implication rules. We exhibit an example showing that this quadratic bound is optimal. As a corollary, this gives a new proof that propositional validity for intuitionistic logic is in PSPACE.