<p>(One formulation of) <a href="https://en.wikipedia.org/wiki/Ramsey%27s_theorem" rel="nofollow noreferrer">Ramsey's theorem</a> states that any colouring of edges of the complete graph with <span class="math-container">$4^n$</span> vertices with two colours will contain a monochromatic clique of size <span class="math-container">$n$</span>. I am new to proof complexity and what interests me is the complexity of proving the <em>upper bound</em> using the <a href="https://cstheory.stackexchange.com/questions/14400/sum-of-squares-proof-system?rq=1">sum-of-squares</a> proof system. Do we know any upper bound or degree lower bounds for this question?</p>
<p>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., <span class="math-container">$S_2$</span> and then shown by Jeřábek [J] to be <span class="math-container">$T_2^3$</span> precisely). Do we know of anything weaker?</p>
<p>[P]: Pudlák, <em><a href="https://link.springer.com/chapter/10.1007/3-540-54487-9_67" rel="nofollow noreferrer">Ramsey's theorem in bounded arithmetic</a></em>, CSL 1990</p>
<p>[J]: Jeřábek, <em><a href="https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/approximate-counting-by-hashing-in-bounded-arithmetic/A9694B6029ED684543A15FEFCEC9F610" rel="nofollow noreferrer">Approximate counting by hashing in bounded arithmetic</a></em>, Journal of Symbolic Logic, 2009</p>

CC BY-SA 4.0
2021-07-08T14:34:30.987Z
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
CC BY-SA 4.0
2021-07-08T15:22:23.627Z
Thanks, Emil. I would accept that as an answer.
ckamath
CC BY-SA 4.0
2021-07-08T15:27:15.113Z
I suppose by $rWPHP$ you are referring to relational $WPHP$?
ckamath
CC BY-SA 4.0
2021-07-08T15:42:25.973Z
No, retraction-pair WPHP, as in my paper that you linked to.
Emil Jeřábek
<reference-request><sum-of-squares><ramsey-theory>
Complexity of (Graph) Ramsey Theorem in Sum-of-Squares Proof System
ckamath
# Complexity of (Graph) Ramsey Theorem in Sum-of-Squares Proof System

(Asked by: username_0 on 2021-07-08)

(One formulation of) [Ramsey's theorem](https://en.wikipedia.org/wiki/Ramsey%27s_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](https://cstheory.stackexchange.com/questions/14400/sum-of-squares-proof-system?rq=1) 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](https://link.springer.com/chapter/10.1007/3-540-54487-9_67)*, CSL 1990

[J]: Jeřábek, *[Approximate counting by hashing in bounded arithmetic](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/approximate-counting-by-hashing-in-bounded-arithmetic/A9694B6029ED684543A15FEFCEC9F610)*, Journal of Symbolic Logic, 2009

**Tags:** reference-request, sum-of-squares, ramsey-theory

> **Comments:**
> **username_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.  
> **username_0**: Thanks, Emil. I would accept that as an answer.  
> **username_0**: I suppose by $rWPHP$ you are referring to relational $WPHP$?  
> **username_1**: No, retraction-pair WPHP, as in my paper that you linked to.  

---

## 0 answers

