Paris-Harrington tautologies

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington’s Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.

• Type: Journal
• Year: 2010
• Where: ECCC
• Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria
• Keywords: ECCC 2010, Large Ramsey Theorem, Proof Complexity, Quasipolynomial Upper Bound