I have the distinct memory of having often heard and read that intuitionism was inter alia geared to avoid Cantor's uncountable sets, and it may be that this was Brouwer's plan. But are there accounts which demonstrate that early intuitionism (i.e. before the advent of modern intuitionistic set theories, which either do not have the power set or do accept Cantor's conclusion) had some intuitionistically reasonable way of evading Cantor's uncountable sets?
-
2$\begingroup$ I think he did count inevitability $\endgroup$– Will JagyCommented Jan 12, 2015 at 0:16
-
$\begingroup$ I guess the reason is that the intuitionist only recognizes sets that can be constructed out of the basal intuition, "and this can only be done by combining a finite number of times the two operations: 'to create a finite ordinal number' and 'to create the infinite ordinal number $\omega$'. Consequently the intuitionist recognizes only the existence of denumerable sets." (Intuitionism and Formalism, p.58) $\endgroup$– Bruno BentzenCommented Apr 21, 2016 at 11:23
1 Answer
You are probably referring to Brouwer's considerations of the Creative Subject, which can be formulated mathematically as Kripke's schema. It implies that all subsets of $\mathbb{N}$ are countable, for example. I am having trouble finding good references, maybe these two will get you started:
Göran Sundholm: "Constructive recursive functions, Church's thesis and Kripke's schema"
"The Use of Kripke's Schema as a Reduction Principle" D. Van Dalen The Journal of Symbolic Logic Vol. 42, No. 2 (Jun., 1977), pp. 238-240
I know little about the history of Brouwer's mathematics, but I would be very much surprised to hear that he set out to demolish Cantor's set theory. I thought his criticism was pointed at Hilbert's purely existential proofs, not at Cantor. I also never heard that uncountability was considered a problem, it was rather methods of proof.
From a purely mathematical point of view (i.e., ignoring history) it makes no sense to "avoid uncountability" because the usual diagonalization proofs of uncountability of Baire space $\mathbb{N}^{\mathbb{N}}$, Cantor space $\{0,1\}^{\mathbb{N}}$ and powerset $\mathcal{P}(\mathbb{N})$ are intuitionistically valid, and Brouwer would have of course known that. It would be hard for Brouwer to avoid these spaces, especially the Baire and the Cantor spaces, as these correspond to the totalities of all paths through a spread and through a fan, respectively. At best some limited form of "everything is countable" is tenable, for instance "every subset of $\mathbb{N}$ is countable" – which is of course valid classically but not in pure intuitionistic logic.
-
$\begingroup$ How do we e.g. account for the text on the top of page 26 here? May it be that Brouwer rejected such totalities as $\mathbb{N}^\mathbb{N}$? books.google.com.br/… $\endgroup$ Commented Jan 12, 2015 at 0:29
-
$\begingroup$ (I have encountered constructivists of the Martin Löf type who have this conviction that there is no set of the real numbers.) $\endgroup$ Commented Jan 12, 2015 at 0:32
-
1$\begingroup$ "Rejecting higher infinities" can mean something subtler than "I don't believe there are any infinities past $\aleph_0$", especially since intuitionistically infinities cannot be shown linearly ordered and so "past $\aleph_0$" does not mean "everything but countable". There can be subsets of countable sets that are not countable. $\endgroup$ Commented Jan 12, 2015 at 0:44
-
1$\begingroup$ (I am not sure about making public links to books that look like they are copyrighted.) As I said, I am not an expert on the history. It seems to me you can answer your own question better than I can. $\endgroup$ Commented Jan 12, 2015 at 0:54
-
3$\begingroup$ My impression is that Brouwer would probably not have accepted exponentiation as we view it in, for example, topoi. His reals and his sequences of natural numbers would have been some sort of choice sequences. And "some sort" here does not refer only to my ignorance; I think Brouwer changed his mind on what is allowed in a choice sequence. Free choice sequences are pretty clear, but general choice sequences allow one to choose restrictions on future choices. Can one choose restrictions on future restrictions? I think Brouwer vacillated on that. $\endgroup$ Commented Jan 12, 2015 at 0:58