In this paper, we highlight a new computational aspect of Nonstandard Analysis relating to higher-order computability theory. In particular, we prove that the Gandy–Hyland functional equals a primitive recursive functional involving nonstandard numbers inside Nelson’s internal set theory. From this classical and ineffective proof in Nonstandard Analysis, a term from Gödel’s system T can be extracted which computes the Gandy–Hyland functional in terms of a modulus-of-continuity functional and the special fan functional. We obtain several similar relative computability results not involving Nonstandard Analysis from their associated nonstandard theorems. By way of reversal, we show that certain relative computability results, called Herbrandisations, also imply the nonstandard theorem from whence they were obtained. Thus, we establish a direct two-way connection between the field Computability (in particular theoretical computer science) and the field Nonstandard Analysis.
S.Albeverio, R.Høegh-Krohn, J.E.Fenstad and T.Lindstrøm, Nonstandard Methods in Stochastic Analysis and Mathematical Physics, Pure and Applied Mathematics, Vol. 122, Academic Press, 1986, xii + 514.
2.
M.J.Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und Ihrer Grenzgebiete, Vol. 6, Springer, 1985, Metamathematical studies, xxiii + 466.
3.
U.Berger and P.Oliva, Modified bar recursion and classical dependent choice, in: LC01, Lect. Notes Log., Vol. 20, 2005, pp. 89–107.
4.
U.Berger and P.Oliva, Modified bar recursion, Math. Structures Comput. Sci.16(2) (2006), 163–183. doi:10.1017/S0960129506005093.
5.
S.R.Buss, An introduction to proof theory, in: Handbook of Proof Theory, Stud. Logic Found. Math., Vol. 137, North-Holland, Amsterdam, 1998, pp. 1–78.
6.
D.D.Dzhafarov, Reverse Mathematics Zoo. Available at http://rmzoo.uconn.edu/.
7.
Y.L.Ershov, Model C of partial continuous functionals, in: Logic Colloquium 76, Studies in Logic and Foundations in Math., Vol. 87, North-Holland, 1977, pp. 455–467.
8.
M.Escardó, P.Oliva and T.Powell, System T and the product of selection functions, in: Computer Science Logic 2011, LIPIcs. Leibniz Int. Proc. Inform., Vol. 12, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2011, pp. 233–247.
9.
M.Escardó and C.Xu, The inconsistency of a Brouwerian continuity principle with the Curry–Howard interpretation, in: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 38, 2015, pp. 153–164.
10.
R.Gandy and M.Hyland, Computable and recursively countable functions of higher type, in: Logic Colloquium, Studies in Logic and Found. Math., Vol. 87, North-Holland, 1977, pp. 407–438.
11.
K.Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica12 (1958), 280–287. doi:10.1111/j.1746-8361.1958.tb01464.x.
12.
U.Kohlenbach, Foundational and mathematical uses of higher types, in: Reflections on the Foundations of Mathematics (Stanford, CA, 1998), Lect. Notes Log., Vol. 15, ASL, 2002, pp. 92–116.
13.
U.Kohlenbach, Higher order reverse mathematics, in: Reverse Mathematics 2001, Lect. Notes Log., Vol. 21, ASL, 2005, pp. 281–295.
14.
U.Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin, 2008, xx + 532.
15.
J.Longley and D.Normann, Higher-Order Computability, Theory and Applications of Computability, Springer, 2015.
16.
E.Nelson, Internal set theory: A new approach to Nonstandard Analysis, Bull. Amer. Math. Soc.83(6) (1977), 1165–1198. doi:10.1090/S0002-9904-1977-14398-X.
17.
D.Normann, Recursion on the Countable Functionals, LNM, Vol. 811, Springer, 1980, viii + 191.
18.
D.Normann, Characterizing the continuous functionals, J. Symbolic Logic48(4) (1983), 965–969.
19.
D.Normann, E.Palmgren and V.Stoltenberg-Hansen, Hyperfinite type structures, J. Symbolic Logic64(3) (1999), 1216–1242. doi:10.2307/2586626.
20.
D.Normann and S.Sanders, Nonstandard Analysis, Computability Theory, and their connections, 2017. Submitted. Available at https://arxiv.org/abs/1702.06556.
21.
A.Robinson, Non-Standard Analysis, North-Holland, Amsterdam, 1966, xi + 293.
22.
S.Sanders, Taming the Reverse Mathematics zoo, 2014. Submitted. Available at http://arxiv.org/abs/1412.2022.
23.
S.Sanders, The unreasonable effectiveness of Nonstandard Analysis, 2015. Submitted. Available at http://arxiv.org/abs/1508.07434.
24.
S.G.Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Perspectives in Logic, CUP, 2009, xvi + 444.
25.
R.I.Soare, Recursively Enumerable Sets and Degrees, Perspectives in Mathematical Logic, Springer, 1987, xviii + 437.
26.
A.S.Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344, Springer, Berlin, 1973, xv + 485.
27.
B.van den Berg, E.Briseid and P.Safarik, A functional interpretation for nonstandard arithmetic, Ann. Pure Appl. Logic163(12) (2012), 1962–1994. doi:10.1016/j.apal.2012.07.003.
28.
B.van den Berg and S.Sanders, Transfer equals Comprehension, 2014. Available at http://arxiv.org/abs/1409.6881.
