In the context of intuitionistic analysis, we consider the set FF consisting of all continuous functions ϕϕ from [0,1][0,1] to RR such that ϕ(0)=0ϕ(0)=0 and ϕ(1)=1ϕ(1)=1, and the set I0I0 consisting of ϕϕ’s in FF where there exists x∈[0,1]x∈[0,1] such that View the MathML sourceϕ(x)=12. It is well-known that there are weak counterexamples to the intermediate value theorem, and with Brouwer’s continuity principle we have I0≠FI0≠F. However, there exists no satisfying answer to View the MathML sourceI0¬¬=?F. We try to answer to this question by reducing it to a schema (which we call View the MathML sourceED) about intuitionistic decidability that asserts “there exists an intuitionistically enumerable set that is not intuitionistically decidable”. We also introduce the notion of strong Specker double sequence , and prove that the existence of such a double sequence is equivalent to the existence of a function ϕ∈Fmonϕ∈Fmon where View the MathML source¬∃x∈[0,1](ϕ(x)=12)

Keywords