Choice Sequence - Axiomatization

Axiomatization

There are two axioms in particular that we expect to hold of choice sequences as described above. Let denote the relation "the sequence begins with the initial sequence " for choice sequence and finite segment (more specifically, will probably be an integer encoding a finite initial sequence).

We expect the following, called the axiom of open data, to hold of all lawless sequences:

where is a one-place predicate. The intuitive justification for this axiom is as follows: in intuionistic mathematics, verification that holds of the sequence is given as a procedure; at any point of execution of this procedure, we will have examined only a finite initial segment of the sequence. Intuitively, then, this axiom states that since, at any point of verifying that holds of, we will only have verified that holds for a finite initial sequence of ; thus, it must be the case that also holds for any lawless sequence sharing this initial sequence. This is so because, at any point in the procedure of verifying, for any such sharing the initial prefix of encoded by that we have already examined, if we run the identical procedure on, 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, given by:

states that, for any finite prefix (encoded by), there is some sequence 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.