Approximation and Small-Depth Frege Proofs
Stephen J. Bellantoni, Toniann Pitassi, Alasdair Urquhart · SIAM Journal on Computing · 1992
Ajtai [Proceedings of the 29th Annual IEEE Symposium on the Foundations of Computer Science, White Plains, NY, 1988, pp. 346–355; preliminary version] recently proved that if for some fixed d, every formula in a Frege proof of the propositional pigeonhole principle ${\text{PHP}}_n $ has depth at most d, then the proof size is not less than any polynomial in n. By introducing the notion of an “approximate proof” this paper demonstrates how to eliminate the nonstandard model theory, including the nonconstructive use of the compactness theorem, from Ajtai’s lower bound. An approximate proof is one in which each inference is sound on a subset of the possible truth assignments—possibly a different subset for each inference. This paper also shows how to improve the lower bound, giving a specific superpolynomial function $(n^{\Omega (\log ^{[d + 1]} n)} )$ bounding the proof size from below.