We study the proof complexity of Paris-Harrington’s Large Ramsey Theorem for bi-colorings of graphs and of off-diagonal Ramsey’s Theorem. For Paris-Harrington, we prove a non-trivial conditional lower bound in Resolution and a non-trivial 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 an assumption, there is no refutation of the Paris-Harrington formulas of size quasipolynomial 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 off-diagonal Ramsey principle is established. This is obtained by adapting some constructions due to Erdos and Mills. ˝ We prove a non-trivial Resolution lower bound for a family of such off-diagonal Ramsey principles.

On the proof complexity of Paris-harrington and off-diagonal ramsey tautologies / Carlucci, Lorenzo; Galesi, Nicola; Lauria, Massimo. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - ELETTRONICO. - 17:4(2016), pp. 1-25. [10.1145/2946801]

On the proof complexity of Paris-harrington and off-diagonal ramsey tautologies

CARLUCCI, LORENZO;GALESI, NICOLA;LAURIA, MASSIMO
2016

Abstract

We study the proof complexity of Paris-Harrington’s Large Ramsey Theorem for bi-colorings of graphs and of off-diagonal Ramsey’s Theorem. For Paris-Harrington, we prove a non-trivial conditional lower bound in Resolution and a non-trivial 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 an assumption, there is no refutation of the Paris-Harrington formulas of size quasipolynomial 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 off-diagonal Ramsey principle is established. This is obtained by adapting some constructions due to Erdos and Mills. ˝ We prove a non-trivial Resolution lower bound for a family of such off-diagonal Ramsey principles.
2016
Paris-Harrington's principle; proof complexity; Ramsey's theorem; resolution; theoretical computer science; computer science (all); logic; computational mathematics
01 Pubblicazione su rivista::01a Articolo in rivista
On the proof complexity of Paris-harrington and off-diagonal ramsey tautologies / Carlucci, Lorenzo; Galesi, Nicola; Lauria, Massimo. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - ELETTRONICO. - 17:4(2016), pp. 1-25. [10.1145/2946801]
File allegati a questo prodotto
File Dimensione Formato  
Carlucci_Proof-complexity_2016.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 321.99 kB
Formato Adobe PDF
321.99 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/902288
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact