In the context of intuitionistic analysis, we consider the set consisting of all continuous functions from [0,1] to such that =0 and =1, and the set consisting of ’s in where there exists x[0,1] such that . It is well-known that there are weak counterexamples to the intermediate value theorem, and with Brouwer’s continuity principle we have . However, there exists no satisfying answer to . We try to answer to this question by reducing it to a schema 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 where. (shrink)

Let A be a subset of the constructive real line. What are the necessary and sufficient conditions for the set A such that A is continuously separated from other reals, i.e., there exists a continuous function f with f−1(0) = A? In this paper, we study the notions of closed sets and closure maps in constructive reverse mathematics.