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
Journal: Computability, vol. Pre-press, no. Pre-press, pp. 1-14, 2020