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)

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