Baire空间上的杆诱导原理与连续性
Principles of bar induction and continuity on Baire space
摘要：
Brouwer运算，也称为归纳定义的邻域函数，提供了Baire空间上连续性的一个很好的概念，它自然地扩展了Cantor空间上一致连续性的概念。本文引入了Baire空间的一个连续性原理，即从Baire空间到自然数集合的每一个逐点连续函数都是由Brouwer-运算导出的.在Bishop构造性数学中，我们证明了上述原理等价于一个强度介于单调杆归纳和可判定杆归纳之间的杆归纳。我们还表明，单调的酒吧感应和可判定的酒吧感应的特点是类似的连续性原则。此外，我们表明，$Π^{0}_{1}$酒吧归纳一般意味着LLPO（较少的有限原则的全知）。这一点，连同$Σ^{0}_{1}$条归纳蕴涵LPO（全知的有限原理）的事实，表明直观上可接受的条归纳形式要求条是单调的。
英文摘要：
Brouwer-operations, also known as inductively defined neighbourhood functions, provide a good notion of continuity on Baire space which naturally extends that of uniform continuity on Cantor space. In this paper, we introduce a continuity principle for Baire space which says that every pointwise continuous function from Baire space to the set of natural numbers is induced by a Brouwer-operation. Working in Bishop constructive mathematics, we show that the above principle is equivalent to a version of bar induction whose strength is between that of the monotone bar induction and the decidable bar induction. We also show that the monotone bar induction and the decidable bar induction can be characterised by similar principles of continuity. Moreover, we show that the $Π^{0}_{1}$ bar induction in general implies LLPO (the lesser limited principle of omniscience). This, together with a fact that the $Σ^{0}_{1}$ bar induction implies LPO (the limited principle of omniscience), shows that an intuitionistically acceptable form of bar induction requires the bar to be monotone.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
