On constructing completions. (English) Zbl 1099.03044

This paper is based on the constructive set theory CZF of P. Aczel [in: Logic colloquium ’77, Proc., Wroclaw 1977, Stud. Logic Found. Math. 96, 55–66 (1978; Zbl 0481.03035)]. If \(A\) and \(B\) are sets, a total relation \(r\) between \(A\) and \(B\) is defined to be a subset of \(A\times B\) such that, for every \(x\) in \(A\), there is \(y\) in \(B\) with \((x,y)\in r\). The class of such relations is denoted \(\text{mv}(A,B)\). The authors use the following refinement principle, provable in CZF: For sets \(A\) and \(B\), there is a set \(C\subseteq \text{mv}(A,B)\) such that, for every \(r\in \text{mv}(A,B)\), there is \(s\in C\) with \(s\subseteq r\). From this, they deduce that the Dedekind cuts in an ordered set form a set. In particular, the Dedekind reals form a set. A further generalization is obtained by using Richman’s method for completing an arbitrary metric space without sequences to show that the completion of a separable metric space is a set even if the space is a proper class. Thus, every complete separable metric space is a set.


03E70 Nonclassical and second-order set theories
03F65 Other constructive mathematics
54E35 Metric spaces, metrizability


Zbl 0481.03035
Full Text: DOI Link


[1] The L. E. J. Brouwer Centenary Symposium pp 1– (1982)
[2] From Sets and Types to Topology and Analysis (2005)
[3] DOI: 10.1016/S0304-3975(02)00704-1 · Zbl 1044.54001
[4] DOI: 10.2140/pjm.2000.196.213 · Zbl 1046.03036
[5] DOI: 10.1007/s001530050149 · Zbl 0936.03060
[6] Constructive set theory 40 pp 347– (1975)
[7] Twenty-Five Years of Constructive Type Theory pp 127– (1998)
[8] Logic, Methodology, and Philosophy of Science VII pp 17– (1986)
[9] Intuitionistic Type Theory (1980)
[10] Logic Colloquium ’73 pp 73– (1975)
[11] DOI: 10.1016/j.apal.2004.08.002 · Zbl 1068.03045
[12] Reuniting the Antipodes–Constructive and Nonstandard Views of the Continuum (Proceedings of the Symposion) pp 39– (1999)
[13] Constructive Analysis (1985) · Zbl 0656.03042
[14] DOI: 10.1016/S0304-3975(02)00699-0 · Zbl 1045.54002
[15] Foundations of Constructive Analysis (1967) · Zbl 0183.01503
[16] Logic Colloquium ’77 pp 55– (1978)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.