弱 König 引理的更多保守性

我们证明了弱 König 引理的保守性结果，这些结果推广了 Harrington 的著名结论（针对 $\Pi^1_1$ 语句），且在某种程度上正交于 Simpson、Tanaka 和 Yamazaki 的推广（针对形如 $\forall X\exists!Y\psi$ 且 $\psi$ 为算术语句的命题）。特别地，我们证明了 $\mathsf{WKL}_0$ 对于良序原理在 $\mathsf{RCA}_0$ 上是保守的。我们还证明了紧致性（刻画了弱 König 引理）对于具有孤立奇点的连续函数的某些结果是可省略的。