Combinatorial principles equivalent to weak induction
Caleb Davis, Denis R. Hirschfeldt, Jeffry L. Hirst, Jake Pardo, Arno Pauly, Keita Yokoyama · Computability · 2019
We consider two combinatorial principles, ERT and ECT. Both are easily proved in RCA0 plus Σ20 induction. We give two proofs of ERT in RCA0, using different methods to eliminate the use of Σ20 induction. Working in the weakened base system RCA0∗, we prove that ERT is equivalent to Σ10 induction and ECT is equivalent to Σ20 induction. We conclude with a Weihrauch analysis of the principles, showing ERT≡WLPO∗