Individual choice sequences -- History, development and use

TL;DR

This paper analyzes Brouwer’s use of individual choice sequences, showing how the continuum consists of lawlike and incompletely determined sequences and how the Continuity Principle (CP) anchors intuitionistic analysis. It reconstructs Brouwer’s postwar method via the Theory of Individual Choice Sequences (TICS), introducing Box_n modalities, drifts, fleeing properties, and various checking numbers to capture the dependence of sequence values on untested propositions. The author argues that TICS provides a clearer, more faithful account of Brouwer’s CS-arguments than the traditional Theory of Choice Sequences (TCS) and Kripke’s Schema, and uses this framework to critique standard results such as KS and MP. The work further distinguishes reduced versus full continua, emphasizes undecidability rather than decidability in Brouwer’s continuum, and advocates reorienting intuitionistic foundations toward future-influenced constructions with substantial philosophical and mathematical implications.

Abstract

We follow the history and development of Brouwer's use of individual choice sequences up to the discovery of a method to apply them successfully in 1927. With the principles we derive from this first use we analyze in detail Brouwer's work from that time onward. Our reconstruction uses only very basic principles. It aligns exactly with Brouwer's work after 1927 and, moreover, it gives a clear explanation of the proofs of his results and the terms he uses.