ECCC-Report TR10-153https://eccc.weizmann.ac.il/report/2010/153Comments and Revisions published for TR10-153en-usTue, 27 Sep 2011 19:09:54 +0300
Revision 2
| Paris-Harrington tautologies |
Lorenzo Carlucci,
Nicola Galesi,
Massimo Lauria
https://eccc.weizmann.ac.il/report/2010/153#revision2We 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.Tue, 27 Sep 2011 19:09:54 +0300https://eccc.weizmann.ac.il/report/2010/153#revision2
Revision 1
| Paris-Harrington tautologies |
Lorenzo Carlucci,
Nicola Galesi,
Massimo Lauria
https://eccc.weizmann.ac.il/report/2010/153#revision1We 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 Erd?s and MillsWed, 27 Apr 2011 07:51:10 +0300https://eccc.weizmann.ac.il/report/2010/153#revision1
Paper TR10-153
| Paris-Harrington tautologies |
Lorenzo Carlucci,
Nicola Galesi,
Massimo Lauria
https://eccc.weizmann.ac.il/report/2010/153We 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.Thu, 07 Oct 2010 15:48:47 +0200https://eccc.weizmann.ac.il/report/2010/153