(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

  • 1
    $\begingroup$ 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. $\endgroup$ Jul 8, 2021 at 14:34
  • $\begingroup$ Thanks, Emil. I would accept that as an answer. $\endgroup$
    – ckamath
    Jul 8, 2021 at 15:22
  • $\begingroup$ I suppose by $rWPHP$ you are referring to relational $WPHP$? $\endgroup$
    – ckamath
    Jul 8, 2021 at 15:27
  • 1
    $\begingroup$ No, retraction-pair WPHP, as in my paper that you linked to. $\endgroup$ Jul 8, 2021 at 15:42


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.