The Community for Technology Leaders
2011 IEEE 26th Annual Conference on Computational Complexity (2011)
San Jose, California USA
June 8, 2011 to June 11, 2011
ISSN: 1093-0159
ISBN: 978-0-7695-4411-3
pp: 93-103
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

N. Galesi, M. Lauria and L. Carlucci, "Paris-Harrington Tautologies," 2011 IEEE 26th Annual Conference on Computational Complexity(CCC), San Jose, California USA, 2011, pp. 93-103.
93 ms
(Ver 3.3 (11022016))