Namespaces
Variants
Actions

Difference between revisions of "Spread (in intuitionistic logic)"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
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" />.
+
<!--
 +
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.
 +
-->
  
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" />.
+
{{TEX|auto}}
 +
{{TEX|done}}
  
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
+
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 $.
  
<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>
+
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  $.
  
<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>
+
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
  
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" />.
+
$$
 +
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.
 
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.
Line 15: Line 76:
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Heyting,  "Intuitionism: an introduction" , North-Holland  (1970)</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Heyting,  "Intuitionism: an introduction" , North-Holland  (1970)</TD></TR></table>
 
 
  
 
====Comments====
 
====Comments====
 
  
 
====References====
 
====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>
 
<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>

Latest revision as of 08:22, 6 June 2020


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)

Comments

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
How to Cite This Entry:
Spread (in intuitionistic logic). Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Spread_(in_intuitionistic_logic)&oldid=48786
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article