2

(One formulation of) Ramsey's theorem states that any colouring of edges of the complete graph with $4^n$ vertices with two colours will contain a monochromatic clique of size $n$. I am new to proof complexity and what interests me is the complexity of proving the upper bound using the sum-of-squares proof system. Do we know any upper bound or degree lower bounds for this question?

A related question is: which is the weakest proof system in which we know that Ramsey's theorem is provable? I am aware of a result due to Pudlák [P] which shows that this is possible in bounded arithmetic (i.e., $S_2$ and then shown by Jeřábek [J] to be $T_2^3$ precisely). Do we know of anything weaker?

[P]: Pudlák, Ramsey's theorem in bounded arithmetic, CSL 1990

[J]: Jeřábek, Approximate counting by hashing in bounded arithmetic, Journal of Symbolic Logic, 2009

ckamath
  • 223
  • 1
  • 5
  • 1
    As for bounded arithmetic, I believe nothing better than $T^1_2+\mathit{rWPHP}(PV_2)$ (which is included in $T^3_2$) is known. As for propositional proof systems, lower bounds are known for resolution (see Lauria, Pudlák, Rödl, Thapen: The complexity of proving that a graph is Ramsey) and cutting planes (Lauria: A rank lower bound for cutting planes proofs of Ramsey's theorem); I don’t know if there are any SoS lower bounds. – Emil Jeřábek Jul 08 '21 at 14:34
  • Thanks, Emil. I would accept that as an answer. – ckamath Jul 08 '21 at 15:22
  • I suppose by $rWPHP$ you are referring to relational $WPHP$? – ckamath Jul 08 '21 at 15:27
  • 1
    No, retraction-pair WPHP, as in my paper that you linked to. – Emil Jeřábek Jul 08 '21 at 15:42

0 Answers0