A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one has to use a countable choice axiom in the proof and that Markov's Principle is replaceable by slightly strengthening the Double-negation Shift schema. We show that this strengthened version of Double-negation Shift can nonetheless be derived in a constructive intermediate logic based on delimited control operators, extended with axioms for higher-type Heyting Arithmetic. We formalize the argument and thus obtain a proof term that directly derives Open Induction on Cantor space by the shift and reset delimited control operators of Danvy and Filinski.
Open Induction
Axiom of Choice
Double Negation Shift
Markov's Principle
delimited control operators
188-201
Regular Paper
Danko
Ilik
Danko Ilik
Keiko
Nakata
Keiko Nakata
10.4230/LIPIcs.TYPES.2013.188
Zena M. Ariola and Hugo Herbelin. Minimal classical logic and control operators. In Thirtieth International Colloquium on Automata, Languages and Programming, ICALP'03, Eindhoven, The Netherlands, June 30 to July 4, 2003, volume 2719 of Lecture Notes in Computer Science, pages 871-885. Springer, 2003.
Michael Beeson. Goodman’s theorem and beyond. Pacific Journal of Mathematics, 84:1-16, 1979.
Ulrich Berger. A computational interpretation of open induction. In F. Titsworth, editor, Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science, pages 326-334. IEEE Computer Society, 2004.
Thierry Coquand. Constructive topology and combinatorics. In J. Myers and M. O'Donnell, editors, Constructivity in Computer Science, volume 613 of Lecture Notes in Computer Science, pages 159-164. Springer Berlin / Heidelberg, 1992. URL: http://dx.doi.org/10.1007/BFb0021089.
http://dx.doi.org/10.1007/BFb0021089
Thierry Coquand. A note on the open induction principle, 1997.
Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical report, Computer Science Department, University of Copenhagen, 1989. DIKU Rapport 89/12.
Olivier Danvy and Andrzej Filinski. Abstracting control. In LISP and Functional Programming, pages 151-160, 1990.
Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361-391, 1992.
Hugo Herbelin. An intuitionistic logic that proves Markov’s principle. In Proceedings, 25th Annual IEEE Symposium on Logic in Computer Science (LICS'10), Edinburgh, UK, 11-14 July 2010, page N/A. IEEE Computer Society Press, 2010.
Hugo Herbelin. A constructive proof of dependent choice, compatible with classical logic. In Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 25-28 June 2012, Dubrovnik, Croatia, pages 365-374. IEEE Computer Society, 2012.
Danko Ilik. Delimited control operators prove double-negation shift. Annals of Pure and Applied Logic, 163(11):1549-1559, 2012.
Ulrich Kohlenbach. Applied proof theory: proof interpretations and their use in mathematics. Springer Monographs in Mathematics. Springer-Verlag, Berlin, 2008.
Jean-Louis Krivine. Dependent choice, `quote' and the clock. Theor. Comput. Sci., 308(1-3):259-276, 2003.
Chetan Murthy. Extracting Classical Content from Classical Proofs. PhD thesis, Department of Computer Science, Cornell University, 1990.
Jean-Claude Raoult. Proving open properties by induction. Information Processing Letters, 29:19-23, 1988.
Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In Proc. Sympos. Pure Math., Vol. V, pages 1-27. American Mathematical Society, Providence, R.I., 1962.
Anne S. Troelstra, editor. Metamathematical Investigations of Intuitionistic Arithmetic and analysis. Lecture Notes in Mathematics 344. Springer-Verlag, 1973.
Wim Veldman. The principle of open induction on the unit interval [0,1] and some of its equivalents. Slides from presentation, May 2010.
Wim Veldman. Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s Alternative. ArXiv e-prints, June 2011.
Wim Veldman. Some further equivalents of Brouwer’s Fan Theorem and of Kleene’s Alternative. ArXiv e-prints, November 2013.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode