When I started to write this question I was really confused, but now I think I am starting to get it. Nonetheless I'd like some confirmation that my understanding is correct.
I have read, heard said, and even said myself that in Bishop-style constructive mathematics all functions are continuous—even computable. (Update: This last sentece was poorly worded. See Carl's correction below.) (This isn't an axiom or a constructively provable fact. It just is that one cannot constructively prove the existence of a discontinuous function.) I am starting to realize this is not quite as straight-forward as I thought, so I'd like some clarification.
The issue seems to arise when one defines a function $f:A \rightarrow \mathbb{R}$ where $A$ is a subset of a set $X$. (Bishop understands a subset to be an (computable) imbedding $i: A \hookrightarrow X$.) To complicate matters Bishop calls the space of such functions $\mathcal{F}(X)$ making them sound as if they should be understood as partial (and therefore partial computable!) functions on $X$. However, it seems such functions $f$ are not always continuous on $X$ or even on $A$ when $A$ is given the restricted topology of $X$. Instead it seems that $f$ is only sure to be continuous on the topology given by the representation of $A$, which can differ greatly from the topology on $X$.
My questions:
- Does my understanding seem correct?
- Are there any good resources on this subject?
Here are a few examples of the phenomena I am talking about.
-
Given a "complemented set" $A=(A_0,A_1)$ where $A_0,A_1 \subseteq X$ are disjoint, e.g. the pair $[0,1/2], (1/2,1]$, then Bishop and Bridges (p 73) construct the characteristic function as
$$\chi_A(x) =
\begin{cases}
1 & x \in A_0, \\
0 & x \in A_1. \\
\end{cases}$$
with domain $A_0 \cup A_1$. This function is continuous (even computable) on the disjoint sum of $A_0$ and $A_1$, but not necessarily on $A_0 \cup A_1$ (using the topology of $X$). Since it is not constructively provable that, say, $[0,1/2] \cup (1/2,1] = [0,1]$, it is therefore not constructively provable that $\chi_{[0,1/2]}$ is a discontinuous function on $[0,1]$. -
Given a sequence of functions $\phi_n : X \rightarrow \mathbb{R}$, Bishop and Bridges (p 225), define the function $\phi = \sum_n \phi_n$ with domain
$$\{x \in X : \sum_n |\phi_n(x)|\ \text{ converges}\}.$$
(The context is measure theory.) It seems that for this definition to make sense constructively, the domain would have to be understood via its $\Pi^0_3$ definition and is therefore represented as a countable intersection of countable unions of closed sets. Then for any $x$ in the set, from each representation of $x$ one can uniformly compute $\sum_n |\phi_n(x)|$ and therefore compute $\sum_n \phi_n(x)$.
Best Answer
Bishop's mathematics is compatible with classical mathematics. For example, if we look at set theory in Bishop's framework, each model V of ZFC is a model of Bishop's system, and if we look at second-order arithmetic in Bishop's system then the standard model of second-order arithmetic is a model of Bishop's system.
So it is not true that, in Bishop's system, every function must be continuous.
On the other hand, Bishop's system is compatible with the nonclassical axiom that every function is continuous. So you cannot prove the existence of a discontinuous function.
Bishop's system is, in this sense, neutral between constructive and classical mathematics. It is weak enough, among constructive systems, to admit classical models, but it is also weak enough, among classical systems, to admit nonclassical models.
One nice (and short) reference on Bishop's system is Varieties of Constructive Mathematics by Bridges and Richman. The authors contrast Bishop's system with other constructive systems.