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

TL;DR

This paper explores how strong arithmetizable theories can uniformly verify consistency schemas through selector proofs, revealing a computational uniformity that cannot be internalized as G"odel's second incompleteness theorem.

Contribution

It extends Artemov's results to all sufficiently strong theories, showing the existence of primitive recursive selectors producing proofs of all consistency schema instances.

Findings

Selector proofs exist for all instances of the consistency schema in strong theories.

This uniform verification does not translate into an internalized uniform consistency sentence.

The work connects selector proofs to broader provability and reflection frameworks.

Abstract

In much discussed work Artemov has recently shown 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 recast that this phenomenon extends to all sufficiently strong arithmetizable theories: For such theories $T$, there exists a primitive recursive selector producing proofs of all instances of the associated consistency schema. This results -- a soft version of a classical result of Pudl\'ak -- yields a form of computational uniformity, despite the fact that it cannot be internalized as the uniform consistency sentence of G\"odel's Second Incompleteness Theorem. Our main goal is to analyze this gap and to locate selector proofs within the broader framework of provability and reflection.