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.
|||A. Heyting, "Intuitionism: an introduction" , North-Holland (1970)|
|[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=12218