Spread (intuitionism)

In intuitionistic mathematics, a species is a collection (similar to a classical set in that a species is determined by its members). A spread is a particular kind of species of infinite sequences defined via finite decidable properties. In modern terminology, a spread is an inhabited closed set of sequences. The notion of spread was first proposed by L. E. J. Brouwer (1918B), and was used to define the real numbers (also called the continuum). As Brouwer's ideas were developed, the use of spreads became common in intuitionistic mathematics, especially when dealing with choice sequences and the foundations of intuitionistic analysis (Dumett 77, Troelstra 77).

Simple examples of spreads are:

• the set of sequences of even numbers;
• the set of sequences of the integers 1–6;
• the set of sequences of valid terminal commands.

Spreads are defined via a spread function which performs a (decidable) "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 sequence satisfy 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 vertex labels.

Formal definition

This article uses ${\displaystyle \langle }$ to denote the beginning of a sequence and ${\displaystyle \rangle }$ to denote the end of a sequence.

A spread function ${\displaystyle s}$ is a function that maps finite sequences to either 0 [i.e. the finite sequence is admissible to the spread] or 1 [i.e. the finite sequence is inadmissible to the spread], and satisfies the following properties:

• Given any finite sequence ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ either ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$ or ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1}$ (the property ${\displaystyle s}$ "tests" for must be decidable).

• Given the empty sequence (the sequence with no elements represented by ${\displaystyle \langle \rangle }$), ${\displaystyle s(\langle \rangle )=0}$ (the empty sequence is in every spread).

• Given any finite sequence ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ such that ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$ then there must exist some ${\displaystyle k}$ such that ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i},k\rangle )=0}$ (every finite sequence in the spread can be extended to another finite sequence in the spread by adding an extra element to the end of the sequence)

Given an infinite sequence ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$, we say that the finite sequence ${\displaystyle \langle y_{1},y_{2},\ldots ,y_{i}\rangle }$ is an initial segment of ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ iff ${\displaystyle x_{1}=y_{1}}$ and ${\displaystyle x_{2}=y_{2}}$ and ... and ${\displaystyle x_{i}=y_{i}}$.

Thus we say that an infinite sequence ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ is admissible to a spread defined by spread function ${\displaystyle s}$ iff every initial segment of ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ is admissible to ${\displaystyle s}$.

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 ${\displaystyle s}$ 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 ${\displaystyle s}$ defines a fan iff given any sequence admissible to the spread ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$, then there exists some ${\displaystyle k}$ such that, given any ${\displaystyle j>k}$ then ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i},j\rangle )=1}$ (i.e. given a sequence admissible to the fan, we have only finitely many possible extensions that are also admissible to the fan, and we know the maximal element we may append to our admissible sequence such that the extension remains admissible).

Some examples of fans are:

• the set of sequences of legal chess moves;
• the set of infinite binary sequences;
• the set of sequences of letters.

Commonly used spreads/fans

This section provides the definition of 2 spreads commonly used in the literature.

The universal spread (the continuum)

Given any finite sequence ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$, we have ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$. 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 ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$, if all of our elements (${\displaystyle x_{1},x_{2},\ldots ,x_{i}}$) are 0 or 1 then ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$, otherwise ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1}$. 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 (or integers) 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 ${\displaystyle s}$, and some function ${\displaystyle f}$ acting on finite sequences.

An example of a dressed spread is the spread of integers such that ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$ iff ${\displaystyle \forall y_{0<y\leq i}[x_{i}=2x_{y-1}+/-1\ or\ 0]}$, and the function ${\displaystyle f(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=x_{i}*2^{2-i}}$ (the dressed spread representing the real numbers).

References

• L.E.J. Brouwer Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre, KNAW Verhandelingen, 5: 1–43 (1918A)
• Michael Dummett Elements of Intuitionism, Oxford University Press (1977)
• A. S. Troelstra Choice Sequences: A Chapter of Intuitionistic Mathematics, Clarendon Press (1977)

Author notes

Dressed spreads – how we get from spreads to the reals.