重访不动点关于直觉主义算术的保守性
逻辑
2021-12-22 v3
摘要
本文给出了严格正不动点的直觉主义理论 关于 Heyting 算术（HA）的保守性的一个新证明，该结论最初由 Arai（2011）在完全一般性下证明。该证明将 嵌入到 Beeson 偏项逻辑上的相应理论中，然后使用两个连续解释：该理论到由几乎负不动点生成的子理论的可实现性解释，以及利用几乎负公式的满足谓词层次到带偏项的 Heyting 算术的直接解释。最后应用 van den Berg 与 van Slooten（2018）的结果，即带偏项的 Heyting 算术加上算术公式的自可实现性模式关于 HA 是保守的。
引用
@article{arxiv.2110.08240,
title = {Revisiting the conservativity of fixpoints over intuitionistic arithmetic},
author = {Mattias Granberg Olsson and Graham E. Leigh},
journal= {arXiv preprint arXiv:2110.08240},
year = {2021}
}
备注
24 pages, 0 figures; v2: added and emphasized references in section 1, added reference in section 5.2; v3: corrected notational error in theorem 4.9 and removed unused notations in definition 4.7, corrected some typos