Are all functions in Bishop's constructive mathematics continuous?

Question

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:

1. Does my understanding seem correct?
2. Are there any good resources on this subject?

---

Here are a few examples of the phenomena I am talking about.

1. 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]$.

2. 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)$.

Answer 1

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.

Answer 2

With example 1: It is not constructively provable that $\chi_{[0,1/2]}$ is a function on $[0,1]$. A reasonable constructive theorem is that $\chi_{[0,1/2]}$ can not be extended to a continuous function on that interval.

With example 2: An element of the domain can be thought of as an element of $X$ together with a modulus of convergence for $\Sigma |\phi_n(x)|$. For any element so presented, one can compute the sum $\Sigma \phi_n(x)$.

I offer example 3: For every real $r$, there is an integer $n$ with $n>r$.

This is an easy constructive theorem, proved by taking an integer at least 2 greater than the first rational in the Cauchy sequence which defines $r$. However, it does not lead to a function $f:R\rightarrow N$, which would have to be discontinuous. It leads instead to a non-extensional operation taking elements of $R$ to elements of $N$.

I find all the oddities around this question to be present, and fairly clear, in this example.

Answer 3

Discontinuous functions are perfectly acceptable in constructive mathematics.

But BISH (the way of doing constructive math as put forward by Errett Bishop) is actually deficient in its definition of 'continuous function'. (As pointed out in my PhD thesis modern intuitionistic topology, and the follow-up article On the foundations of constructive mathematics --- especially in relation to the theory of continuous functions).

Topology was not Bishop's strongest suit when he started BISH (of which I am nonetheless still an admirer, but it really needs to be replaced by a way of defining spaces and functions which is far more precise and foundationally balanced).

Brouwer on the other hand was a master topologist, and in intuitionistic mathematics you will not find any such deficiencies.

If we use Brouwer's methods and a set-theoretic definition of 'function' and 'topology', then the following things hold in BISH on a meta-level:

• Functions which are total on a Polish space are always continuous
• Partial functions on a Polish space can be discontinuous (for a 'classical' example see below)
• Functions which are total on a 'natural space' are always continuous w.r.t. the (natural) apartness topology, but other topologies are possible. For Polish spaces the metric and the apartness topologies coincide (see my book Natural Topology on arXiv and the article Exact computation over topological spaces).

A constructive example of a discontinuous partial function is the following:

$f(x):= 0\ \mbox{if}\ x\in\mathbb{Q}\\ f(x):= 1\ \mbox{if}\ x\,\#\,\mathbb{Q}$

which is defined on $\mathbb{Q}\cup\mathbb{I}\subsetneq\mathbb{R}$ where $\mathbb{I}$ is the set of positively irrational reals.