Subcountability under realizability.
Charles McCarty · Notre Dame Journal of Formal Logic · 1986
Among the open problems in the metamathematics of constructivity catalogued by Michael Beeson in [2] are those of the consistency of IZF with SCDS and with SCMS.SCDS is the assertion that every discrete set is subcountable; SCMS asserts that every metric space is subcountable.Solutions to the SCDS and SCMS problems serve not only to advance the techniques of model theory for intuitionism, but also to give some confirmation to three distinct insights into the overall structure of constructive mathematics.The first insight is that of Bishop, who suggested that even the strongest constructive systems should admit interpretations that reveal constructive mathematics as having "numerical meaning".The second insight is GreenleaPs intuition that the mainspring of the constructive theory of cardinality is not "raw size" of sets, as it is on the classical account, but rather logical or mathematical structure.The third is perhaps more a presupposition of traditional intuitionism than an insight.It was presupposed by Brouwer that the domain of significant mathematics includes only sets which are, from the classical standpoint, relatively small and highly structured.By working the model-theoretic approach to realizability which derives from Kleene's work, we show that the full intuitionistic set theory IZF is consistent with SCDS and SCMS.In fact, both SCDS and SCMS hold in a realizability structure, V(Kl), which is a close relative of forms of realizability presented by Beeson in [1].We also formulate a new principle, SCAS, which is a strong generalization of both SCDS and SCMS.SCAS is the assertion that every set with strict apart-*The style of reasoning exploited in this paper was developed jointly by the author and Dr.