Document Open Access Logo

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators

Authors Danko Ilik, Keiko Nakata

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2013.188.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Danko Ilik
Keiko Nakata

Cite AsGet BibTex

Danko Ilik and Keiko Nakata. A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 188-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.TYPES.2013.188

Abstract

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.
Keywords
  • Open Induction
  • Axiom of Choice
  • Double Negation Shift
  • Markov's Principle
  • delimited control operators

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. Michael Beeson. Goodman’s theorem and beyond. Pacific Journal of Mathematics, 84:1-16, 1979. Google Scholar
  3. 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. Google Scholar
  4. 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.
  5. Thierry Coquand. A note on the open induction principle, 1997. Google Scholar
  6. Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical report, Computer Science Department, University of Copenhagen, 1989. DIKU Rapport 89/12. Google Scholar
  7. Olivier Danvy and Andrzej Filinski. Abstracting control. In LISP and Functional Programming, pages 151-160, 1990. Google Scholar
  8. Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361-391, 1992. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. Danko Ilik. Delimited control operators prove double-negation shift. Annals of Pure and Applied Logic, 163(11):1549-1559, 2012. Google Scholar
  12. Ulrich Kohlenbach. Applied proof theory: proof interpretations and their use in mathematics. Springer Monographs in Mathematics. Springer-Verlag, Berlin, 2008. Google Scholar
  13. Jean-Louis Krivine. Dependent choice, `quote' and the clock. Theor. Comput. Sci., 308(1-3):259-276, 2003. Google Scholar
  14. Chetan Murthy. Extracting Classical Content from Classical Proofs. PhD thesis, Department of Computer Science, Cornell University, 1990. Google Scholar
  15. Jean-Claude Raoult. Proving open properties by induction. Information Processing Letters, 29:19-23, 1988. Google Scholar
  16. 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. Google Scholar
  17. Anne S. Troelstra, editor. Metamathematical Investigations of Intuitionistic Arithmetic and analysis. Lecture Notes in Mathematics 344. Springer-Verlag, 1973. Google Scholar
  18. Wim Veldman. The principle of open induction on the unit interval [0,1] and some of its equivalents. Slides from presentation, May 2010. Google Scholar
  19. Wim Veldman. Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s Alternative. ArXiv e-prints, June 2011. Google Scholar
  20. Wim Veldman. Some further equivalents of Brouwer’s Fan Theorem and of Kleene’s Alternative. ArXiv e-prints, November 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact