In
intuitionistic mathematics, a ''species'' is a collection (similar to a classical
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
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
Luitzen Egbertus Jan Brouwer (; ; 27 February 1881 – 2 December 1966), usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, who worked in topology, set theory, measure theory and compl ...
(1918B), and was used to define the
real numbers
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every real ...
(also called the
continuum
Continuum may refer to:
* Continuum (measurement), theories or models that explain gradual transitions from one condition to another without abrupt changes
Mathematics
* Continuum (set theory), the real line or the corresponding cardinal number ...
). 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
In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.
This contrasts with ''classical analysis'', which (in this context) simply means analysis done according to the (more com ...
(Dummett 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
Director may refer to:
Literature
* ''Director'' (magazine), a British magazine
* ''The Director'' (novel), a 1971 novel by Henry Denker
* ''The Director'' (play), a 2000 play by Nancy Hasty
Music
* Director (band), an Irish rock band
* ''D ...
tree
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondary growth, plants that are ...
with numerical
vertex
Vertex, vertices or vertexes may refer to:
Science and technology Mathematics and computer science
*Vertex (geometry), a point where two or more curves, lines, or edges meet
* Vertex (computer graphics), a data structure that describes the positio ...
labels.
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
.e. the finite sequence is ''admissible'' to the spreador 1
.e. the finite sequence is ''inadmissible'' to the spread and satisfies the following properties:
*Given any finite sequence
either
or
(the property
"tests" for must be decidable).
*Given the empty sequence (the sequence with no elements represented by
),
(the empty sequence is in every spread).
*Given any finite sequence
such that
then there must exist some
such that
(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
, we say that the finite sequence
is an ''initial segment'' of
if and only if
and
and ... and
.
We say that an infinite sequence
is admissible to a spread defined by spread function
if and only if 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 if and only 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
In mathematics, particularly in order theory, an upper bound or majorant of a subset of some preordered set is an element of that is greater than or equal to every element of .
Dually, a lower bound or minorant of is defined to be an element ...
on the value for each
element of any sequence admissible to the spread.
Formally; a spread function
defines a fan if and only if given any sequence admissible to the spread
, then there exists some
such that, given any
then
(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
Binary may refer to:
Science and technology Mathematics
* Binary number, a representation of numbers using only two digits (0 and 1)
* Binary function, a function that takes two arguments
* Binary operation, a mathematical operation that ...
;
*the set of sequences of letters.
Commonly used spreads/fans
This section provides the definition of two spreads commonly used in the literature.
The universal spread (the
continuum
Continuum may refer to:
* Continuum (measurement), theories or models that explain gradual transitions from one condition to another without abrupt changes
Mathematics
* Continuum (set theory), the real line or the corresponding cardinal number ...
)
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
Binary may refer to:
Science and technology Mathematics
* Binary number, a representation of numbers using only two digits (0 and 1)
* Binary function, a function that takes two arguments
* Binary operation, a mathematical operation that ...
.
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
real
Real may refer to:
Currencies
* Brazilian real (R$)
* Central American Republic real
* Mexican real
* Portuguese real
* Spanish real
* Spanish colonial real
Music Albums
* ''Real'' (L'Arc-en-Ciel album) (2000)
* ''Real'' (Bright album) (2010) ...
s. 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
if and only if
:
,
and the function
(the dressed spread representing the
real numbers
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every real ...
).
References
*
L. E. J. Brouwer
Luitzen Egbertus Jan Brouwer (; ; 27 February 1881 – 2 December 1966), usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, who worked in topology, set theory, measure theory and compl ...
''Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre'', KNAW Verhandelingen, 5: 1–43 (1918A)
*
Michael Dummett
Sir Michael Anthony Eardley Dummett (27 June 1925 – 27 December 2011) was an English academic described as "among the most significant British philosophers of the last century and a leading campaigner for racial tolerance and equality." He wa ...
''Elements of Intuitionism'', Oxford University Press (1977)
*
A. S. Troelstra ''Choice Sequences: A Chapter of Intuitionistic Mathematics'', Clarendon Press (1977)
{{reflist
Intuitionism