摘要 Abstract
我们构造了一个拓扑斯,在其中Dedekind实数是可数的。这个拓扑斯来源于一种新的实现性概念,我们称之为参数化实现性,基于部分组合代数,其应用依赖于参数。实现者在给定参数集上均匀操作。我们的构造使用了Joseph Miller发现的一组实数序列$[0,1]$,该序列在某种意义上是非对角化的,即任何从该序列的表示中一致oracle-可计算的实数必须已经出现在序列中。当将其用作参数集时,这将产生一个拓扑斯,在其中非对角化序列成为Dedekind实数的满射,从而使其内部可数。所得的拓扑斯是直觉主义的:它否定排中律和可数选择公理。然而,分析学的大部分内容在内部仍然成立。Cauchy实数是不可数的。Hilbert立方是可数的,因此Lawvere的理论可以推出布劳威尔不动点定理。中间值定理和弱排中律的解析形式成立,而弱排中律则不成立。虽然没有实值映射具有跳跃,但所有此类映射是否连续仍然是开放问题。最后,闭区间$[0,1]$,由于是可数的,可以用总长度小于任意$\epsilon > 0$的开区间的序列覆盖,且没有有限子覆盖。然而,我们证明了任何使用有理端点的区间进行的覆盖必须承认有限子覆盖。
We construct a topos in which the Dedekind reals are countable. The topos arises from a new kind of realizability, which we call parameterized realizability, based on partial combinatory algebras whose application depends on a parameter. Realizers operate uniformly with respect to a given parameter set. Our construction uses a sequence of reals in $[0,1]$, discovered by Joseph Miller, that is non-diagonalizable in the sense that any real which is oracle-computable uniformly from representations of the sequence must already appear in it. When used as the parameter set, this yields a topos in which the non-diagonalizable sequence becomes an epimorphism onto the Dedekind reals, rendering them internally countable. The resulting topos is intuitionistic: it refutes both the law of excluded middle and countable choice. Nevertheless, much of analysis survives internally. The Cauchy reals are uncountable. The Hilbert cube is countable, so Brouwer's fixed-point theorem follows from Lawvere's. The intermediate value theorem and the analytic form of the lesser limited principle of omniscience hold, while the limited principle of omniscience fails. Although no real-valued map has a jump, it remains open whether all such maps are continuous. Finally, the closed interval $[0,1]$, being countable, can be covered by a sequence of open intervals of total length less than any $\epsilon > 0$, with no finite subcover. Yet, we show that any cover using intervals with rational endpoints must admit a finite subcover.