良序原理与$\Pi^1_4$-语句：一项先导研究
逻辑
2020-06-23 v1
摘要
在先前的工作中，作者证明了沿的-归纳等价于“每个序数上的正规函数都有不动点”这一陈述的适当形式化。更准确地说，这是针对用J.-Y. Girard的膨胀子表示正规函数证明的，膨胀子是良序的特别一致的变换。本文在下一个类型层面上展开工作，考虑膨胀子的一致变换，称为-ptykes。我们证明了沿的-归纳等价于所有满足特定正规性条件的-ptykes的不动点存在性。除了这一具体结果外，本文还为用良序原理分析进一步的-语句铺平了道路。
引用
@article{arxiv.2006.12111,
title = {Well ordering principles and $\Pi^1_4$-statements: a pilot study},
author = {Anton Freund},
journal= {arXiv preprint arXiv:2006.12111},
year = {2020}
}