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