Namespaces
Variants
Actions

Spread (in intuitionistic logic)

From Encyclopedia of Mathematics
Jump to: navigation, search


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 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