The principle of open induction and Specker sequences
Mohammad Ardeshir, Zahra Ghafouri · Logic Journal of IGPL · 2016
The schema ED asserts that ‘there exists an intuitionistically enumerable subset of |${\Bbb N}$| which is not intuitionistically decidable.’ In this article, we prove that in the presence of Markov’s Principle over Bishop’s constructive analysis, |$ eg {\bf ED}$| is equivalent to the principle of open induction on |$[0,1]$|, via Specker sequences.