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 completelyit 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. 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) such that:

• ; and

• .

Note that the first point above is slightly misleading, as we may specify, for example, that the values in a sequence be drawn exclusively from the set of natural numbers—we can specify, a priori, the range of the sequence.

The canonical example of a lawless sequence is the series of rolls of a die. This specification comprises the procedure for generating the lawless sequence in question. At no point, then, is any particular future value of the sequence known.

Axiomatization

There are two axioms will probably be an integer encoding a finite initial sequence).

We expect the following, called the axiom of open data is a one-place predicate is given as a procedure, we will get the same result. The axiom can be generalized for any predicate taking an arbitrary number of arguments.

Another axiom is required for lawless sequences. The axiom of density beginning with that prefix. We require this axiom so as not to have any "holes" in the set of choice sequences. This axiom is the reason we require that arbitrarily long finite initial sequences of lawless choice sequences can be specified in advance; without this requirement, the axiom of density is not necessarily guaranteed.

See also

Notes

References