An interpretation of the Sigma-2 fragment of classical Analysis in System T

TL;DR

This paper demonstrates that the $\,\Sigma_2$-fragment of classical Analysis can be interpreted constructively within G"odel's System T by extending it with a continuations operator, avoiding bar recursion.

Contribution

It introduces a realizability interpretation of the $\,\Sigma_2$-fragment using only System T and a continuations operator, bypassing bar recursion.

Findings

The $\,\Sigma_2$-fragment is essentially constructive.

Weak Church's Rule holds for this fragment.

The result applies even with the full Axiom of Choice.

Abstract

We show that it is possible to define a realizability interpretation for the $\Sigma_2$-fragment of classical Analysis using G\"odel's System T only. This supplements a previous result of Schwichtenberg regarding bar recursion at types 0 and 1 by showing how to avoid using bar recursion altogether. Our result is proved via a conservative extension of System T with an operator for composable continuations from the theory of programming languages due to Danvy and Filinski. The fragment of Analysis is therefore essentially constructive, even in presence of the full Axiom of Choice schema: Weak Church's Rule holds of it in spite of the fact that it is strong enough to refute the formal arithmetical version of Church's Thesis.