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 $ \Pi $ of sequences of natural numbers is called a spread if the following conditions are satisfied: 1) there exists an effective rule $ a $( a so-called spread law) by which for any sequences $ \langle n _ {1} \dots n _ {m} \rangle $ one can determine whether or not it is a node of $ \Pi $; 2) the empty sequence $ \langle \rangle $ is a node of any spread; 3) if the sequence $ \langle n _ {1} \dots n _ {m} \rangle $ is a node of the spread, then any initial sequence of it, of the form $ \langle n _ {1} \dots n _ {i} \rangle $ for $ i \leq m $, is also a node of $ \Pi $; and 4) if the sequence $ \langle n _ {1} \dots n _ {m} \rangle $ is a node of $ \Pi $, then there exists a positive integer $ k $ such that $ \langle n _ {1} \dots n _ {m} , k \rangle $ is a node of $ \Pi $.

If one orders the sequences of positive integers by considering that $ \tau < \pi $ if and only if $ \tau $ is a proper initial part of $ \pi $, then from the point of view of this order the spread $ \Pi $ is an infinite tree with origin $ \langle \rangle $, given effectively (given by a law). A choice sequence $ \alpha $( or, more generally, an arbitrary effective function converting natural numbers into natural numbers) is called an element of a spread $ \Pi $, symbolically $ \alpha \in \Pi $, if for any $ n $ the sequence $ \langle \alpha ( 0) \dots \alpha ( n - 1 ) \rangle $ is a node of $ \Pi $. In applications one often has to deal with the notion of a labelled spread. A labelled spread $ \Gamma $ consists of a spread $ \Pi $ and an effective rule $ \Gamma _ \Pi $( the so-called complementary spread law) attributing to each node $ \pi $ of $ \Pi $ some object $ \Gamma _ \Pi ( \pi ) $. Thus there is a natural correspondence between each element of the spread $ \Pi $ and a sequence of objects given by the law $ \Gamma _ \Pi $.

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 $ \langle \rangle $ correspond to $ 0 $, let the operation of concatenating two sequences be coded by a primitive recursive function $ x * y $, and let $ \widehat{x} $ denote the number of the sequence with unique element $ x $. The statement that the tuple with number $ x $ is a node of the spread given by $ a $ is written as $ a ( x) = 0 $. Then the formula $ \mathop{\rm Spr} ( a) $ describing the notion "the function a defines a spread" is written in the form

$$ a ( 0) = 0 \& \forall x y ( a ( x * y ) = 0 \supset a ( x) = 0 ) \& $$

$$ \& \ \forall x ( a ( x) = 0 \supset \exists y ( a ( x * \widehat{y} ) = 0 ) ) . $$

Finally, if by $ \overline \alpha \; ( n) $ one denotes the number of the sequence $ \langle \alpha ( 0) \dots \alpha ( n - 1 ) \rangle $, where $ n $ is the length of the sequence, then the formula $ \alpha \in a $( "a is an element of the spread given by a" ) is written as $ \forall x a ( \overline \alpha \; ( x) ) = 0 $.

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