Veldman关于Cantor空间上开归纳的一个直接证明
A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
摘要：
首先，我们重建了Wim Veldman关于Cantor空间上的开归纳可以由双否定移位和马尔可夫原理导出的结果。在这样做的时候，我们注意到在证明中必须使用可数选择公理，并且马尔可夫原理可以通过稍微加强双重否定移位模式来替换。我们表明，这种加强版本的双否定移位仍然可以在一个建设性的中间逻辑的基础上定界控制算子，扩展与公理更高类型的Heyting算术。我们形式化的参数，从而获得一个证明项，直接导出康托空间上的移位和复位分隔控制算子的Danvy和Filinski的开放归纳。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
