Equivalence of bar induction and bar recursion for continuous functions with continuous moduli
Equivalence of bar induction and bar recursion for continuous functions with continuous moduli
复制标题
对于具有连续模的连续函数，条形归纳和条形递归等价
DOI：
10.1016/j.apal.2019.04.001
复制
发表时间：
2019
影响因子：
0.8
通讯作者：
Makoto Fujiwara and Tatsuji Kawai
中科院分区：
文献类型：
--
作者：
Makoto Fujiwara and Tatsuji Kawai
我们比较布劳威尔的酒吧定理和斯佩克特的酒吧递归的最低类型的建设性逆向数学的背景下。为此，我们重新制定酒吧递归作为一个逻辑原则，说明存在一个酒吧递归的每一个功能，作为停止条件的酒吧递归。然后，我们证明了可判定的酒吧感应是等价的存在一个酒吧递归的每个连续函数从N N到N的连续模。我们还介绍了风扇递归，酒吧递归的二叉树，并证明了可判定风扇定理是等价于存在一个风扇递归的每个连续函数从{0，1} N到N的连续模。棒归纳法的等价性在所有有限类型中的直觉算术的扩展版本上都成立，并被哥德尔的辩证法解释的特征原则所扩充。另一方面，在不使用这些额外原理的情况下，证明了Fan定理的等价性。
We compare Brouwer's bar theorem and Spector's bar recursion for the lowest type in the context of constructive reverse mathematics. To this end, we reformulate bar recursion as a logical principle stating the existence of a bar recursor for every function which serves as the stopping condition of bar recursion. We then show that the decidable bar induction is equivalent to the existence of a bar recursor for every continuous function from N N to N with a continuous modulus. We also introduce fan recursion, the bar recursion for binary trees, and show that the decidable fan theorem is equivalent to the existence of a fan recursor for every continuous function from {0, 1} N to N with a continuous modulus. The equivalence for bar induction holds over the extensional version of intuitionistic arithmetic in all finite types augmented with the characteristic principles of Gödel's Dialectica interpretation. On the other hand, we show the equivalence for fan theorem without using such extra principles.