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