论佐恩引理的计算内容
计算机科学中的逻辑
2020-04-29 v2 逻辑
摘要
我们给出佐恩引理（Zorn's lemma）一个抽象实例的计算解释，该实例在全有限类型算术语言中表述为良基性原理。这通过哥德尔（Gödel）的函数解释实现，并需要引入一种新颖的、基于非良基偏序的递归形式；我们借助域论技术证明了该递归在全连续函数模型中的存在性。我们表明，序列字典序上开归纳的函数解释实化器可作为我们主要结论的一个简单应用得出。
引用
@article{arxiv.2001.03540,
title = {On the computational content of Zorn's lemma},
author = {Thomas Powell},
journal= {arXiv preprint arXiv:2001.03540},
year = {2020}
}