In intuitionistic mathematics, a spread is a particular kind of species of infinite sequences defined via finite decidable properties.
Here a species is a collection, a notion similar to a classical set in that a species is determined by its members.
The notion of spread was first proposed by L. E. J. Brouwer (1918B), and was used to define the continuum.
As his ideas were developed, the use of spreads became common in intuitionistic mathematics, especially when dealing with choice sequences and intuitionistic analysis (see Dummett 77, Troelstra 77).
In the latter, real numbers are represented by the dressed spreads of natural numbers or integers.
The more restricted so called fans are of particular interest in the intuitionistic foundations of mathematics.
There, their main use is in the discussion of the fan theorem (which is about bars, not discussed here), itself a result used in the derivation of the uniform continuity theorem.
In modern terminology, a spread is an inhabited closed set of sequences.
Spreads are defined via a spread function, which performs a (decidable) "check" on finite sequences.
If all the finite initial parts of an infinite sequence satisfy a spread function's "check", then we say that the infinite sequence is admissible to the spread.
Graph theoretically, one may think of a spread in terms of a rooted, directed tree with numerical vertex labels.
In graph terms, it is finitely branching.
Finally, a dressed spread is a spread together some function acting on finite sequences.
" to denote the beginning resp.
The sequence with no elements, the so called empty sequence, is denoted by
is a function on finite sequences that satisfies the following properties: Given a finite sequence, if
returns 0, the sequence is admissible to the spread given through
The empty sequence is admissible and so part of every spread.
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.
In that way, the spread function acts as a characteristic function accepting many long finite sequences.
For example, for a predicate characterizing a law-like, unending sequence of numbers, one may validate that it is admissible with respect to some spread function.
Informally, a spread function
defines a fan if, 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: So 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.
Simple examples of spreads include What follows are two spreads commonly used in the literature.
In other words, this is the spread containing all possible sequences.
This spread is often used to represent the collection of all choice sequences.
In other words, this is the spread containing all binary sequences.
This represents the real numbers.