Premium
Decidability and Specker sequences in intuitionistic mathematics
Author(s) -
Ardeshir Mohammad,
Ramezanian Rasoul
Publication year - 2009
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200710094
Subject(s) - mathematics , decidability , sequence (biology) , limit of a sequence , monotone polygon , intuitionistic logic , axiom , bounded function , discrete mathematics , limit (mathematics) , combinatorics , propositional calculus , mathematical analysis , genetics , geometry , biology
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)