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

TL;DR

This paper presents a constructive proof of Open Induction on Cantor space using delimited control operators, linking logic principles with programming language constructs.

Contribution

It introduces a new proof method that derives Open Induction from a strengthened Double-negation Shift schema via delimited control operators.

Findings

Constructive proof of Open Induction on Cantor space.

Connection between logical principles and control operators.

Formalization of the proof as a proof term.

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.