Constructive mathematics plus existence of discontinuous functions

120 Views Asked by At

Bishop's constructive mathematics (BISH) is meant to be the intersection of the theories of Brouwer, early Recursion Theory, and classical mathematics, and so it can be modelled by any model for the latter (so, e.g. it doesn't contradict classical mathematics). Brouwer's Intuitionist mathematics and Recursion Theory both imply that all functions are continuous (and computable).

I'm curious from the standpoint of reverse mathematics, if we take BISH+the existence of a discontinuous function, say, the Heaviside function, how strong is the resulting theory? For instance, does that allow you to prove any kind of omniscience (Bishop's language) or choice?

1

There are 1 best solutions below

0
On BEST ANSWER

The existence of any function $f:[0,1] \to (-\infty,0) \cup (0,\infty)$ with $f(0) < 0$ and $f(1) > 0$ implies WLPO for the natural numbers.

(For the special case of (a slight modification of) the Heaviside function defined as a total function with $H(x) = -1$ for $x \leq 0$ and $H(x) = 1$ otherwise, you can skip to the last paragraph and read all references to '$L$' and '$a_n$' as $0$ and $2^{-n}$ respectively.)

We define the sequences $l_n$ and $u_n$ as follows:

$l_0 = 0$ and $u_0 = 1$. If $f(\frac{l_n + u_n}{2}) < 0$ then $l_{n+1} = \frac{l_n + u_n}{2}$ and $u_{n+1} = u_n$. Otherwise, $l_{n+1} = l_n$ and $u_{n+1} = \frac{l_n + u_n}{2}$. (Note that $<0$ is a decidable predicate on $(-\infty,0) \cup (0,\infty)$, so this is a constructively valid definition.)

These sequences are both Cauchy sequences with common limit $L$. Moreover, $f(l_n)$ are always negative and $f(u_n)$ are always positive. If $f(L) > 0$ we define $a_n = l_n$ and if $f(L) < 0$ we define $a_n = u_n$; this gives us a Cauchy sequence $a_n$ where every value of $f(a_n)$ has different sign to $f(L)$.

Now, given a decidable predicate $\phi$ on $\mathbb N$, let $\bar n$ be the least element of $\{n\} \cup \{k :\mathbb N \mid \neg \phi(k)\}$ (so $n = \bar n$ iff $\phi(k)$ holds for all $k < n$), and let $A$ be the limit of the Cauchy sequence $a_{\bar n}$. Depending on whether $f(L)$ and $f(A)$ have the same sign, $\forall n:\mathbb N. n = \bar n$ is either true or false, so $\forall n:\mathbb N. \phi(n)$ is decidable. Hence WLPO holds.