Difference between revisions of "Fan"
(Importing text file) |
Ulf Rehmann (talk | contribs) m (tex encoded by computer) |
||
| Line 1: | Line 1: | ||
| + | <!-- | ||
| + | f0381801.png | ||
| + | $#A+1 = 16 n = 0 | ||
| + | $#C+1 = 16 : ~/encyclopedia/old_files/data/F038/F.0308180 Fan, | ||
| + | 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}} | ||
| + | |||
''finitary spread'' | ''finitary spread'' | ||
| − | A spread (cf. [[Spread (in intuitionistic logic)|Spread (in intuitionistic logic)]]) | + | A spread (cf. [[Spread (in intuitionistic logic)|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 | + | 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 | + | 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 | + | 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|bar induction]] and Brouwer's continuity principle (cf. [[Intuitionism|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==== | ====References==== | ||
<table><TR><TD valign="top">[1]</TD> <TD valign="top"> S.C. Kleene, R.E. Vesley, "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland (1965)</TD></TR></table> | <table><TR><TD valign="top">[1]</TD> <TD valign="top"> S.C. Kleene, R.E. Vesley, "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland (1965)</TD></TR></table> | ||
| − | |||
| − | |||
====Comments==== | ====Comments==== | ||
| − | Formula (*) can be read as: An element of a fan | + | 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==== | ====References==== | ||
<table><TR><TD valign="top">[a1]</TD> <TD valign="top"> A.S. Troelstra, "Choice sequences" , Clarendon Press (1977)</TD></TR></table> | <table><TR><TD valign="top">[a1]</TD> <TD valign="top"> A.S. Troelstra, "Choice sequences" , Clarendon Press (1977)</TD></TR></table> | ||
Latest revision as of 19:38, 5 June 2020
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) |
Fan. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Fan&oldid=18210