抽象可证性结构中的不动点
Fixed points in abstract provability structures
浏览论文内容
中文总结 AI 辅助
该研究围绕抽象可证性结构（APS）的不动点，明确其度的定义，证明度为2的项存在不动点，建立相关层级并推导G2类结果，还在特定交半格APS中得到更强结论。
中文摘要 AI 辅助
我们研究抽象可证性结构（APS）中的不动点，该结构由Beklemishev和Shamkanov提出，是用于研究哥德尔第二不完全性定理（G2）的序理论框架。对于由可证性操作符$\boldsymbol{\boxtimes}$和可反驳性操作符$\boldsymbol{\boxtimes}$构建的单变量APS项，我们根据项的度（即$\boldsymbol{\boxtimes}$的出现次数）研究其不动点的存在性与唯一性。我们证明所有度为2的项都存在不动点，并在项$\boldsymbol{\boxtimes}\boldsymbol{\boxtimes}^k v$的不动点性质间建立严格层级关系；进一步表明该层级的合适层级可保证所有正度单变量APS项的不动点存在且唯一，还得到若干类G2的不可反驳结果，部分仅依赖度的奇偶性。最后，我们考虑基于交半格的APS，在附加条件下得到更强的不动点结果，且参数化不动点性质蕴含勒布定理的抽象形式。
英文摘要
We study fixed points in abstract provability structures (APSs), which were introduced by Beklemishev and Shamkanov as an order-theoretic framework for studying Gödel's second incompleteness theorem (G2). For one-variable APS terms built from the provability and refutability operations $\Box$ and $\boxtimes$, we investigate the existence and uniqueness of fixed points in terms of their degree. The degree of a term is the number of occurrences of $\boxtimes$. We prove that every term of degree two has a fixed point and establish a strict hierarchy among the fixed-point properties of the terms $\boxtimes\Box^k v$. We further show that suitable levels of this hierarchy guarantee the existence and uniqueness of fixed points for arbitrary one-variable APS terms of positive degree. We also obtain several G2-like non-refutability results, some of which depend only on whether the degree is even or odd. Finally, we consider APSs based on meet-semilattices. Under an additional condition, we obtain stronger fixed-point results and show that a parametrized fixed-point property implies an abstract form of Löb's theorem.
