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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01092411
Contributeur : Danko Ilik <>
Soumis le : lundi 8 décembre 2014 - 16:20:15
Dernière modification le : mercredi 25 avril 2018 - 10:45:27
Document(s) archivé(s) le : lundi 9 mars 2015 - 12:10:16

Fichiers

shift-analysis.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

76