用邻域函数表示 $\mathrm{HA}^{\omega}$ 的可定义函数

Brouwer（1927）声称，从Baire空间到自然数的每个函数都由定义域容许杆归纳的邻域函数所诱导。我们证明，对于该系统的可定义函数，Brouwer的断言在全体有限类型的Heyting算术（$\mathrm{HA}^{\omega}$）中是可证的。该证明不依赖于规范化或序数分析等精细的证明论方法。相反，我们在 $\mathrm{HA}^{\omega}$ 中内化了Escardó（2013）关于Gödel系统T的对话树解释。该解释确定了项的一种语法翻译，从而由具有所需性质的 $\mathrm{HA}^{\omega}$ 闭项得到邻域函数。作为此结果的应用，我们证明了 $\mathrm{HA}^{\omega}$ 的一些熟知性质：从 $\mathbb{N}^{\mathbb{N}}$ 到 $\mathbb{N}$ 的可定义函数在Cantor空间上的均匀连续性；在杆归纳规则下的封闭性；以及具有可定义停止函数的最低类型的杆递归的封闭性。