Spread (in intuitionistic logic)
A notion in intuitionistic mathematics (see Intuitionism). It is a population, a species, consisting of finite sequences (cf. Tuple) of positive integers, called the nodes of the spread (or the admissible sequences of the spread). More precisely, a species of sequences of natural numbers is called a spread if the following conditions are satisfied: 1) there exists an effective rule
(a so-called spread law) by which for any sequences
one can determine whether or not it is a node of
; 2) the empty sequence
is a node of any spread; 3) if the sequence
is a node of the spread, then any initial sequence of it, of the form
for
, is also a node of
; and 4) if the sequence
is a node of
, then there exists a positive integer
such that
is a node of
.
If one orders the sequences of positive integers by considering that if and only if
is a proper initial part of
, then from the point of view of this order the spread
is an infinite tree with origin
, given effectively (given by a law). A choice sequence
(or, more generally, an arbitrary effective function converting natural numbers into natural numbers) is called an element of a spread
, symbolically
, if for any
the sequence
is a node of
. In applications one often has to deal with the notion of a labelled spread. A labelled spread
consists of a spread
and an effective rule
(the so-called complementary spread law) attributing to each node
of
some object
. Thus there is a natural correspondence between each element of the spread
and a sequence of objects given by the law
.
In the language of formal intuitionistic mathematical analysis a spread is given by a function — its spread law. With that end in view one considers the standard primitive recursive one-to-one correspondence between sequences of natural numbers and natural numbers. Let the tuple correspond to
, let the operation of concatenating two sequences be coded by a primitive recursive function
, and let
denote the number of the sequence with unique element
. The statement that the tuple with number
is a node of the spread given by
is written as
. Then the formula
describing the notion "the function a defines a spread" is written in the form
![]() |
![]() |
Finally, if by one denotes the number of the sequence
, where
is the length of the sequence, then the formula
( "a is an element of the spread given by a" ) is written as
.
In the foundations of mathematics, generalizations of the concept of a spread, in which sequences of natural numbers are replaced by sequences of more complicated objects (for example, by sequences consisting of choice sequences) are also considered.
References
[1] | A. Heyting, "Intuitionism: an introduction" , North-Holland (1970) |
Comments
References
[a1] | M.A.E. Dummett, "Elements of intuitionism" , Oxford Univ. Press (1977) |
[a2] | A.S. Troelstra, D. van Dalen, "Constructivism in mathematics, an introduction" , 1–2 , North-Holland (1988–1989) |
[a3] | A.S. Troelstra, "Principles of intuitionism" , Springer (1969) |
[a4] | A.S. Troelstra, "Choice sequences" , Clarendon Press (1977) |
[a5] | G. van der Hoeven, I. Moerdijk, "On choice sequences determined by spreads" J. Symbolic Logic , 49 (1984) pp. 908–916 |
Spread (in intuitionistic logic). Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Spread_(in_intuitionistic_logic)&oldid=48786