Choice Sequence

Definition

A choice sequence is an infinite sequence of elements $(a_0,a_1,a_2,\dots )$ from some set $A$, where each element $a_n$ is freely chosen without any predetermined law or algorithm. Choice sequences are fundamental objects in Brouwer’s intuitionistic mathematics and constructive analysis.

Formally, a choice sequence $\alpha$ is a function $\alpha :\mathbb{N}\to A$ that is constructed step by step, where at each stage $n$ the value $\alpha (n)$ is chosen freely by a creating subject, independent of any mathematical law. Common choices for $A$ include natural numbers $\mathbb{N}$, binary choices $2:=\{0,1\}$, or any finite or infinite set.

Types of Choice Sequences

Lawless sequences: Sequences where no restriction is placed on the choices made. Each term is completely free and independent of previous choices. Lawlike sequences: Sequences that are eventually determined by some computable law, though the law itself may not be known initially. Restricted choice sequences: Sequences where certain constraints or patterns must be satisfied, but within these constraints the choices remain free.

Properties

Choice sequences satisfy the continuity principle: any function defined on choice sequences can depend only on finite initial segments. If $f(\alpha )=f(\beta )$ for choice sequences $\alpha$ and $\beta$, then there exists $n$ such that $\alpha (k)=\beta (k)$ for all $k<n$.

The fan theorem applies to choice sequences: every infinite sequence of choices through a finitely branching tree must pass through some node infinitely often.

Constructive Analysis

In constructive real analysis, choice sequences over various types are used to represent real numbers as Cauchy sequences or Dedekind cuts. A real number $r$ may correspond to a choice sequence $\alpha :\mathbb{N}\to \mathbb{Q}$ where $\alpha (n)$ encodes increasingly precise rational approximations to $r$, or to binary choice sequences representing the digits of its binary expansion.

The creating subject plays a crucial role, as choice sequences model the temporal process of mathematical construction where each choice is made at a specific moment in time.

Relationship to Classical Mathematics

Choice sequences provide counterexamples to classical principles in intuitionistic mathematics:

• The law of excluded middle fails for properties of choice sequences
• The axiom of choice takes on a constructive meaning through choice sequences
• Classical theorems about real numbers may fail when interpreted via choice sequences

Applications

• Modeling free will and indeterminacy in mathematical foundations
• Constructive proofs in real analysis and topology
• Formalization of Brouwer’s intuitionistic program
• Study of continuity and computability in constructive mathematics

Related Concepts

• Brower’s Program
• Intuinistic First-Order Logic
• Constructive Mathematics
• Continuity Principle