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

https://hal.inria.fr/hal-01092411
Contributor : Danko Ilik <>
Submitted on : Monday, December 8, 2014 - 4:20:15 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Monday, March 9, 2015 - 12:10:16 PM

Files

shift-analysis.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01092411, version 1

Collections

Citation

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

Share

Metrics

Record views

439

Files downloads

124