Uniformity of Consistency in Arithmetic and Gödel's Second Incompleteness Theorem: Ein Märchen

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ödel's Second Incompleteness Theorem. We further analyze this latter discrepancy and locate selector-proofs within the broader framework of provability and reflection.

Substantially revised version. The paper now incorporates the finite-fragment consistency step in the analysis of selector-proofs and proves a corresponding selector-proof theorem for uniformly reflexive theories. Sections 2 and 3 have been rewritten, with examples including extensions of PA and ZF and a revised discussion of Gödel's 2. UVS, reflection and Hilbert's program