English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

First, we reconstruct Wim Veldman's result that Open Induction on Cantorspace can be derived from Double-negation Shift and Markov's Principle. Indoing this, we notice that one has to use a countable choice axiom in the proofand that Markov's Principle is replaceable by slightly strengthening theDouble-negation Shift schema. We show that this strengthened version ofDouble-negation Shift can nonetheless be derived in a constructive intermediatelogic based on delimited control operators, extended with axioms forhigher-type Heyting Arithmetic. We formalize the argument and thus obtain aproof term that directly derives Open Induction on Cantor space by the shiftand reset delimited control operators of Danvy and Filinski.

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