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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Liste complète des métadonnées

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 : Wednesday, March 27, 2019 - 4:41:29 PM
Document(s) archivé(s) le : 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

402

Files downloads

103