This Article 
 Bibliographic References 
 Add to: 
2011 26th Annual IEEE Conference on Computational Complexity
Paris-Harrington Tautologies
San Jose, California USA
June 08-June 11
ISBN: 978-0-7695-4411-3
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.
Index Terms:
proof complexity, bounded-depth frege, resolution, ramsey
Lorenzo Carlucci, Nicola Galesi, Massimo Lauria, "Paris-Harrington Tautologies," ccc, pp.93-103, 2011 26th Annual IEEE Conference on Computational Complexity, 2011
Usage of this product signifies your acceptance of the Terms of Use.