Uniformity of Consistency in Arithmetic and G\"odel's Second Incompleteness Theorem: Ein M\"archen

Abstract

In much discussed work Artemov has recently argued that, for $\mathrm{PA}$, the consistency schema admits a form of uniform verification via selector-proofs, despite the unprovability of the corresponding uniform consistency sentence $\mathrm{Con}(\mathrm{PA})$. In this note, we show that this phenomenon extends to all sufficiently strong, uniformly reflexive arithmetizable theories, including $\mathrm{ZF}$ and many of their extensions: For such theories $T$, there exists a primitive recursive selector which, given a derivation code $d$, extracts a finite fragment $T_d\subseteq T$ containing the non-logical axioms occurring in $d$, uses a reflexivity proof of $\mathrm{Con}(T_d)$, and produces a $T$-proof that $d$ is not a derivation of $0=1$. As a dictum, one obtains a $T$-verification of the consistency of $T$ in a uniform way, despite the fact that it cannot be internalized as the single universal consistency sentence prohibited by G\"odel's Second Incompleteness Theorem. We further analyze this latter discrepancy and locate selector-proofs within the broader framework of provability and reflection.