San Jose, California USA
June 8, 2011 to June 11, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CCC.2011.17
We study the proof complexity of Paris-Harrington's Large Ramsey Theorem for bi-colorings of graphs. We prove a non-trivial conditional lower bound in Resolution and a quasi-polynomial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in Res(2). We show that under such assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by adapting some constructions due to Erdos and Mills.
proof complexity, bounded-depth frege, resolution, ramsey
Nicola Galesi, Lorenzo Carlucci, "Paris-Harrington Tautologies", CCC, 2011, 2012 IEEE 27th Conference on Computational Complexity, 2012 IEEE 27th Conference on Computational Complexity 2011, pp. 93-103, doi:10.1109/CCC.2011.17