Namespaces
Variants
Actions

Difference between revisions of "Fan"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
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)]]) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381801.png" /> such that for any node <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381802.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381803.png" /> there exists only a finite number of natural numbers <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381804.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381805.png" /> is a node of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381806.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381807.png" />, which expresses the concept  "the function a defines a fan" , is written as
+
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
  
<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/f/f038/f038180/f0381808.png" /></td> <td valign="top" style="width:5%;text-align:right;">(*)</td></tr></table>
+
$$ \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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f0381809.png" /> means  "the function a defines a spread" .
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f03818010.png" /> such that for each element of the fan this object is defined by the first <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f03818011.png" /> 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:
+
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:
  
<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/f/f038/f038180/f03818012.png" /></td> </tr></table>
+
$$
 +
\mathop{\rm Fan} ( a)  \& \
 +
( \forall \alpha \in a )
 +
\exists x  \phi ( \alpha , x) \supset
 +
$$
  
<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/f/f038/f038180/f03818013.png" /></td> </tr></table>
+
$$
 +
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f03818014.png" /> is an infinite sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f03818015.png" /> all finite initial segments of which belong to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f038/f038180/f03818016.png" />.
+
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)
How to Cite This Entry:
Fan. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Fan&oldid=18210
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article