View source for Spread (in intuitionistic logic)

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868901.png" /> of sequences of natural numbers is called a spread if the following conditions are satisfied: 1) there exists an effective rule <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868902.png" /> (a so-called spread law) by which for any sequences <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868903.png" /> one can determine whether or not it is a node of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868904.png" />; 2) the empty sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868905.png" /> is a node of any spread; 3) if the sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868906.png" /> is a node of the spread, then any initial sequence of it, of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868907.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868908.png" />, is also a node of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s0868909.png" />; and 4) if the sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689010.png" /> is a node of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689011.png" />, then there exists a positive integer <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689012.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689013.png" /> is a node of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689014.png" />.

If one orders the sequences of positive integers by considering that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689015.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689016.png" /> is a proper initial part of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689017.png" />, then from the point of view of this order the spread <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689018.png" /> is an infinite tree with origin <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689019.png" />, given effectively (given by a law). A choice sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689020.png" /> (or, more generally, an arbitrary effective function converting natural numbers into natural numbers) is called an element of a spread <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689021.png" />, symbolically <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689022.png" />, if for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689023.png" /> the sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689024.png" /> is a node of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689025.png" />. In applications one often has to deal with the notion of a labelled spread. A labelled spread <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689026.png" /> consists of a spread <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689027.png" /> and an effective rule <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689028.png" /> (the so-called complementary spread law) attributing to each node <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689029.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689030.png" /> some object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689031.png" />. Thus there is a natural correspondence between each element of the spread <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689032.png" /> and a sequence of objects given by the law <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689033.png" />.

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689034.png" /> correspond to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689035.png" />, let the operation of concatenating two sequences be coded by a primitive recursive function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689036.png" />, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689037.png" /> denote the number of the sequence with unique element <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689038.png" />. The statement that the tuple with number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689039.png" /> is a node of the spread given by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689040.png" /> is written as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689041.png" />. Then the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689042.png" /> describing the notion  "the function a defines a spread"  is written in the form

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689043.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689044.png" /></td> </tr></table>

Finally, if by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689045.png" /> one denotes the number of the sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689046.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689047.png" /> is the length of the sequence, then the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689048.png" /> ( "a is an element of the spread given by a" ) is written as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086890/s08689049.png" />.

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>