choice, axiom of See LÖWENHEIM – SKOLEM THEO -. REM , SET THEORY. choice sequence, a variety of infinite sequence introduced by L. E. J. Brouwer to express the non-classical properties of the continuum (the set of real numbers) within intuitionism. A choice sequence is determined by a finite initial segment together with a ‘rule’ for continuing the sequence. The rule, however, may allow some freedom in choosing each subsequent element. Thus the sequence might start with the rational numbers 0 and then ½, and the rule might require the n ! 1st element to be some rational number within (½)n of the nth choice, without any further restriction. The sequence of rationals thus generated must converge to a real number, r. But r’s definition leaves open its exact location in the continuum. Speaking intuitionistically, r violates the classical law of trichotomy: given any pair of real numbers (e.g., r and ½), the first is either less than, equal to, or greater than the second. From the 1940s Brouwer got this non-classical effect without appealing to the apparently nonmathematical notion of free choice. Instead he used sequences generated by the activity of an idealized mathematician (the creating subject), together with propositions that he took to be undecided. Given such a proposition, P – e.g. Fermat’s last theorem (that for n ( 2 there is no general method of finding triplets of numbers with the property that the sum of each of the first two raised to the nth power is equal to the result of raising the third to the nth power) or Goldbach’s conjecture (that every even number is the sum of two prime numbers) – we can modify the definition of r: The n ! 1st element is ½ if at the nth stage of research P remains undecided. That element and all its successors are ½ ! (½)n if by that stage P is proved; they are ½ † (½)n if P is refuted. Since he held that there is an endless supply of such propositions, Brouwer believed that we can always use this method to refute classical laws. In the early 1960s Stephen Kleene and Richard Vesley reproduced some main parts of Brouwer’s theory of the continuum in a formal system based on Kleene’s earlier recursion-theoretic interpretation of intuitionism and of choice sequences. At about the same time – but in a different and occasionally incompatible vein – Saul Kripke formally captured the power of Brouwer’s counterexamples without recourse to recursive functions and without invoking either the creating subject or the notion of free choice. Subsequently Georg Kreisel, A. N. Troelstra, Dirk Van Dalen, and others produced formal systems that analyze Brouwer’s basic assumptions about open-futured objects like choice sequences. See also MATHEMATICAL INTUITIONISM , PHILOSOPHY OF MATHEMATIC. C.J.P.