The double negation of the intermediate value theorem (Q636312)

This paper studies the double negation of the intermediate value theorem for monotonous, continuous functions in an intuitionistic (constructive) setting. It is proved that if there exists a monotonous, continuous function for which the double negation of the intermediate value property doesn't hold, then there exists a Specker sequence. Furthermore, under the same assumption, there also exists an intuitionistically enumerable subset that is not decidable. A further main result of the paper is that there exists a monotonous, continuous function for which the double negation of the intermediate value property doesn't hold if and only if there exists a strong Specker double sequence. The authors relate their results to the open question of whether there exists a continuous function (so: not necessarily monotonous) for which the double negation of the intermediate value property doesn't hold. Two related articles are [\textit{M. Ardeshir} and \textit{R. Ramezanian}, Math. Log. Q. 55, No. 6, 637--648 (2009; Zbl 1192.03046)] and [\textit{W. Veldman}, J. UCS 11, No. 12, 2142--2158 (2005; Zbl 1128.03049)].