Skip to main content
2 of 2
deleted 46 characters in body
Bjørn Kjos-Hanssen
  • 24.8k
  • 3
  • 58
  • 114

They show that $\DeclareMathOperator{\WKL}{WKL}\DeclareMathOperator{\RT}{RT}\DeclareMathOperator{\RCA}{RCA} \RT^2_2$ is $\Pi^0_3$-conservative over $\RCA_0$. Thus, there is no way that $\RT^2_2$ can be essential in a proof of simple first-order statements like for instance the twin prime conjecture, that have a $\Pi^0_3$ form: $$ (\forall n)(\exists p>n)(p\text{ is prime and }p+2\text{ is prime.}) $$ (This is $\Pi^0_2$ which is, in particular, $\Pi^0_3$.)

First-order means you quantify over numbers only, whereas $\RT^2_2$ itself involves quantifying over sets of numbers, making it second order.

For comparison, Leo Harrington (1978) showed that $\WKL_0$ (weak König's lemma) is $\Pi^1_1$-conservative, hence in particular also $\Pi^0_3$-conservative, over $\RCA_0$.

Bjørn Kjos-Hanssen
  • 24.8k
  • 3
  • 58
  • 114