Decidability and Specker sequences in intuitionistic mathematics

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema (which we call ED ) about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED . We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)