An Escape from Vardanyan's Theorem

TL;DR

This paper introduces and proves the completeness of a new first-order provability logic system, $ extsf{QRC}_1$, using Kripke models, providing insights into the structure of provability logics within arithmetic theories.

Contribution

The authors generalize Kripke soundness and completeness proofs for $ extsf{QRC}_1$, establishing its arithmetical semantics and its relation to existing provability logics.

Findings

$ extsf{QRC}_1$ is complete with respect to arithmetical semantics.

$ extsf{QRC}_1$ is the strictly positive fragment of $ extsf{QGL}$.

$ extsf{QRC}_1$ is a fragment of $ extsf{QPL}( extsf{PA})$.

Abstract

Vardanyan's Theorems state that $\mathsf{QPL}(\mathsf{PA})$ - the quantified provability logic of Peano Arithmetic - is $\Pi^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf{QRC}_1$ was previously introduced by the authors as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf{QRC}_1$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf{QRC}_1$ is the strictly positive fragment of $\mathsf{QGL}$ and a fragment of $\mathsf{QPL}(\mathsf{PA})$.