Spreads are defined via a spread function which performs a "check" on finite sequences. The notion of a spread and its spread function are interchangeable in the literature; both are treated as one and the same. If all the finite initial parts of an infinite sequencesatisfy a spread function's "check", then we can say that the infinite sequence is admissible to the spread. Graph theoretically, one may think of a spread as a rooted, directed tree with numerical vertexlabels.
Formal definition
This article uses to denote the beginning of a sequence and to denote the end of a sequence. A spread function is a function that maps finite sequences to either 0 or 1 , and satisfies the following properties:
Given any finite sequence such that then there must exist some such that
Given an infinite sequence, we say that the finite sequence is an initial segment of iff and and... and. Thus we say that an infinite sequence is admissible to a spread defined by spread function iff every initial segment of is admissible to.
Fans
A special type of spread that is of particular interest in the Intuitionistic foundations of mathematics is a finitary spread; also known as a fan. The main use of fans is in the fan theorem, a result used in the derivation of the uniform continuity theorem. Informally; a spread function defines a fan iff given a finite sequence admissible to the spread, there are only finitely many possible values that we can add to the end of this sequence such that our new extended finite sequence is admissible to the spread. Alternatively, we can say that there is an upper bound on the value for each element of any sequence admissible to the spread. Formally; a spread function defines a fan iff given any sequence admissible to the spread, then there exists some such that, given any then . Some examples of fans are:
Given any finite sequence, we have. In other words, this is the spread containing all possible sequences. This spread is often used to represent the collection of all choice sequences.
The binary spread
Given any finite sequence, if all of our elements are 0 or 1 then, otherwise. In other words, this is the spread containing all binary sequences.
Dressed Spreads
A key use of spreads in the foundations of intuitionisitic analysis is the use of spreads of natural numbers to represent reals. This is achieved via the concept of a dressed spread, which we outline below. A dressed spread is a pair of objects; a spread, and some function acting on finite sequences. An example of a dressed spread is the spread of integers such that iff, and the function .
Author notes
Dressed spreads – how we get from spreads to the reals.