凝聚原理与Bolzano-Weierstrass原理

本文旨在确定Bolzano-Weierstrass原理(BW)及其一个弱变体的实例的逻辑和计算强度。我们证明BW在实例意义上等价于$\Sigma^0_1$-树的弱König引理($\Sigma^0_1$-WKL)。这意味着，从每个有界实数序列可以计算出一个无穷$\Sigma^0_1$-0/1树，使得该树的每个无穷分支都产生一个聚点，反之亦然。特别地，这表明度d >> 0'恰好是那些对所有有界可计算序列都包含一个聚点的度。设BW_weak为如下原理：每个有界实数序列都包含一个柯西子序列(收敛但不一定快速收敛的序列)。我们证明BW_weak在实例意义上等价于(强)凝聚原理(StCOH)，并利用这一点获得了BW_weak的计算和逻辑强度的分类。特别地，我们证明BW_weak不能解决停机问题，也不会导致超出原始递归的增长。因此它严格弱于BW。我们还讨论了BW_weak的可能用途。