Namespaces
Variants
Actions

Fan

From Encyclopedia of Mathematics
Revision as of 19:38, 5 June 2020 by Ulf Rehmann (talk | contribs) (tex encoded by computer)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search


finitary spread

A spread (cf. Spread (in intuitionistic logic)) $ \pi $ such that for any node $ \langle n _ {1} \dots n _ {m} \rangle $ of $ \pi $ there exists only a finite number of natural numbers $ k $ for which $ \langle n _ {1} \dots n _ {m} , k\rangle $ is a node of $ \pi $.

In the language of formal intuitionistic mathematical analysis, the function $ \mathop{\rm Fan} ( a) $, which expresses the concept "the function a defines a fan" , is written as

$$ \tag{* } \mathop{\rm Spr} ( a) \& \ \forall x ( a( x)= 0 \supset \ \exists y \forall z ( a( x * \widehat{z} ) = 0 \supset z \leq y)), $$

where $ \mathop{\rm Spr} ( a) $ means "the function a defines a spread" .

Brouwer's fan theorem: If there exists a rule with the aid of which a certain object — say, a natural number — can be assigned to each element of a fan, then there exists a natural number $ z $ such that for each element of the fan this object is defined by the first $ z $ values of the element. Brouwer's theorem is used in proving many specifically intuitionistic facts such as the uniform continuity of every real function defined on a closed interval. In formal intuitionistic mathematical analysis Brouwer's fan theorem is usually proved with the aid of bar induction and Brouwer's continuity principle (cf. Intuitionism). In the language of this formal theory the fan theorem may be written down as follows:

$$ \mathop{\rm Fan} ( a) \& \ ( \forall \alpha \in a ) \exists x \phi ( \alpha , x) \supset $$

$$ \supset \ \exists z ( \forall \alpha \in a) \exists x ( \forall \beta \in a) ( \overline \alpha \; ( z) = \overline \beta \; ( z) \supset \phi ( \beta , x)). $$

References

[1] S.C. Kleene, R.E. Vesley, "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland (1965)

Comments

Formula (*) can be read as: An element of a fan $ a $ is an infinite sequence $ \alpha $ all finite initial segments of which belong to $ a $.

References

[a1] A.S. Troelstra, "Choice sequences" , Clarendon Press (1977)
How to Cite This Entry:
Fan. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Fan&oldid=46903
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article