A note on propositional proof complexity of some Ramsey-type statements

Any valid Ramsey statement n −→ (k)2 2 can be encoded into a DNF formula RAM(n, k) of size O(nk) and with terms of size k 2 . Let rk be the minimal n for which the statement holds. We prove that RAM(rk, k) requires exponential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll [15]. As a consequence of Pudl´ak’s work in bounded arithmetic [19] it is known that there are quasi-polynomial size constant depth Frege proofs of RAM(4k, k), but the proof complexity of these formulas in resolution R or in its extension R(log) is unknown. We define two relativizations of the Ramsey statement that still have quasi-polynomial size constant depth Frege proofs but for which we establish exponential lower bound for R. The complexity of proving various Ramsey-type combinatorial statements is well studied in connection with Peano arithmetic or systems of second order arithmetic, or even with set theory. The foremost example is the ParisHarrington extension of fi...

• Type: Journal
• Year: 2011
• Where: AML
• Authors: Jan Krajícek
• Keywords: AML 2011, Constant Depth Frege, Mathematics, Ramsey Theorem, Size Constant Depth