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 diverge, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we provide a self-contained and modern analysis of Goodstein’s principle, obtaining some variations and improvements. We explore notions of optimality for notation systems and apply them to the classical Goodstein process and to a weaker variant based on multiplication rather than exponentiation. In particular, we introduce the notion of base-change maximality, and show how it leads to far-reaching extensions of Goodstein’s result. We moreover show that by varying the initial base of the Goodstein process, one readily obtains independence results for each of the fragments $\mathsf {I}\Sigma _n$ of Peano arithmetic.

Following the finitist’s rejection of the complete totality of the natural numbers, a finitist language allows only propositional connectives and bounded quantifiers in the formula-construction but not unbounded quantifiers. This is opposed to the currently standard framework, a first-order language. We conduct axiomatic studies on the notion of truth in the framework of finitist arithmetic in which at least smash function $\#$ is available. We propose finitist variants of Tarski ramified truth theories up to rank $\omega $, of Kripke–Feferman truth theory and of Friedman–Sheard truth theory, and show that all of these have the same strength as the finitist arithmetic of one higher level along Grzegorczyk hierarchy. On the other hand, we also show that adding Burgess-style groundedness schema, adjusted to the finitist setting, makes Kripke–Feferman truth theory as strong as primitive recursive arithmetic. Meanwhile, we obtain some basic results on finitist theories of (full and hat) inductive definitions and on the second order axiom of hat inductive definitions for positive operators.

Here, we present a category ${\mathbf {pEff}}$ which can be considered a predicative variant of Hyland's Effective Topos ${{\mathbf {Eff} }}$ for the following reasons. First, its construction is carried in Feferman’s predicative theory of non-iterative fixpoints ${{\widehat {ID_1}}}$ . Second, ${\mathbf {pEff}}$ is a list-arithmetic locally cartesian closed pretopos with a full subcategory ${{\mathbf {pEff}_{set}}}$ of small objects having the same categorical structure which is preserved by the embedding in ${\mathbf {pEff}}$ ; furthermore subobjects in ${{\mathbf {pEff}_{set}}}$ are classified by a non-small object in ${\mathbf {pEff}}$ . Third ${\mathbf {pEff}}$ happens to coincide with the exact completion of the lex category defined as a predicative rendering in ${{\widehat {ID_1}}}$ of the subcategory of ${{\mathbf {Eff} }}$ of recursive functions and it validates the Formal Church’s thesis. Hence pEff turns out to be itself a predicative rendering of a full subcategory of ${{\mathbf {Eff} }}$ .

We describe punctual categoricity in several natural classes, including binary relational structures and mono-unary functional structures. We prove that every punctually categorical structure in a finite unary language is ${\text {PA}}(0')$-categorical, and we show that this upper bound is tight. We also construct an example of a punctually categorical structure whose degree of categoricity is $0''$. We also prove that, with a bit of work, the latter result can be pushed beyond $\Delta ^1_1$, thus showing that punctually categorical structures can possess arbitrarily complex automorphism orbits.

As a consequence, it follows that binary relational structures and unary structures are not universal with respect to primitive recursive interpretations; equivalently, in these classes every rich enough interpretation technique must necessarily involve unbounded existential quantification or infinite disjunction. In contrast, it is well-known that both classes are universal for Turing computability.

We determine the proof-theoretic ordinals (i) of ${\cal C} - {\bf{TI}}[\alpha ]$, the transfinite induction along α, for any hyperarithmetical level ${\cal C}$, in the first order setting and (ii) of any combination of iterated arithmetical comprehension and ${\cal C} - {\bf{TI}}[\alpha ]$ for ${\cal C}\, \equiv \,{\rm{\Pi }}_k^i ,{\rm{\Sigma }}_k^i$ ($i\, = \,0,1$) in the second order setting.