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.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.