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.

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 ${\displaystyle \mathbb {N} }$ 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 ${\displaystyle i}$th element in the sequence of natural numbers will be the number ${\displaystyle i-1}$. Similarly, a function ${\displaystyle f:\mathbb {N} \mapsto \mathbb {N} }$ mapping from the natural numbers into the natural numbers effectively determines the value for any argument it takes, and thus describes a lawlike sequence.

...
Wikipedia