On a Theorem by Bezboruah & Shepherdson
Pith reviewed 2026-05-15 15:34 UTC · model grok-4.3
The pith
PA^- does not prove the consistency of any theory under the stated conditions.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
Bezboruah and Shepherdson showed that PA^- does not prove Con(T) whenever T meets the relevant conditions, such as being consistent and satisfying the syntactic requirements spelled out in the theorem. Visser defends this claim against Kreisel's argument that it is meaningless, compares it to Pudlák's related extension of Gödel's second theorem, and gives a new proof that uses a sequence-coding construction drawn from an insight of Nielsen and Markov.
What carries the argument
The Bezboruah-Shepherdson theorem, which asserts that PA^- proves no consistency statement Con(T) for any theory T meeting the paper's conditions on consistency and syntactic closure.
If this is right
- Even the weakest standard fragment of arithmetic is too weak to prove its own consistency.
- Consistency statements for stronger theories cannot be established inside PA^-.
- Pudlák's strengthening of the second incompleteness theorem operates at a higher level than this result.
- A sequence-coding method based on Nielsen and Markov suffices to carry out the proof without extra assumptions.
Where Pith is reading between the lines
- Analogous results may hold for other minimal arithmetics such as Robinson's Q.
- The choice of axioms needed to prove consistency statements must be made carefully above the level of PA^-.
- The result raises the question of exactly which additional axioms first allow a theory to prove consistency of basic arithmetic.
Load-bearing premise
The theories T under discussion are consistent and satisfy the formal conditions that allow the theorem to apply, and Kreisel's objection can be set aside.
What would settle it
A formal derivation inside PA^- of Con(T) for some specific theory T that meets every condition listed in the paper would refute the central claim.
read the original abstract
We discuss an incompleteness result proven by Bezboruah and Shepherdson. This result tells us that the weak theory ${\sf PA}^-$ does not prove the consistency of any theory (under certain assumptions explained in the paper). Kreisel argued that such a result is not meaningful. We discuss Kreisel's objection and conclude that his argument does not hold water. We compare Pudl\'ak's extension of the Second Incompleteness Theorem with the Bezboruah-Sheperdson Theorem. Finally, we reprove the Bezboruah-Sheperdson Theorem for a sequence coding based on an insight of Nielsen and Markov.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper discusses the Bezboruah-Shepherdson incompleteness theorem stating that the weak theory PA^- does not prove the consistency of any theory (under assumptions detailed in the manuscript). It addresses and rejects Kreisel's objection to the result's meaningfulness, compares the theorem to Pudlák's extension of the second incompleteness theorem, and provides an independent reproof of the Bezboruah-Shepherdson result using a sequence coding based on Nielsen and Markov.
Significance. If the reproof is fully formalizable in PA^-, the result would clarify the boundaries of provability of consistency statements in very weak arithmetical theories, reinforcing that even minimal base theories like PA^- lack the resources for self-verification of consistency. The explicit treatment of Kreisel's objection and the comparison with Pudlák add contextual value to the literature on incompleteness in subsystems of arithmetic.
major comments (2)
- [reproof section] The reproof section (using Nielsen-Markov sequence coding) does not explicitly verify that the definitions of sequence length, concatenation, and decoding functions, along with their basic properties (e.g., existence of codes for arbitrary finite sequences), are provable from the axioms of PA^- alone. PA^- lacks full induction, so any tacit use of collection or induction in these lemmas would render the formalization invalid and undermine the central claim that PA^- fails to prove consistency.
- [comparison with Pudlák] The assumptions under which PA^- fails to prove consistency (mentioned in the abstract and reader's strongest claim) are not stated with sufficient precision in the comparison to Pudlák's theorem; without an explicit list of these assumptions (e.g., regarding the form of the consistency statement or the theory being consistent), it is unclear whether the Bezboruah-Shepherdson result is strictly stronger or merely a special case.
minor comments (2)
- [abstract] Inconsistent spelling of the name 'Shepherdson' (appears as Shepherdson, Sheperdson in the abstract).
- [introduction] The manuscript should include a brief explicit statement of the axioms of PA^- at the outset to make the base theory clear to readers unfamiliar with the exact formulation used.
Simulated Author's Rebuttal
We thank the referee for the careful reading and valuable suggestions, which will help improve the clarity and rigor of the manuscript. We address the two major comments point by point below.
read point-by-point responses
-
Referee: [reproof section] The reproof section (using Nielsen-Markov sequence coding) does not explicitly verify that the definitions of sequence length, concatenation, and decoding functions, along with their basic properties (e.g., existence of codes for arbitrary finite sequences), are provable from the axioms of PA^- alone. PA^- lacks full induction, so any tacit use of collection or induction in these lemmas would render the formalization invalid and undermine the central claim that PA^- fails to prove consistency.
Authors: We agree that the reproof would be strengthened by an explicit verification that the relevant definitions and lemmas are provable in PA^- without invoking induction or collection beyond the theory's resources. The Nielsen-Markov coding was selected precisely because its basic properties (length, concatenation, decoding, and existence of codes for finite sequences) can be established using only the axioms of PA^-. In the revised version we will add a short subsection that states and proves these lemmas directly from the PA^- axioms, thereby confirming that the entire argument remains within the theory. revision: yes
-
Referee: [comparison with Pudlák] The assumptions under which PA^- fails to prove consistency (mentioned in the abstract and reader's strongest claim) are not stated with sufficient precision in the comparison to Pudlák's theorem; without an explicit list of these assumptions (e.g., regarding the form of the consistency statement or the theory being consistent), it is unclear whether the Bezboruah-Shepherdson result is strictly stronger or merely a special case.
Authors: We accept that the comparison section would benefit from a more precise enumeration of the assumptions. The Bezboruah-Shepherdson result concerns the unprovability in PA^- of Con(T) for any theory T that is consistent and extends PA^- (with the consistency statement formalized in the usual way). In the revision we will insert an explicit list of these assumptions immediately before the comparison with Pudlák's theorem and briefly indicate how the result relates to (but is not subsumed by) Pudlák's extension of the second incompleteness theorem. revision: yes
Circularity Check
Minor self-citation in historical discussion; central reproof uses external Nielsen-Markov coding without definitional reduction
full rationale
The paper's core claim is an incompleteness result for PA^- reproved via a sequence coding drawn from Nielsen and Markov. No equation or lemma is shown to reduce by construction to its own inputs or to a fitted parameter renamed as prediction. The discussion of Bezboruah-Shepherdson, Pudlák, and Kreisel consists of standard scholarly citation rather than load-bearing self-citation chains that would force the result. The derivation therefore remains self-contained against external benchmarks and receives only the minimal score for ordinary prior-work references.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.