Speaker: Ulrich Berger (Swansea University)

Abstract: Consider a continuous functional F : (N -> B) -> N where N is the type
of natural numbers and B is the type of Booleans, both endowed with
the discrete topology, and the function space N -> B carries the
pointwise topology. By a compactness argument (Koenig's Lemma or Fan
Theorem), F is uniformly continuous. Therefore, there exists a least
modulus of uniform continuity for F, that is, a least natural number m
such that F equates any two arguments that coincide below m. The
mapping F |-> m is called Fan Functional. Gandy showed that the Fan
Functional is computable. Later it was shown that it is computable
even in the restricted sense of Kleene's schemata (S1-S9), or,
equivalently, PCF.  In this talk we show that the Fan Functional is
the computational content of a constructive proof of the uniform
continuity of F.