论文标题
关于Zorn引理的计算内容
On the computational content of Zorn's lemma
论文作者
论文摘要
我们对Zorn的引理的抽象实例进行了计算解释，以所有有限类型的算术语言中的一种良好的原理。这是通过Gödel的功能解释来实现的，需要在非曲折的部分顺序上引入一种新型的递归形式，其在总连续功能模型中的存在是使用域理论技术证明的。我们表明，在序列上对词素订购的开放式归纳的功能解释的实现者是我们主要结果的简单应用。
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven using domain theoretic techniques. We show that a realizer for the functional interpretation of open induction over the lexicographic ordering on sequences follows as a simple application of our main results.
