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.

Metatheory. The weak continuity principle WC-N is not a description of choice sequences but an axiom about them, and it is classically false: it refutes the limited principle of omniscience and hence excluded middle, so intuitionistic analysis and classical analysis are inconsistent with each other rather than nested. From WC-N together with the fan theorem — the contrapositive of König's lemma for finitely branching spreads, and a consequence of bar induction — Brouwer derived that every total function on [0,1] is uniformly continuous. Kleene and Vesley, The Foundations of Intuitionistic Mathematics (1965), gave the formal system FIM and used function realizability to show it consistent, which is what makes continuity a coherent axiom rather than an error. Kreisel and Troelstra (1970) axiomatized lawless sequences by open data, density, and decidable equality, and proved an elimination theorem: every formula of LS is equivalent to one without quantifiers over lawless sequences, so LS is conservative over its lawlike part. Sheaf models over spreads, due to van der Hoeven and Moerdijk, give a classical semantics for the whole apparatus.

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

Limitations. The continuity principles are not merely non-classical but anti-classical: adding excluded middle to WC-N is inconsistent, so nothing proved here transfers to a classical setting, and unlike Bishop's neutral core this theory cannot be read classically at all. Lawless sequences are a fragile object. They cannot be paired — a pair of lawless sequences is not lawless — so the theory of LS is not closed under the constructions one wants, and the axioms have to be restricted to formulas without lawless parameters in the wrong positions. Extensional equality of choice sequences is undecidable — LS makes identity of lawless sequences decidable only because they are given by name — and there is no canonical notion: lawless, lawlike, and Troelstra's sequences-with-restrictions validate different continuity principles, so "choice sequence" names a family of incompatible axiomatizations. The elimination theorem cuts both ways: since LS proves no new lawlike theorem, lawless sequences add no arithmetical content. And bar induction, which the fan theorem and hence Brouwer's continuity theorem lean on, is assumed rather than justified — Brouwer's own argument for the bar theorem has never been accepted as a proof.

© 2026 Lingenic LLC