Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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

Danko Ilik 1 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We show that it is possible to define a realizability interpretation for the Σ 2 -fragment of classical Analysis using Gödel'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 con-structive, 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.
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Danko Ilik Connect in order to contact the contributor
Submitted on : Monday, December 8, 2014 - 4:20:15 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Monday, March 9, 2015 - 12:10:16 PM


Files produced by the author(s)


  • HAL Id : hal-01092411, version 1



Danko Ilik. An interpretation of the Sigma-2 fragment of classical Analysis in System T. 2014. ⟨hal-01092411⟩



Record views


Files downloads