English

Combinatorial principles equivalent to weak induction

Logic 2018-12-27 v1

Abstract

We consider two combinatorial principles, ERT{\sf{ERT}} and ECT{\sf{ECT}}. Both are easily proved in RCA0{\sf{RCA}}_0 plus Σ20{\Sigma^0_2} induction. We give two proofs of ERT{\sf{ERT}} in RCA0{\sf{RCA}}_0, using different methods to eliminate the use of Σ20{\Sigma^0_2} induction. Working in the weakened base system RCA0{\sf{RCA}}_0^*, we prove that ERT{\sf{ERT}} is equivalent to Σ10{\Sigma^0_1} induction and ECT{\sf{ECT}} is equivalent to Σ20{\Sigma^0_2} induction. We conclude with a Weihrauch analysis of the principles, showing ERTWLPO<WTCNWECT{\sf{ERT}} {\equiv_{\rm W}} {\sf{LPO}}^* {<_{\rm W}}{{\sf{TC}}_{\mathbb N}}^* {\equiv_{\rm W}} {\sf{ECT}}.

Cite

@article{arxiv.1812.09943,
  title  = {Combinatorial principles equivalent to weak induction},
  author = {Caleb Davis and Denis R. Hirschfeldt and Jeffry L. Hirst and Jake Pardo and Arno Pauly and Keita Yokoyama},
  journal= {arXiv preprint arXiv:1812.09943},
  year   = {2018}
}
R2 v1 2026-06-23T06:55:25.632Z