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

arXiv1301.5089MaRDI QIDQ6238935FDOQ6238935

Danko Ilik

Publication date: 22 January 2013

Abstract: We show that it is possible to define a realizability interpretation for the $Sigm{a}_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.

Mathematics Subject Classification ID

Theory of programming languages (68N15) Subsystems of classical logic (including intuitionistic logic) (03B20) Foundations of classical theories (including reverse mathematics) (03B30) Higher-type and set recursion theory (03D65) Axiom of choice and related propositions (03E25) Relative consistency and interpretations (03F25) Constructive and recursive analysis (03F60) Functionals in proof theory (03F10)

This page was built for publication: An interpretation of the Sigma-2 fragment of classical Analysis in System T

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6238935)