Combinatorial principles equivalent to weak induction

Issue title: Dagstuhl Seminar on Measuring the Complexity of Computational Content 2018

Guest editors: Vasco Brattka, Damir D. Dzhafarov, Alberto Marcone and Arno Pauly

Article type: Research Article

Authors: Davis, Caleb^{a; *} | Hirschfeldt, Denis R.^b | Hirst, Jeffry^c | Pardo, Jake^d | Pauly, Arno^e | Yokoyama, Keita^f

Affiliations: [a] Department of Mathematical Sciences, Appalachian State University, NC, USA. davisc3@appstate.edu | [b] Department of Mathematics, The University of Chicago, IL, USA. drh@math.uchicago.edu | [c] Department of Mathematical Sciences, Appalachian State University, NC, USA. hirstjl@appstate.edu | [d] Department of Mathematical Sciences, Appalachian State University, NC, USA. pardo@alumni.nd.edu | [e] Department of Computer Science, Swansea University, United Kingdom. arno.m.pauly@gmail.com | [f] School of Information Science, Japan Advanced Institute of Science and Technology, Japan. y-keita@jaist.ac.jp

Correspondence: [*] Corresponding author. davisc3@appstate.edu.

Abstract: 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∗<WTCN∗≡WECT.

Keywords: Reverse mathematics, Weihrauch reduction, induction

DOI: 10.3233/COM-180244

Journal: Computability, vol. 9, no. 3-4, pp. 219-229, 2020