Choice Sequences

Origin. Brouwer (1920s). Intuitionist foundations. Sequences created by free choice. Not predetermined. Foundation for Brouwerian analysis.

Models. Sequences α: ℕ → ℕ created step by step. Lawless: no determining law. Lawlike: recursive or definable. Continuity principles. Spreads and bars.

Formalism.

Choice sequence: α: ℕ → ℕ constructed over time. α(n) chosen freely at stage n. Not determined in advance.

Lawless sequences: No constraint on future choices. Only finite initial segment known. Extensional identity: α = β iff ∀n. α(n) = β(n).

Continuity principle (weak): If ∀α∃n.A(α,n), then: ∀α∃m,n. (∀β. ᾱm = β̄m → A(β,n)) Result depends only on finite prefix.

Bar induction: If every α has a barred node (initial segment in B): And property P is inductive and holds at B: Then P holds at root.

Spread: Tree of finite sequences (admissible). Choice sequences: infinite paths through spread.

Fan theorem: In finitely branching spread (fan): If every path hits bar, bar is finite. Uniform bound exists.

Brouwer's thesis: All functions ℕ^ℕ → ℕ continuous. Contradicts classical: characteristic function of diagonal.

Symbols.

Symbol	Unicode	Name	Meaning
α, β	—	Sequences	Choice sequences
ᾱn	—	Prefix	Initial segment
B	—	Bar	Barring set
∀α	—	Forall	Over sequences

Metatheory. Inconsistent with classical. Continuity forced. Fan theorem provable. Spreads model real numbers.

Applies to. Intuitionistic analysis. Real number theory. Constructive foundations. Brouwerian mathematics.

Limitations. Incompatible with classical math. Non-standard framework. Limited acceptance. Technical complexity.