Weihrauch and constructive reducibility between existence statements

Article type: Research Article

Authors: Fujiwara, Makoto^{; *}

Affiliations: School of Science and Technology, Meiji University, Kanagawa, Japan. makotofujiwara@meiji.ac.jp

Correspondence: [*] Corresponding author. makotofujiwara@meiji.ac.jp.

Abstract: We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical to some formal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas. In addition, we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics.

Keywords: Foundations of mathematics, Weihrauch reducibility, reverse mathematics, constructive mathematics, finite-type arithmetic, existence statements

DOI: 10.3233/COM-190278

Journal: Computability, vol. 10, no. 1, pp. 17-30, 2021