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.
J.Berger, H.Ishihara, T.Kihara and T.Nemoto, The binary expansion and the intermediate value theorem in constructive reverse mathematics, Arch. Math. Logic58(1–2) (2019), 203–217. doi:10.1007/s00153-018-0627-2.
2.
E.Bishop, Foundations of Constructive Analysis, McGraw-Hill Book Co., New York–Toronto, Ont.–London, 1967.
3.
V.Brattka and G.Gherardi, Weihrauch degrees, omniscience principles and weak computability, J. Symbolic Logic76(1) (2011), 143–176. doi:10.2178/jsl/1294170993.
4.
V.Brattka and G.Gherardi, Effective choice and boundedness principles in computable analysis, Bull. Symbolic Logic17(1) (2011), 73–117. doi:10.2178/bsl/1294186663.
5.
V.Brattka, G.Gherardi and A.Pauly, Weihrauch complexity in computable analysis, Preprint, https://arxiv.org/pdf/1707.03202.pdf.
6.
F.G.Dorais, Classical consequences of continuous choice principles from intuitionistic analysis, Notre Dame J. Form. Log.55(1) (2014), 25–39. doi:10.1215/00294527-2377860.
7.
F.G.Dorais, D.D.Dzhafarov, J.L.Hirst, J.R.Mileti and P.Shafer, On uniform relationships between combinatorial problems, Trans. Amer. Math. Soc.368(2) (2016), 1321–1359. doi:10.1090/tran/6465.
8.
F.G.Dorais, J.L.Hirst and P.Shafer, Reverse mathematics, trichotomy and dichotomy, J. Log. Anal.4(13) (2012), 1–14.
9.
D.D.Dzhafarov, Strong reductions between combinatorial principles, J. Symb. Log.81(4) (2016), 1405–1431. doi:10.1017/jsl.2016.1.
10.
Y.L.Ershov, S.S.Goncharov, A.Nerode, J.B.Remmel and V.W.Marek (eds), Handbook of Recursive Mathematics. Vol. 2. Recursive Algebra, Analysis and Combinatorics, Studies in Logic and the Foundations of Mathematics, Vol. 139, North-Holland, Amsterdam, 1998.
11.
M.Fujiwara, Intuitionistic provability versus uniform provability in RCA, in: Evolving Computability, Lecture Notes in Comput. Sci., Vol. 9136, Springer, Cham, 2015, pp. 186–195. doi:10.1007/978-3-319-20028-6_19.
12.
M.Fujiwara, Effective computability and constructive provability for existence sentences(abstract), Logic Colloquium 2016, The Bulletin of Symbolic Logic23 (2017), 241–242.
13.
M.Fujiwara and U.Kohlenbach, Classical provability of uniform versions and intuitionistic provability, Math. Log. Q.61(3) (2015), 132–150. doi:10.1002/malq.201300056.
14.
M.Fujiwara and U.Kohlenbach, Interrelation between weak fragments of double negation shift and related principles, J. Symb. Log.83(3) (2018), 991–1012. doi:10.1017/jsl.2017.63.
15.
M.Fujiwara and K.Yokoyama, A note on the sequential version of statements, in: The Nature of Computation, Lecture Notes in Comput. Sci., Vol. 7921, Springer, Heidelberg, 2013, pp. 171–180.
16.
J.L.Hirst, Combinatorics in subsystems of second order arithmetic, Thesis (Ph.D.) – The Pennsylvania State University, ProQuest LLC, Ann Arbor, MI, 1987.
17.
J.L.Hirst, Marriage theorems and reverse mathematics, in: Logic and Computation (Pittsburgh, PA, 1987), Contemp. Math., Vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 181–196. doi:10.1090/conm/106/1057822.
18.
J.L.Hirst, Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math.55(4) (2007), 303–316. doi:10.4064/ba55-4-2.
19.
J.L.Hirst and C.Mummert, Reverse mathematics and uniformity in proofs without excluded middle, Notre Dame J. Form. Log.52(2) (2011), 149–162. doi:10.1215/00294527-1306163.
20.
H.Ishihara, Constructive reverse mathematics: Compactness properties, in: From Sets and Types to Topology and Analysis, Oxford Logic Guides, Vol. 48, Oxford Univ. Press, Oxford, 2005, pp. 245–267. doi:10.1093/acprof:oso/9780198566519.003.0016.
21.
U.Kohlenbach, Higher order reverse mathematics, in: Reverse Mathematics 2001, Lecture Notes in Logic, Cambridge University Press, 2005, pp. 281–295.
22.
U.Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008.
23.
R.Kuyper, On Weihrauch reducibility and intuitionistic reverse mathematics, J. Symb. Log.82(4) (2017), 1438–1458. doi:10.1017/jsl.2016.61.
24.
S.G.Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Perspectives in Logic, Cambridge University Press, Cambridge, 2009.
25.
A.S.Troelstra (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344, Springer-Verlag, Berlin, New York, 1973.
26.
K.Weihrauch, Computable Analysis: An Introduction, Texts in Theoretical Computer Science. An EATCS Series, Springer-Verlag, Berlin, 2000.
