## System T and the Product of Selection Functions

### Thomas Powell (joint work with Martin
Escardo and Paulo Oliva)

Godel's primitive recursive functionals can be seen as a computational
analogue of induction, in the sense that they directly realise the
dialectica interpretation of the induction rule. Furthermore, it is
well known that the fragment of arithmetic with induction restricted
to Sigma_n formulas is dialectica interpreted by the fragment of
Godel's system T with recursion restricted to formulas of type level
n-1.

A lesser known hierarchy of fragments of arithmetic are those based on
the axiom of finite choice, which were shown by Parsons to be strictly
interleaving on the induction fragments. In this presentation I
discuss the dialectica interpretation of these fragments, and argue
that the natural computational analogue of finite choice is given by
the product of selection functions - an intuitive procedure that
computes optimal strategies in sequential games.

Finally, I will show that this product of selection functions is
equivalent to Godel's primitive recursive functionals, and compare the
corresponding fragments of system T in a computational version of
Parsons' result.

This is a survey of work done in collaboration with Paulo Oliva and
Martin Escardo.