Going Forth
摘要
We discuss specifically intuitionistic ideas, based on Brouwer’s “second act”: choice sequences and species. A particular kind of species, spreads, is used to model the non-denumerable continuum. The Continuity Principle, which essentially states that a total function on a spread depends only on finite initial segments of choice sequences, leads us to the Fan Theorem (a form of compactness) and the Uniform Continuity Theorem. We also discuss the Brouwer-Kripke Schema, which models the Creating Subject and has surprising mathematical consequences. Finally, we compare Brouwer’s approach with the recursive mathematics of Markov and with the pragmatic but watered-down constructivism of Bishop.