##
On Selection Functions and Generalised Quantifiers

### Paulo Oliva

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).