arxiv: 2605.00266 · v2 · submitted 2026-04-30 · 🧮 math.LO

Recognition: unknown

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

Harald Grobner

Authors on Pith no claims yet

Pith reviewed 2026-05-09 19:27 UTC · model grok-4.3

classification 🧮 math.LO

keywords consistency schemaGödel second incompletenessprimitive recursive selectorarithmetizable theoriesprovability logicreflection principlesuniform verification

0 comments

The pith

For any sufficiently strong arithmetizable theory T, a primitive recursive selector produces proofs for every instance of the consistency schema even though the uniform consistency sentence remains unprovable.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Artemov showed that Peano arithmetic admits selector proofs for each separate instance of the consistency schema, even though the single uniform sentence Con(PA) cannot be proved inside PA. The paper extends this to every sufficiently strong arithmetizable theory T by exhibiting a primitive recursive function that selects a proof for each instance of T's consistency schema. A reader would care because the result supplies a concrete computational form of uniformity that Gödel's second incompleteness theorem forbids at the level of a single internalized sentence. The analysis examines the precise gap between the selector and the uniform sentence and places both inside the larger setting of provability logic and reflection principles. The argument is presented as a soft, constructive version of a classical result due to Pudlák.

Core claim

The paper claims that for every sufficiently strong arithmetizable theory T there exists a primitive recursive selector that, given any numeral n, produces a proof in T of the instance Con_n(T) asserting the consistency of T up to proofs of length n. This selector delivers computational uniformity across all instances without T ever proving the single sentence that quantifies over all n at once. The construction is obtained by extending Artemov's method for PA; the resulting gap between schema and sentence is then located inside the standard framework of provability predicates and reflection.

What carries the argument

The primitive recursive selector function that, for each instance of the consistency schema, outputs a T-proof of that instance.

If this is right

Consistency verification for any such T can be performed by a single computable procedure that works instance by instance.
The impossibility of proving the uniform consistency sentence inside T persists for every sufficiently strong arithmetizable T.
Selector proofs supply a form of uniformity that is strictly weaker than the internalized uniform consistency statement ruled out by Gödel's second theorem.
The same selector technique applies uniformly across the entire class of theories meeting the strength and arithmetizability conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar selectors might exist for other schematic reflection principles once the corresponding uniform sentences are shown unprovable.
The result suggests that automated proof systems could in principle generate consistency proofs on demand without ever needing to prove a single global consistency statement.
One could ask whether the selector itself can be formalized inside a weaker base theory and what that would imply for relative consistency proofs.

Load-bearing premise

The theories T must be sufficiently strong and arithmetizable so that the selector construction known for PA can be carried over without change.

What would settle it

Exhibit one sufficiently strong arithmetizable theory T together with a proof that no primitive recursive function selects T-proofs for all instances of its consistency schema.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This note extends Artemov's selector for PA consistency instances to any strong enough arithmetizable theory T, but the move is a direct recast rather than a deep new construction.

read the letter

The main takeaway is that for any sufficiently strong arithmetizable T, there is a primitive recursive function that outputs a proof of each instance of the consistency schema for T, even though T cannot prove the single uniform consistency sentence. The paper presents this as a generalization of Artemov's PA result and calls it a soft version of Pudlák's earlier work. It does a clean job of spelling out why the selector gives computational uniformity without contradicting Gödel's second theorem, and it situates the selector inside the usual apparatus of provability predicates and reflection principles. That framing is useful for seeing the precise gap between the schema and the uniform sentence. The argument appears to rest on the standard facts that arithmetization works for any such T and that the basic syntactic properties remain provable, so the selector stays primitive recursive once the axiom set is replaced by a general recursive enumeration. No new circularity or non-uniform dependence on T is introduced. The soft spot is that the note is short and the abstract supplies no explicit construction or proof sketch, so it is difficult to judge how much technical work the generalization actually requires. If the details amount to swapping in the general axiom set while preserving the recursion from the PA case, then the advance is incremental and mainly clarificatory. The title suggests the author intends it as a light story rather than a heavy theorem. This is for proof theorists who already know Artemov and the consistency-schema literature. A reader wanting a compact statement of how the selector behaves outside PA will get value from it. The thinking is clear and the engagement with prior results is honest. I would bring it to a reading group as a maybe. I would not cite it in my own work in the next year. It deserves peer review as a short note that sharpens an existing distinction.

Referee Report

1 major / 1 minor

Summary. The manuscript claims that for sufficiently strong arithmetizable theories T, there exists a primitive recursive selector producing proofs of all instances of the associated consistency schema. This extends Artemov's result for PA and is described as a soft version of a classical result of Pudlák, yielding computational uniformity despite the unprovability of the uniform consistency sentence Con(T) by Gödel's second incompleteness theorem. The note's goal is to analyze this gap and situate selector proofs within the broader framework of provability and reflection principles.

Significance. If the existence of the selector is rigorously established, the result would clarify the distinction between schema-wise provability of consistency instances and the non-existence of a uniform consistency sentence, providing a computational perspective on reflection principles that complements Pudlák's work. It would highlight how certain forms of uniformity can be achieved externally without being internalized in the theory itself.

major comments (1)

[Abstract] Abstract: The central claim asserts the existence of a primitive recursive selector for arbitrary sufficiently strong arithmetizable T, but the manuscript provides no construction, proof sketch, or argument showing how the PA selector of Artemov generalizes while remaining primitive recursive once the specific axioms of PA are replaced by the recursive axiom set of a general T. This is load-bearing for the result, as the primitivity and uniformity depend on the details of the arithmetization and the selector function.

minor comments (1)

The manuscript is extremely concise and assumes detailed familiarity with Artemov's construction; adding a short paragraph outlining the key steps of the generalization (even if informal) would make the note more self-contained.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed reading and for identifying the need for greater explicitness in the presentation of the main result. We address the major comment below and will incorporate the suggested clarification in the revised manuscript.

read point-by-point responses

Referee: [Abstract] Abstract: The central claim asserts the existence of a primitive recursive selector for arbitrary sufficiently strong arithmetizable T, but the manuscript provides no construction, proof sketch, or argument showing how the PA selector of Artemov generalizes while remaining primitive recursive once the specific axioms of PA are replaced by the recursive axiom set of a general T. This is load-bearing for the result, as the primitivity and uniformity depend on the details of the arithmetization and the selector function.

Authors: We agree that the manuscript would be strengthened by an explicit outline of the generalization. The current version relies on the reader recognizing that the selector construction for PA (via the standard arithmetization of the provability predicate and the recursive enumeration of axioms) carries over directly once T is assumed to be recursively axiomatizable and sufficiently strong; however, we did not spell out the necessary adjustments to the proof predicate and the bounding functions. In the revised version we will add a short section (approximately one page) that (i) recalls Artemov’s selector for PA, (ii) shows how the same primitive-recursive definition works verbatim when the axiom set is replaced by an arbitrary recursive set A_T, and (iii) verifies that the resulting selector remains primitive recursive by composing the standard primitive-recursive functions for Gödel numbering, substitution, and proof verification with the recursive enumeration of A_T. This addition will make the load-bearing claim fully self-contained while preserving the note’s concise character. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper recasts Artemov's established result for PA (a primitive-recursive selector for consistency-schema instances) to arbitrary sufficiently strong arithmetizable theories T by invoking the standard effectiveness of syntax arithmetization and the preservation of primitivity under replacement of the axiom set. No equation or construction in the note reduces the selector existence claim to a self-definition, a fitted parameter, or a self-citation chain; the cited results of Artemov and Pudlák function as external, independently verifiable inputs. The acknowledged gap with the uniform consistency sentence is explained by Gödel's second incompleteness theorem, an external fact that does not depend on the paper's own constructions. The derivation therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the standard assumption that the theories are arithmetizable and sufficiently strong to interpret basic syntax; no free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption Theories T are arithmetizable and sufficiently strong (able to represent syntax and basic arithmetic)
Invoked to extend the selector construction beyond PA

pith-pipeline@v0.9.0 · 5438 in / 1233 out tokens · 29642 ms · 2026-05-09T19:27:48.247385+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

24 extracted references · 2 canonical work pages

[1]

S. N. Artemov, Explicit provability and constructive semantics, Bulletin of Symbolic Logic 7 (2001), no. 1, 1--36

2001
[2]

S. N. Artemov, The provability of consistency, arXiv:1902.07404, 2019

work page arXiv 1902
[3]

S. N. Artemov, Serial properties, selector proofs and the provability of consistency, Journal of Logic and Computation 35 (2025), no. 3, exae034

2025
[4]

S. N. Artemov, Consistency formula is strictly stronger in PA than PA-consistency, arXiv:2508.20346, 2025

work page arXiv 2025
[5]

D. D. Auerbach, Expressing Consistency: G\"odel's Second Incompleteness Theorem and Intensionality in Metamathematics, Ph.D. thesis, Massachusetts Institute of Technology, 1978

1978
[6]

D. D. Auerbach, Review of Michael Detlefsen, Hilbert's Program: An Essay on Mathematical Instrumentalism, Journal of Symbolic Logic 54 (1989), no. 2, 620--622

1989
[7]

L. D. Beklemishev, Iterated local reflection versus iterated consistency, Annals of Pure and Applied Logic 75 (1995), 25--48

1995
[8]

L. D. Beklemishev, Reflection principles and provability algebras in formal arithmetic, Russian Mathematical Surveys 60 (2005), no. 2, 197--268

2005
[9]

L. D. Beklemishev, Calibrating provability logic: from modal logic to reflection calculus, Russian Mathematical Surveys 65 (2010), no. 5, 857--899

2010
[10]

Detlefsen, On interpreting G\"odel's second theorem, Journal of Philosophical Logic 8 (1979), 297--313

M. Detlefsen, On interpreting G\"odel's second theorem, Journal of Philosophical Logic 8 (1979), 297--313

1979
[11]

Detlefsen, Hilbert's Program: An Essay on Mathematical Instrumentalism, Synthese Library, vol

M. Detlefsen, Hilbert's Program: An Essay on Mathematical Instrumentalism, Synthese Library, vol. 182, D. Reidel, Dordrecht, 1986

1986
[12]

Detlefsen, What does G\"odel's second theorem say?, Philosophia Mathematica 9 (2001), no

M. Detlefsen, What does G\"odel's second theorem say?, Philosophia Mathematica 9 (2001), no. 1, 37--71

2001
[13]

Feferman, Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae 49 (1960), 35--92

S. Feferman, Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae 49 (1960), 35--92

1960
[14]

odel, \"Uber formal unentscheidbare S\

K. G\"odel, \"Uber formal unentscheidbare S\"atze der Principia Mathematica und verwandter Systeme I, Monatshefte f\"ur Mathematik und Physik 38 (1931), 173--198

1931
[15]

H\'ajek and P

P. H\'ajek and P. Pudl\'ak, Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic, Springer, Berlin, 1993

1993
[16]

Hilbert and P

D. Hilbert and P. Bernays, Grundlagen der Mathematik II, Springer, Berlin, 1939

1939
[17]

R. G. Jeroslow, Consistency statements in formal arithmetic, Fundamenta Mathematicae 72 (1971), 17--40

1971
[18]

R. P. Langlands, Automorphic representations, Shimura varieties, and motives. Ein M\"archen, in: Automorphic Forms, Representations and L-Functions, Proc. Sympos. Pure Math., vol. 33, Part 2, Amer. Math. Soc., Providence, RI, 1979, pp. 205--246

1979
[19]

M. H. L\"ob, Solution of a problem of Leon Henkin, Journal of Symbolic Logic 20 (1955), no. 2, 115--118

1955
[20]

Pudl\'ak, On the length of proofs of finitistic consistency statements in first order theories, in J

P. Pudl\'ak, On the length of proofs of finitistic consistency statements in first order theories, in J. B. Paris, A. J. Wilkie and G. M. Wilmers (eds.), Logic Colloquium '84, North-Holland, Amsterdam, 1986, pp. 165--196

1986
[21]

M. D. Resnik, On the philosophical significance of consistency proofs, Journal of Philosophical Logic 3 (1974), no. 1/2, 133--147

1974
[22]

Smory\'nski, Self-Reference and Modal Logic, Universitext, Springer-Verlag, New York, 1985

C. Smory\'nski, Self-Reference and Modal Logic, Universitext, Springer-Verlag, New York, 1985

1985
[23]

Steiner, Review of Michael Detlefsen, Hilbert's Program: An Essay on Mathematical Instrumentalism, Journal of Philosophy 88 (1991), no

M. Steiner, Review of Michael Detlefsen, Hilbert's Program: An Essay on Mathematical Instrumentalism, Journal of Philosophy 88 (1991), no. 6, 331--336

1991
[24]

Visser, Provability logic, in D

A. Visser, Provability logic, in D. M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, 2nd ed., vol. 4, Kluwer, Dordrecht, 2001, 1--107

2001