一句话：证明在函数可实现性拓扑斯中所有度量空间可分、可判等对象可数，从而给出直觉主义逻辑不可证明相关命题的模型。
论文研究直觉主义逻辑中度量空间可分性与集合可数性的可证明性边界。作者在函数可实现性拓扑斯中工作，并进一步在综合拓扑框架下分析一般空间：证明每个度量空间都是可分的，每个具有可判等性的对象都是可数的；更一般地，每个 T0 空间可分、每个离散空间可数。由此得到，直觉主义逻辑无法证明存在不可分度量空间或具有可判等性的不可数集合，即使额外假设 Dependent choice、Function choice、Markov 原理以及 Brouwer 的连续性与扇原理等被函数可实现性验证的原则。结果刻画了这些经典上显然的性质在构造性/可实现性语义下的必然成立性。
We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equality, even if we assume principles that are validated by function realizability, such as Dependent and Function choice, Markov's principle, and Brouwer's continuity and fan principles.