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

Danko Ilik (1) , Keiko Nakata (2)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 Institute of Cybernetics

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.

Mots clés: Open Induction; Axiom of Choice; Double Negation Shift; Markov's Principle; delimited control operators

Domaines: Logique [math.LO]; Logique en informatique [cs.LO]; Langage de programmation [cs.PL]

Danko Ilik, Keiko Nakata. A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. Leibniz International Proceedings in Informatics , 2014, pp.288-201. ⟨10.4230/LIPIcs.TYPES.2013.188⟩. ⟨hal-01092427⟩