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.