Made with higher types
To be or not to be constructive: that is not the question (arxiv link)
Sam Sanders
The aim of this paper is to show that (classical) Nonstandard Analysis (NSA hereafter) inhabits the twilight zone between constructive and non-constructive mathematics. Intuitively speaking, we develop the idea that the fundamental predicate 'is standard' can be interpreted as 'is computationally relevant', while the usual 'law of excluded middle' is a computationally neutral principle in NSA.
The paper starts (essentially) from scratch and contains a detailed introduction of NSA. An overview of the computational and constructive aspects of NSA is given. Some philosophical considerations are discussed.
This paper was originally published here, in Indagationes Mathematicae.
Formalism 16 (arxiv link)
Sam Sanders
The aim of this paper is to debunk the Bishop-Connes critique of Nonstandard Analysis. Their critique, while based on very different motivations, is centered around the same idea, namely that Nonstandard Analysis somehow lacks any and all computational content. We show this idea to be baseless using a number of elementary examples. This paper was originally published here, in Synthese.