Iterated Definability, Lawless Sequences, and Brouwer’s Continuum
The research on which this article is based was motivated by the wish to find a model of Kreisel’s lawless sequence axioms in which the lawlike and lawless sequences form disjoint, inhabited, well-defined classes within Brouwer’s continuum. The original results, reported as they developed in four papers over a period of ten years from 1986 to 1996, have so far lacked a reader-friendly presentation. Since the question of absolute definability is related to the subject of these Bristol Workshops, I offer here a straightforward exposition of the final model and formal system with axioms for numbers, lawlike sequences, and arbitrary choice sequences. A choice sequence is defined to be lawless if it satisfies an extensional (un)predictability condition from which extensional versions of Kreisel’s axioms of open data and strong continuous choice follow. The law of excluded middle can be assumed for properties of lawlike and independent lawless sequences only, while Brouwer’s continuity principle applies to properties of all choice sequences. Iterating definability, quantifying over numbers and over lawlike and independent lawless sequences, yields a classical model of the lawlike sequences with a natural wellordering. Under the (classically consistent and intuitionistically plausible) assumption that the closure ordinal of the iteration is countable, a realizability interpretation establishes the consistency of a common extension FIRM(≺) of classical analysis R and Kleene’s intuitionistic analysis FIM. Lawlike sequences behave classically, while the lawless sequences form a disjoint, Baire comeager collection of choice sequences, of classical measure zero. Thus Brouwer’s continuum can be understood as a relatively chaotic expansion of a completely determined, well-ordered classical continuum.