The usual existential and universal quantifiers over a set X can be thought of as type 2 operations, which take a predicate p : X -> Bool as input and return a Bool as output. If instead of Bool we allow an arbitrary set R, several other operations can also be thought of as "generalised quantifiers", e.g.
limit : (Nat -> A) -> A
supremum : (X -> Real) -> Real
integration : ([0,1] -> Real) -> Real.
A selection function for a quantifier phi : (X -> R) -> R is a function
e : (X -> R) -> X
which produces the point where the quantifier is attainable, i.e.
phi(p) = p(e(p)).
In the case of the existential quantifier, for instance, this is Hilbert's epsilon term. In the case of integration, the mean value theorem says that integration over C[0,1] has a selection function, i.e. for any p in C[0,1] there exists an x in [0,1] such that
integration(p) = p(x).
Hence, there must exists a function e : ([0,1] -> R) -> [0,1] such that
integration(p) = p(e(p)).
This talk aims to motivate the two concepts and various associated constructions through simple concrete examples from Nash equilibrium (backward induction), fixed point theory (Bekic's lemma), algorithms (backtracking) and proof theory (bar recursion). The talk is based on joint work with Martin Escardo (preprint).