系统T中对经典分析Sigma-2片段的一种解释
逻辑
2015-01-30 v3 计算机科学中的逻辑
摘要
我们证明，仅使用Gödel的系统T即可为经典分析的 -片段定义一种可实现性解释。这补充了Schwichtenberg关于类型0和1上bar递归的先前结果，展示了如何完全避免使用bar递归。我们的结果通过对系统T进行保守扩充来证明，扩充中引入了源自Danvy和Filinski编程语言理论的可组合续延算子。因此，分析的该片段本质上是构造性的，即使在存在完整选择公理模式的情况下也是如此：尽管它强大到足以反驳形式算术版本的Church论题，弱Church规则对其依然成立。
引用
@article{arxiv.1301.5089,
title = {An interpretation of the Sigma-2 fragment of classical Analysis in System T},
author = {Danko Ilik},
journal= {arXiv preprint arXiv:1301.5089},
year = {2015}
}