Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

Partial consistency statements can be expressed as polynomial-size propositional formulas. Frege proof systems have polynomial-size partial self-consistency proofs. Frege proof systems have polynomial-size proofs of partial consistency of extended Frege proof systems if and only if Frege proof systems polynomially simulate extended Frege proof systems. We give a new proof of Reckhow's theorem that any two Frege proof systems p-simulate each other. The proofs depend on polynomial size propositional formulas defining the truth of propositional formulas. These are already known to (...) exist since the Boolean formula value problem is in alternating logarithmic time; this paper presents a proof of this fact based on a construction which is somewhat simpler than the prior proofs of Buss and of Buss-Cook- Gupta-Ramachandran. (shrink)