# To be or not to be constructive, that is not the question

## TL;DR

This paper explores the nuanced spectrum between constructive and non-constructive mathematics, demonstrating that classical Nonstandard Analysis exhibits properties of both, and formalizes its local constructiveness.

## Contribution

It challenges the binary classification of mathematics as either constructive or non-constructive by analyzing classical Nonstandard Analysis as a twilight-zone example.

## Key findings

- Classical Nonstandard Analysis can be interpreted as locally constructive.
- The predicate 'x is standard' can be seen as 'x is computable'.
- Results formalize Osswald's conjecture on the local constructiveness of Nonstandard Analysis.

## Abstract

In the early twentieth century, L.E.J. Brouwer pioneered a new philosophy of mathematics, called intuitionism. Intuitionism was revolutionary in many respects but stands out -mathematically speaking- for its challenge of Hilbert's formalist philosophy of mathematics and rejection of the law of excluded middle from the 'classical' logic used in mainstream mathematics. Out of intuitionism grew intuitionistic logic and the associated Brouwer-Heyting-Kolmogorov interpretation by which 'there exists x' intuitively means 'an algorithm to compute x is given'. A number of schools of constructive mathematics were developed, inspired by Brouwer's intuitionism and invariably based on intuitionistic logic, but with varying interpretations of what constitutes an algorithm. This paper deals with the dichotomy between constructive and non-constructive mathematics, or rather the absence of such an 'excluded middle'. In particular, we challenge the 'binary' view that mathematics is either constructive or not. To this end, we identify a part of classical mathematics, namely classical Nonstandard Analysis, and show it inhabits the twilight-zone between the constructive and non-constructive. Intuitively, the predicate 'x is standard' typical of Nonstandard Analysis can be interpreted as 'x is computable', giving rise to computable (and sometimes constructive) mathematics obtained directly from classical Nonstandard Analysis. Our results formalise Osswald's longstanding conjecture that classical Nonstandard Analysis is locally constructive. Finally, an alternative explanation of our results is provided by Brouwer's thesis that logic depends upon mathematics.