Related papers: Goodstein revisited
Goodstein sequences are numerical sequences in which a natural number m, expressed as the complete normal form to a given base a, is modified by increasing the value of the base a by one unit and subtracting one unit from the resulting…
The classical Goodstein process, defined via hereditary base-$k$ exponential normal form, is a well-known example of a principle unprovable in Peano Arithmetic. In this paper, we generalize this framework by constructing a new Goodstein…
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…
Goodstein's argument is essentially that the hereditary representation m_{[b]} of any given natural number m in the natural number base b can be mirrored in Cantor Arithmetic, and used to well-define a finite decreasing sequence of…
In arXiv:2508.14768, a variant of Goodstein's original process was recently introduced which, given a set $B\subseteq \mathbb{N}$ of bases, writes each $n\in\mathbb{N}$ in $B$-normal form, namely $n=b^ea+r$, where $b\in B$ the greatest base…
In the late 1980s, Abrusci, Girard and van de Wiele defined a variant of Goodstein sequences: the so-called inverse Goodstein sequence. In their work, they show that it terminates precisely at the Bachmann-Howard ordinal. This reveals that…
Goodstein's principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to grow very quickly, but eventually decrease to zero.…
Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on G\"{o}del's reformulation, and including additional details…
The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that…
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…
In 2010, Vladimir Voevodsky gave a lecture on "What If Current Foundations of Mathematics Are Inconsistent?" Among other things he said that he was seriously suspicious that an inconsistency in PA (first-order Peano arithmetic) might…
The original Goodstein process proceeds by writing natural numbers in nested exponential $k$-normal form, then successively raising the base to $k+1$ and subtracting one from the end result. Such sequences always reach zero, but this fact…
In the Handbook of Mathematical Logic, the Paris-Harrington variant of Ramsey's theorem is celebrated as the first result of a long 'search' for a purely mathematical incompleteness result in first-order arithmetic. This paper questions the…
Feferman proved in 1962 that any arithmetical theorem is a consequence of a suitable transfinite iteration of full uniform reflection of $\mathsf{PA}$. This result is commonly known as Feferman's completeness theorem. The purpose of this…
Building on Buchholz' assignment for ordinals below Bachmann-Howard ordinal, see Buchholz 2003, we introduce systems of fundamental sequences for two kinds of relativized $\vartheta$-function-based notation systems of strength…
The use of ordinal patterns (OPs) for analyzing the dependence structure of univariate and continuously distributed processes has gained popularity in recent years. This research goes one step further and considers the transcripts being…
In this note let us give two remarks on proof-theory of PA. First a derivability relation is introduced to bound witnesses for provable $\Sigma_{1}$-formulas in PA. Second Paris-Harrington's proof for their independence result is…
Natural numbers are represented by Grzegorczyk functions. The representation is implicit in the technique of H. Friedman. An iterated base-shift in the representation with subtracting 1 yields a sequence, Grzegorczyk sequence. It is shown…
For Hilbert, the consistency of a formal theory T is an infinite series of statements "D is free of contradictions" for each derivation D and a consistency proof is i) an operation that, given D, yields a proof that D is free of…
In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's Programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert's epsilon-substitution method. There was, however,…