View source for Spread (in intuitionistic logic)

<!--
s0868901.png
$#A+1 = 49 n = 0
$#C+1 = 49 : ~/encyclopedia/old_files/data/S086/S.0806890 Spread (in intuitionistic logic)
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

A notion in intuitionistic mathematics (see [[Intuitionism|Intuitionism]]). It is a population, a [[Species|species]], consisting of finite sequences (cf. [[Tuple|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====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Heyting,   "Intuitionism: an introduction" , North-Holland  (1970)</TD></TR></table>

====Comments====

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  M.A.E. Dummett,   "Elements of intuitionism" , Oxford Univ. Press  (1977)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  A.S. Troelstra,   D. van Dalen,   "Constructivism in mathematics, an introduction" , '''1–2''' , North-Holland  (1988–1989)</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  A.S. Troelstra,   "Principles of intuitionism" , Springer  (1969)</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  A.S. Troelstra,   "Choice sequences" , Clarendon Press  (1977)</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  G. van der Hoeven,   I. Moerdijk,   "On choice sequences determined by spreads"  ''J. Symbolic Logic'' , '''49'''  (1984)  pp. 908–916</TD></TR></table>