Fan

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[edit]

Comments[edit]

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[edit]