Combinatorial Principles Equivalent to Weak Induction

by Caleb Davis, Denis R. Hirschfeldt, Jeffry L. Hirst, Jake Pardo, Arno Pauly, and Keita Yokoyama

Status: Computability 9 (2020) 219 - 229

Availability: online journal version and preprint

Abstract. We consider two combinatorial principles, ERT and ECT. Both are easily proved in RCA0 plus Σ02 induction. We give two proofs of ERT in RCA0, using different methods to eliminate the use of Σ02 induction. Working in the weakened base system RCA0*, we prove that ERT is equivalent to Σ01 induction and ECT is equivalent to Σ02 induction. We conclude with a Weihrauch analysis of the principles, showing ERT ≡W LPO* <W TCN*W ECT.