Fixed points in abstract provability structures

Abstract

We study fixed points in abstract provability structures (APSs), which were introduced by Beklemishev and Shamkanov as an order-theoretic framework for studying G\"odel'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\"ob's theorem.