Choice sequence

In intuitionistic mathematics, a choice sequence is a constructive formulation of a sequence. Since the Intuitionistic school of mathematics, as formulated by L. E. J. Brouwer, rejects the idea of a completed infinity, in order to use a sequence (which is, in classical mathematics, an infinite object), we must have a formulation of a finite, constructible object which can serve the same purpose as a sequence. Thus, Brouwer formulated the choice sequence, which are given as constructions, rather than as abstract, infinite objects.

Lawlike and Lawless Sequences

A distinction is made between lawless and lawlike sequences. A lawlike sequence is one that can be described completely -- it is a completed construction, that can be fully described. For example, the natural numbers $\mathbb {N}$ can be thought of as a lawlike sequence: the sequence can be fully constructively described by the unique element 0 and a successor function. Given this formulation, we know that the $i$th element in the sequence of natural numbers will be the number $i-1$. Similarly, a function $f:\mathbb {N} \mapsto \mathbb {N}$ mapping from the natural numbers into the natural numbers effectively determines the value for any argument it takes, and thus describes a lawlike sequence.

A lawless sequence, on the other hand, is one that is not predetermined. It is to be thought of as a procedure for generating values for the arguments 0, 1, .... That is, a lawless sequence $\alpha _{n}$ is a procedure for generating $\alpha _{0}$, $\alpha _{1}$, ... (the elements of the sequence $\alpha$) such that:

• At any given moment of construction of the sequence $\alpha$, only an initial segment of the sequence is known, and no restrictions are placed on the future values of $\alpha$; and
• One may specify, in advance, an initial segment $\langle \alpha _{0},\alpha _{1},\ldots ,\alpha _{k}\rangle$ of $\alpha$.

Note that the first point above is slightly misleading, as we may specify, for example, that the values in a sequence be drawn exclusively from the set of natural numbers -- we can specify, a priori, the range of the sequence.

The canonical example of a lawless sequence is the series of rolls of a die. We specify which die to use and, optionally, specify in advance the values of the first k rolls (for $k\in \mathbb {N}$). Further, we restrict the values of the sequence to be in the set $\{1,2,3,4,5,6\}$. This specification comprises the procedure for generating the lawless sequence in question. At no point, then, is any particular future value of the sequence known.

Reference

• Jacquette, Dale, A Companion to Philosophical Logic, p. 517.

• Troelstra, A.S., Analysing Choice Sequences, Journal of Philosophical Logic, 12:2 (1983:May) p. 197.

• Troelstra, A. S.; D. van Dalen. Constructivism in Mathematics: An Introduction. North HOlland, 1988.