On polynomial size Frege proofs of certain combinatorial principles
Peter Clote · 1993
Abstract Using a theorem of Barrington, we give a new recursion theoretic characterization of the class of ALOGT IM E computable functions and then introduce a corresponding free-variable equational calculus ALV′. The system ALV′, more elegant than an earlier system ALV, allows straightforward definitions of parity and other counting predicates, as well as the proof of correctness of these predicates. One thus easily obtains polynomial size Frege proofs for certain combinatorial principles such as the pigeonhole principle (S.R. Buss) and the equipartition principle (A. Goerdt).