A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
From MaRDI portal
Publication:2968417
DOI10.4230/LIPICS.TYPES.2013.188zbMATH Open1359.03046arXiv1209.2229MaRDI QIDQ2968417
Publication date: 13 March 2017
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.
Full work available at URL: https://arxiv.org/abs/1209.2229
This page was built for publication: A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2968417)
