A parity-based Frege proof for the symmetric pigeonhole principle.
Steve Firebaugh · Notre Dame Journal of Formal Logic · 1993
Sam Buss produced the first polynomial size Frege proof of the pigeonhole principle.We introduce a variation of that problem and produce a simpler proof based on parity.The proof appearing here has an upper bound that is quadratic in the size of the input formula.