10
$\begingroup$

I've seen several times people mentioning that the notion of an algorithm / a computation is taken as a primitive notion in L. E. J. Brouwer's intuitionism. For instance, in Varieties of Constructive Mathematics (1987, p.1), Bridges and Richman write that:

In Bishop's constructive mathematics (BISH), and in Brouwer's intuitionism (INT), the notion of an algorithm, or finite routine, is taken as primitive. Russian constructivism (BUSS), on the other hand, operates within a fixed programming language, and an algorithm is a sequence of symbols in that language.

To the best of my knowledge, Brouwer's intuitionistic mathematics is fundamentally a languageless creation of the mind which is erected on the two acts of intuitionism: (i) the first act gives us the construction that corresponds to the natural numbers; (ii) the second act provides us with the notion of free choice sequents. To put it other way, there is no explicit mention of algorithms.

On the other hand, it seems that this common (?mis?)conception, namely, that the notion of an algorithm is a primitive notion in Brouwer's intuitionisim, came with the influence of the BHK interpretation, where the notion of a proof (which, by the Curry-Horward correspondence, corresponds to the notion of a program) plays the central role in this informal interpretation of intuitionistic logic. However, as I said, this is intuitionistic logic and not Brouwer's intuitionisim - and I do think it helps to keep both apart.

Can we justify this claim that the notion of an algorithm is a primitive notion in Brouwer's intuitionism?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Wouldn't this question stand a better change of getting a good answer at hsm.stackexchange.com? $\endgroup$
    – Andrej Bauer
    Commented Nov 29, 2016 at 7:23

2 Answers 2

Reset to default
4
$\begingroup$

Since the work of Church and Turing (say around 1936), the notion of algorithm is definitely not considered primitive in intuitionism. But Brouwer started intuitionistic mathematics more than 2 decades before (1907, 1912), and in the absence of a commonly accepted notion of algorithm, he formulated his idea (somewhat) like this:

A sequence of natural numbers arises in the course of time, like a walk through the (infinite) tree $\mathbb{N}^*$ of finite sequences, choosing at each 'node' a next continuation.

The result is an infinite branch, or an 'arrow' as Brouwer called it. At any node (also right at the start) one may specify a definite finite law which completely governs all next choices (so that there really is no choice left at all). If one does so right at the start, the arrow is called a 'sharp arrow' or a 'lawlike sequence'.

Since the 1930's definition of recursion, it has become standard to identify 'sharp arrow' and 'lawlike sequence' with recursive sequences, I believe.

Improve this answer
$\endgroup$
4
$\begingroup$

As far as I know, Brouwer's intuitionism involves a primitive notion of "construction". This might be viewed as "a finite routine" --- finite because it should be possible to finish a construction. I think of these constructions or routines as somewhat nebulous things, not nearly as precise as what are usually called algorithms. So I wouldn't use the word "algorithm" for these things. But perhaps what Bridges and Richman have in mind is that, even though they choose to call these things algorithms, they need not be algorithms in the usual sense; the contrast with "sequence of symbols in [a fixed programming] language" seems to indicate something like that.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .