Choice sequence
In intuitionistic mathematics, a choice sequence is a constructive formulation of a sequence. Since the Intuitionistic school of mathematics, as formulated by L. E. J. Brouwer, rejects the idea of a completed infinity, in order to use a sequence (which is, in classical mathematics, an infinite object), we must have a formulation of a finite, constructible object that can serve the same purpose as a sequence. Thus, Brouwer formulated the choice sequence, which is given as a construction, rather than an abstract, infinite object. Lawlike and lawless sequences A distinction is made between lawless and lawlike sequences. A lawlike sequence is one that can be described completely—it is a completed construction, that can be fully described. For example, the natural numbers can be thought of as a lawlike sequence: the sequence can be fully constructively described by the unique element 0 and a successor function. Given this formulation, we know that the th element in the sequence of natural numbers will be the number . Similarly, a function mapping from the natural numbers into the natural numbers effectively determines the value for any argument it takes, and thus describes a lawlike sequence. A lawless (also, free) sequence, on the other