On Bar Recursive Interpretations of Analysis

Research output: ThesisDoctoral Thesis

Abstract

This dissertation concerns the computational interpretation of analysis via proof interpretations, and examines the variants of bar recursion that have been used to interpret the axiom of choice. It consists of an applied and a theoretical component.

The applied part contains a series of case studies which address the issue of understanding the meaning and behaviour of bar recursive programs extracted from proofs in analysis. Taking as a starting point recent work of Escardo and Oliva on the product of selection functions, solutions to Goedel’s functional interpretation of several well known theorems of mathematics are given, and the semantics of the extracted programs described. In particular, new game-theoretic computational interpretations are found for weak Koenig’s lemma for Σ^0_1-trees and for the minimal-bad-sequence argument.

On the theoretical side several new definability results which relate various modes of
bar recursion are established. First, a hierarchy of fragments of system T based on finite
bar recursion are defined, and it is shown that these fragments are in one-to-one correspondence with the usual fragments based on primitive recursion. Secondly, it is shown that the so called ‘special’ variant of Spector’s bar recursion actually defines the general one. Finally, it is proved that modified bar recursion (in the form of the implicitly controlled product of selection functions), open recursion, update recursion and the Berardi-BezemCoquand realizer for countable choice are all primitive recursively equivalent in the model of continuous functionals.
Original languageEnglish
QualificationPh.D.
Awarding Institution
  • Queen Mary University, London
Supervisors/Advisors
  • Oliva, Paulo, Supervisor, External person
  • Robinson, Edmund, Supervisor, External person
Award date31 Oct 2013
Publication statusPublished - 2013

Cite this