Skip to main content
deleted 46 characters in body
Source Link
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 ``The twin prime conjecture is true'' etc.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.

This is a very interesting and impressive result. It is not the first of its kindFor comparison, though: Leo Harrington (1978) showed decades ago that another system $\WKL_0$ (weak König's lemma) is $\Pi^1_1$-conservative, hence in particular also $\Pi^0_3$-conservative, over $\RCA_0$.

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 ``The twin prime conjecture is true'' etc. 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.

This is a very interesting and impressive result. It is not the first of its kind, though: Leo Harrington showed decades ago that another system $\WKL_0$ (weak König's lemma) is $\Pi^1_1$-conservative over $\RCA_0$.

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$.

Source Link
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 ``The twin prime conjecture is true'' etc. 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.

This is a very interesting and impressive result. It is not the first of its kind, though: Leo Harrington showed decades ago that another system $\WKL_0$ (weak König's lemma) is $\Pi^1_1$-conservative over $\RCA_0$.