2
$\begingroup$

(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

Improve this question
$\endgroup$
4
  • 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$
    – Emil Jeřábek
    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$
    – Emil Jeřábek
    Jul 8, 2021 at 15:42

0

Reset to default

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.