8
$\begingroup$

The partial μ-recursive functions which may or may not be provably total seem to have some direct relation to the initial motivations for intuitionistic mathematics. (Following Kronecker, one motivation might have been that mathematical statements should be reducible to statements about the natural numbers, or computable functions of the natural numbers.)

When Brouwer and Heyting did their initial work, the understanding of those partial functions was still evolving significantly. However, this excuse no longer applies to the time when Errett Bishop published his Foundations of constructive analysis. However, extramathematical observations like that "all functions in Bishop's constructive mathematics are continuous" indicate that function always meant provably total function, because otherwise a formulation like "no discontinuous function can be proved to be total in Bishop's constructive mathematics" would seem to be less misleading and better capture what is really going on.

So did Bishop, Heyting or Brouwer (or any other prominent "early" proponent of intuitionism) explicitly discussed this relationship, and clearly indicated to role (and treatment) of such partial functions in intuitionistic mathematics?

$\endgroup$
3
  • $\begingroup$ I don't follow how the question whether partial functions are considered would have any impact at all on whether externally all functions are continuous. $\endgroup$
    – Arno
    Nov 24, 2015 at 12:40
  • $\begingroup$ @Arno If the word "function" is used synonymously with "provably total function", then externally all functions are continuous. One way to achieve this (in intuitionistic mathematics) is to define the domain of the function suitably, which then translate into the fact that the domain of the function is not provably equal to the entire interval $[0,1]$. $\endgroup$ Nov 24, 2015 at 13:34
  • 2
    $\begingroup$ I wonder whether everyone is thinking the same way. Do we think that the function $f(0) = 0$ and $f(x) = 1$ for $x \not = 0$ is a partial function defined on the set $\{x \in \mathbb{R} : x = 0 \lor x \not = 0\}$? (Of course that set is not decidable and may not be all of $\mathbb{R}$, from a constructive viewpoint.) $\endgroup$ Nov 24, 2015 at 16:24

2 Answers 2

10
$\begingroup$

I don't believe that Bishop explicitly assumed all functions are continuous. I think that "no discontinuous function can be proved to be total in Bishop's constructive mathematics" is actually a very good way of summarizing the situation.

For example, consider how we would state "All functions from $\mathbb{R}$ to $\mathbb{Z}$ are constant" in a Bishop-type framework. A function would be a procedure that takes a representation of a real number and produces an integer, which is extensional in the sense that any two representations of the same real must produce the same integer. Now, if we try to produce a discontinuous function in this sense, we will find that the definition for the function cannot be proved to be total. This is because, if the function was total, then we could prove that for each real there is a finite amount of information about the real which already determines the output (using some version of Weak König's lemma, say), and that would mean that the function would need to be continuous. The key point is that it is not a function that is proved to be total, but rather a definition of a function.

In their Varieties of Constructive Mathematics (1987), which is a good reference on the subject, Bridges and Richman work with an non-formal system BISH which is a subsystem both of classical mathematics and of other constructive frameworks. In particular, every proof in BISH is also a proof in classical mathematics, so BISH cannot prove every function $\mathbb{R}\to\mathbb{N}$ is constant, or anything like that. They explicitly describe BISH as "Bishop's mathematics", and because Bridges had already been a co-author for the later edition of Constructive Mathematics by Bishop and Bridges, I take this as a relatively authoritative opinion on Bishop's viewpoint.

On the subject of partial functions, the system RUSS of Bridges and Richman adds a classically false axiom:

CPF: There is an enumeration $\phi_0$, $\phi_1$, $\ldots$ of all partial functions from $\mathbb{N}$ to $\mathbb{N}$ with countable domains.

They show that BISH + CPF does prove every function from $\mathbb{R}$ to $\mathbb{N}$ is constant, and so BISH + CPF is not compatible with classical models of analysis.

Nowadays, we sometimes identify BISH with formal systems of constructive arithmetic in all finite types (e.g. variants of $\text{HA}^\omega$). These systems are also compatible with classical logic, in the sense that the standard model of arithmetic is also a model of these theories. So these formal representations of BISH also don't prove every function is continuous.

$\endgroup$
9
$\begingroup$

The question of how Brouwer perceived partial functions is very interesting and worthy of investigation. I only have two comments about this:

  • Brouwer and Heyting certainly did consider partial functions such as $1/x$ and discussed its domain in great detail.
  • The Brouwerian Counterexamples are based on the idea of unbounded search, so both Brouwer and Heyting fully understood the idea of $\mu$-recursion.

It would be very interesting to know whether either addressed the idea of a partial function in contrast to the idea of a total function.

However, the main goal of this answer is to correct a false premise of the question: that "every provably total function is continuous" is not a good way to think about Brouwer's continuity theorem. Brouwer proved that "all total functions $[0,1]\to\mathbb{R}$ are uniformly continuous" within his intuitionistic mathematics. There is no mention of "provability" nor any other kind of restriction. Brouwer also showed that classical examples of discontinuous functions, such as the characteristic function of a singleton, are not total by giving specific examples where the functions are not defined. (Note that Brouwer's notion of real numbers allows for a great deal more possibilities than the classical notion.) So there is no room at all in Brouwer's intuitionistic mathematics for total discontinuous functions. This is very different from Bishop's constructive mathematics, which is intended to be compatible with classical mathematics and therefore must allow the possibility of total discontinuous functions.

$\endgroup$
4
  • $\begingroup$ Honestly, I don't know whether Brouwer in 1923 made a distinction between total functions and provably total functions. But from the philosophy of intuitionism, I think that a total function in the intuitionistic sense should be a provably total function. At least it would seem a little odd to suddenly consider "platonic" total function, but reject such "platonic" notions in nearly all other instances. On the other hand, you are probably right that even the "platonic" total functions $[0,1]\to\mathbb R$ will be uniformly continuous, the question is just whether Brouwer has also proved this. $\endgroup$ Nov 24, 2015 at 18:34
  • 2
    $\begingroup$ @ThomasKlimpel: Since Brouwer was against formalism, there is zero chance he meant "provably total". He did mean "total function" in the usual sense, what is dramatically different is what he considered to be a real number. It's fundamentally wrong to believe that Brouwer's intuitionism is about restricting the realm of functions, it is really the concept of real number that got "larger". $\endgroup$ Nov 24, 2015 at 19:33
  • 2
    $\begingroup$ Lovely answer and comments, François! Spot on. $\endgroup$ Nov 24, 2015 at 19:51
  • $\begingroup$ A function becomes {continuous, total} at exactly the moment that the creating subject has determined it to be so. This is separate from the notion of "proof" which really has no place in intuitionistic mathematics—when Heyting said "proof", he did not mean a logical derivation, but rather the act of making an assertion/judgment. $\endgroup$ Nov 24, 2015 at 19:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.