关于ZF的经典可实现性模型的结构
计算机科学中的逻辑
2018-03-20 v1 逻辑
摘要
“经典可实现性”技术是“力迫”方法的扩展；它允许将证明与程序之间的Curry-Howard对应扩展到Zermelo-Fraenkel集合论，并构建ZF的新模型，称为“可实现性模型”。这些模型的结构通常比“力迫模型”的特殊情况复杂得多。我们在此证明，任何可实现性模型的可构造集类都是基础模型的可构造集的初等扩张（在力迫情况下这是一个平凡事实，因为这些类是相同的）。由此可知，Shoenfield绝对性定理适用于可实现性模型。
引用
@article{arxiv.1408.1868,
title = {On the structure of classical realizability models of ZF},
author = {Jean-Louis Krivine},
journal= {arXiv preprint arXiv:1408.1868},
year = {2018}
}
备注
17 pages