Generalizing Goodstein's theorem and Cichon's independence proof

Gunnar Wilken

arxiv: 2511.04526 · v3 · submitted 2025-11-06 · 🧮 math.LO

Generalizing Goodstein's theorem and Cichon's independence proof

Gunnar Wilken This is my paper

Pith reviewed 2026-05-17 23:50 UTC · model grok-4.3

classification 🧮 math.LO

keywords Goodstein's theoremCichon's independence proofΠ¹₁-CA₀ordinal notation systemsBachmann propertyproof theoryindependence resultssecond-order arithmetic

0 comments

The pith

Goodstein's theorem and Cichon's independence proof generalize to Π¹₁-CA₀.

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

The paper generalizes Goodstein's theorem on the termination of certain numerical sequences and Cichon's related independence result to the subsystem Π¹₁-CA₀ of second-order arithmetic. It achieves this by applying results on ordinal notation systems from earlier work. A reader would care because these statements are true but unprovable in weaker systems like Peano arithmetic, so the generalization reveals how much logical strength is needed to prove basic combinatorial facts about numbers.

Core claim

Using results from prior work, we generalize Goodstein's theorem and Cichon's independence proof to Π¹₁-CA₀. The method works for stronger notation systems that provide unique terms for ordinals and enjoy the Bachmann property.

What carries the argument

Ordinal notation systems that assign unique terms to ordinals and satisfy the Bachmann property, enabling the translation of sequence termination into ordinal descent.

Load-bearing premise

The notation systems used provide unique terms for ordinals and enjoy the Bachmann property.

What would settle it

A model of Π¹₁-CA₀ containing a generalized Goodstein sequence that never reaches zero would falsify the claimed generalization.

read the original abstract

We generalize Goodstein's theorem (Goodstein 1944) and Cichon's independence proof (Cichon 1983) to $\Pi^1_1-\mathrm{CA}_0$ using results from (Wilken 2026). The method is generalizable to stronger notation systems that provide unique terms for ordinals and enjoy Bachmann property.

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 generalizes Goodstein termination and Cichon's independence to Π¹₁-CA₀ by plugging in the author's 2026 notation systems with unique terms and Bachmann property, plus notes the method carries to stronger systems.

read the letter

The main thing here is that the paper lifts the Goodstein termination argument and Cichon's independence result up to Π¹₁-CA₀. It does this by using notation systems from the 2026 work that assign unique terms to ordinals and satisfy the Bachmann property, then observes that the same steps work in any stronger system with those two features. That portability is the clearest addition over the 1944 and 1983 originals, which were tied to specific weaker ordinals. It gives a cleaner picture of where these combinatorial statements sit in the hierarchy of second-order arithmetic subsystems. The argument stays direct once the two properties are granted, so the extension itself looks mechanical rather than inventive. The soft spot is the dependence on the prior results. The abstract stays high-level and does not show the concrete instantiation or any fresh checks for Π¹₁-CA₀, so the full paper has to demonstrate that the application requires no extra work beyond what is already verified. If that is laid out plainly, the concern stays minor; if readers still have to reconstruct the steps, it weakens the presentation. This is aimed at people already working on ordinal notations, reverse mathematics, or the proof-theoretic strength of Goodstein-like statements. A reader tracking these exact lines of work would find the modular claim useful for further extensions. It deserves a serious referee to verify the details against the 2026 paper and confirm the portability holds without hidden adjustments.

Referee Report

2 major / 2 minor

Summary. The manuscript claims to generalize Goodstein's theorem (Goodstein 1944) and Cichon's independence proof (Cichon 1983) to the base theory Π¹₁-CA₀. This is done by instantiating the standard termination argument inside an ordinal notation system taken from Wilken 2026, which is asserted to supply unique terms for ordinals and to satisfy the Bachmann property. The authors state that the same method extends immediately to any stronger system possessing the same two properties.

Significance. If the application of the Wilken 2026 notation system is carried out correctly, the result would supply a uniform template for lifting Goodstein-type termination and independence statements to theories whose proof-theoretic ordinals lie above those of PA. The approach credits the prior work for the required ordinal assignments and property verifications rather than re-deriving them.

major comments (2)

[Abstract] Abstract and opening paragraph: the generalization to Π¹₁-CA₀ is asserted by direct appeal to the unique-term and Bachmann-property results of Wilken 2026, yet no explicit reference to a specific lemma or theorem number from that work is supplied, nor is any step of the termination argument reproduced. This leaves the central claim uncheckable from the manuscript alone.
[Main result] The manuscript treats the Bachmann property and uniqueness of terms as black-box inputs sufficient to carry the Goodstein termination argument into Π¹₁-CA₀. If those properties are not re-verified or at least located by precise citation for the particular notation system employed here, the independence statement reduces to a restatement of the cited prior result.

minor comments (2)

A complete bibliographic entry for Wilken 2026 (including arXiv identifier or journal details) should appear in the reference list.
[Abstract] The abstract uses the parenthetical citation '(Wilken 2026)' without a corresponding entry; this should be standardized to the journal's citation style.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting issues of verifiability in the presentation. We address the major comments below and will revise the manuscript accordingly to strengthen the exposition while preserving the core contribution.

read point-by-point responses

Referee: [Abstract] Abstract and opening paragraph: the generalization to Π¹₁-CA₀ is asserted by direct appeal to the unique-term and Bachmann-property results of Wilken 2026, yet no explicit reference to a specific lemma or theorem number from that work is supplied, nor is any step of the termination argument reproduced. This leaves the central claim uncheckable from the manuscript alone.

Authors: We agree that the abstract and opening paragraph would be improved by more precise citations. In the revised version we will explicitly reference the specific lemmas or theorems in Wilken (2026) that establish the unique-term property and the Bachmann property for the ordinal notation system employed. We will also include a concise outline of the standard termination argument and how the two properties are instantiated within it, so that the central claim becomes verifiable from the manuscript without requiring the reader to reconstruct the details from the cited source alone. revision: yes
Referee: [Main result] The manuscript treats the Bachmann property and uniqueness of terms as black-box inputs sufficient to carry the Goodstein termination argument into Π¹₁-CA₀. If those properties are not re-verified or at least located by precise citation for the particular notation system employed here, the independence statement reduces to a restatement of the cited prior result.

Authors: The manuscript's contribution is the observation that the standard Goodstein termination argument lifts directly once a notation system supplies unique terms and satisfies the Bachmann property, together with the observation that this template applies uniformly to any stronger system possessing those two features. We do not re-verify the ordinal-theoretic properties, as that verification is the content of Wilken (2026). To meet the referee's concern we will add precise citations to the relevant results in that paper for the specific notation system used here. This keeps the independence statement as an application rather than a restatement, while making the dependence on prior work fully transparent. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper generalizes Goodstein's theorem and Cichon's independence proof to Π¹₁-CA₀ by instantiating the standard termination argument inside a notation system whose unique terms and Bachmann property are taken from the cited prior work (Wilken 2026). This self-citation supplies the required assumptions about the notation system but does not make the generalization itself equivalent to those inputs by construction; the new content is the explicit portability of the argument to the stronger base theory Π¹₁-CA₀ and the statement that the same method applies to any system meeting the two conditions. No equation or step in the derivation reduces the claimed result to a renaming, fit, or self-referential definition of the target statement.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard background results in ordinal notation theory and the properties asserted for the notation systems in the cited Wilken 2026 paper.

axioms (1)

domain assumption Notation systems provide unique terms for ordinals and enjoy the Bachmann property.
Invoked as the condition under which the method generalizes, per the abstract statement.

pith-pipeline@v0.9.0 · 5336 in / 1296 out tokens · 28236 ms · 2026-05-17T23:50:40.722925+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean equivNat, embed_injective unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We generalize Goodstein’s theorem and Cichon’s independence proof to Π¹₁-CA₀ using results from Wilken [3]. The method is generalizable to stronger notation systems that provide or enable unique terms for ordinals and enjoy Bachmann property.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

[1]

W.\ Buchholz and K.\ Sch\"utte:

work page
[2]

W.\ Buchholz, A.\ Cichon, A.\ Weiermann:

work page
[3]

T.\ J.\ Carlson and G.\ Wilken:

work page
[4]

Proceedings of the American Mathematical Society 87 (1983) 704--706

E.\ A.\ Cichon: A short proof of two recently discovered independence results using recursion theoretic methods. Proceedings of the American Mathematical Society 87 (1983) 704--706

work page 1983
[5]

D.\ Fern\'andez-Duque and A.\ Weiermann:

work page
[6]

H.\ Friedman, N.\ Robertson, and P.\ Seymour:

work page
[7]

The Journal of Symbolic Logic 9 (1944) 33--41

R.\ L.\ Goodstein: On the restricted ordinal theorem. The Journal of Symbolic Logic 9 (1944) 33--41

work page 1944
[8]

J.\ Roger Hindley und Jonathan P.\ Seldin:

work page
[9]

G.\ J\"ager and W.\ Pohlers:

work page
[10]

L.\ Kirby and J.\ Paris:

work page
[11]

J.\ Paris and L.\ Harrington:

work page
[12]

W.\ Pohlers and J.-C.\ Stegert:

work page
[13]

M.\ Rathjen and A.\ Weiermann:

work page
[14]

K.\ Sch\"utte und S.\ G.\ Simpson:

work page
[15]

A.\ Weiermann and G.\ Wilken:

work page
[16]

G.\ Wilken and A.\ Weiermann:

work page
[17]

Annals of Pure and Applied Logic 177 (2026) 1--43

G.\ Wilken: Fundamental sequences based on localization. Annals of Pure and Applied Logic 177 (2026) 1--43

work page 2026

[1] [1]

W.\ Buchholz and K.\ Sch\"utte:

work page

[2] [2]

W.\ Buchholz, A.\ Cichon, A.\ Weiermann:

work page

[3] [3]

T.\ J.\ Carlson and G.\ Wilken:

work page

[4] [4]

Proceedings of the American Mathematical Society 87 (1983) 704--706

E.\ A.\ Cichon: A short proof of two recently discovered independence results using recursion theoretic methods. Proceedings of the American Mathematical Society 87 (1983) 704--706

work page 1983

[5] [5]

D.\ Fern\'andez-Duque and A.\ Weiermann:

work page

[6] [6]

H.\ Friedman, N.\ Robertson, and P.\ Seymour:

work page

[7] [7]

The Journal of Symbolic Logic 9 (1944) 33--41

R.\ L.\ Goodstein: On the restricted ordinal theorem. The Journal of Symbolic Logic 9 (1944) 33--41

work page 1944

[8] [8]

J.\ Roger Hindley und Jonathan P.\ Seldin:

work page

[9] [9]

G.\ J\"ager and W.\ Pohlers:

work page

[10] [10]

L.\ Kirby and J.\ Paris:

work page

[11] [11]

J.\ Paris and L.\ Harrington:

work page

[12] [12]

W.\ Pohlers and J.-C.\ Stegert:

work page

[13] [13]

M.\ Rathjen and A.\ Weiermann:

work page

[14] [14]

K.\ Sch\"utte und S.\ G.\ Simpson:

work page

[15] [15]

A.\ Weiermann and G.\ Wilken:

work page

[16] [16]

G.\ Wilken and A.\ Weiermann:

work page

[17] [17]

Annals of Pure and Applied Logic 177 (2026) 1--43

G.\ Wilken: Fundamental sequences based on localization. Annals of Pure and Applied Logic 177 (2026) 1--43

work page 2026