From Nonstandard Analysis to various flavours of Computability Theory

TL;DR

This paper explores how theorems from Nonstandard Analysis can be translated into results in both classical and higher-order computability theory, expanding the scope of NSA's influence.

Contribution

It demonstrates that NSA theorems can be applied to classical computability theory through textbook proofs, complementing existing higher-order results.

Findings

NSA theorems yield classical computability results via textbook proofs

NSA results are applicable to higher-order computability theory

The paper bridges NSA and classical computability through proof analysis

Abstract

As suggested by the title, it has recently become clear that theorems of Nonstandard Analysis (NSA) give rise to theorems in computability theory (no longer involving NSA). Now, the aforementioned discipline divides into classical and higher-order computability theory, where the former (resp. the latter) sub-discipline deals with objects of type zero and one (resp. of all types). The aforementioned results regarding NSA deal exclusively with the higher-order case; we show in this paper that theorems of NSA also give rise to theorems in classical computability theory by considering so-called textbook proofs.