arXiv subjects

Andreas Weiermann

Publications and source records attributed to Andreas Weiermann.

At least 19 recordsLinked to original sources

arXiv2026

A Walk with Goodstein and Ackermann

Goodstein's theorem states that a certain sequences based on exponential notation for the natural numbers are always finite. The result is independent of Peano arithmetic and is a prototypical example of a proof of termination by transfinite induction. A variant based instead on the Ackermann function has more recently been proposed by Arai et al., and instead is independent of the more powerful theory ${\sf ATR}_0$. However, this result is contingent on rather elaborate normal forms for natural numbers based on a `sandwiching' procedure. This leaves open both the question of whether the sandwiching procedure can be eliminated while retaining the full strength of the Ackermannian Goodstein principle, and whether other normal forms can lead to non-termination. In this article we settle these questions by showing that {\em any} Goodstein process based on the Ackermann function is terminating, and indeed the sandwiching procedure gives rise to Goodstein principles of maximal length. We thus obtain an equivalent principle which does not involve normal forms at all and immediately implies all Ackermannian Goodstein principles that have been considered. Our techniques provide a new approach to termination proofs, where terms in a sequence do not necessarily decrease in complexity, but instead are majorized by some ``master'' process, already known to be terminating.

math.LO↗

arXiv2026

Goodstein at the Second Threshold: An Independence Result for $ID_2$

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 process based on the Hardy hierarchy. We develop an ordinal notation system utilizing a two-step collapsing procedure, which yields a proof-theoretic ordinal of $\psi_0\psi_1(\varepsilon_{\Omega_2+1})$. By defining $k$-normal forms for natural numbers within this system, we introduce a Goodstein-type process and demonstrate that the theory of non-iterated positive inductive definitions for two operators ($ID_2$) cannot prove its termination. This result establishes a new independence result at the second proof-theoretic threshold, further extending the reach of Goodstein-type principles beyond the Bachmann-Howard level.

math.LO↗

arXiv2026

The Ouroboros Goodstein Principle

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 below $n$. The numbers $e$ and $r$ are then recursively written in $B$-normal form, and finally each base of $B$ is replaced by a corresponding base of some other set $C\subseteq \mathbb{N}$. The resulting process was shown to terminate and to be independent of $\mathsf{KP}$, but the proofs relied on two different ordinal assignments: one monotone but not tight enough to establish independence, and another suitable for independence but not monotone and thus ineffective for proving termination. We introduce a new ordinal assignment that simultaneously yields termination and independence, thereby revealing the `true' ordinals associated with the numbers in the process. This assignment allows us to investigate which restrictions to impose on the process in order for the proof-theoretic strength of its termination to lie between the systems $\mathsf{RCA}_0$, $\mathsf{ACA}_0$, $\mathsf{ATR}_0$ and $\mathsf{KP}$.

math.LO↗

arXiv2025

Ordinal Analysis of Well-Ordering Principles, Well Quasi-Orders Closure Properties, and $\Sigma_n$-Collection Schema

The study of well quasi-orders, wqo, is a cornerstone of combinatorics and within wqo theory Kruskal's theorem plays a crucial role. Extending previous proof-theoretic results, we calculate the $\Pi^1_1$ ordinals of two different versions of labelled Kruskal's theorem: $\forall n \,$ $\mbox{KT}_\ell(n)$ and $\mbox{KT}_{\omega}(n)$; denoting, respectively, all the cases of labelled Kruskal's theorem for trees with an upper bound on the branching degree, and the standard Kruskal's theorem for labelled trees. In order to reach these computations, a key step is to move from Kruskal's theorem, which regards preservation of wqo's, to an equivalent Well-Ordering Principle (WOP), regarding instead preservation of well-orders. Given an ordinal function $g$, WOP$(g)$ amounts to the following principle $\forall X\, [\mbox{WO}(X) \rightarrow \mbox{WO}(g(X))]$, where $WO(X)$ states that ``$X$ is a well-order''. In our case, the two ordinal functions involved are ${g}_{\forall}(X)=\sup_{n}\vartheta(\Omega^n \cdot X)$ and ${g}_{\omega}(X)=\vartheta(\Omega^{\omega}\! \cdot X)$. In addition to the ordinal analysis of Kruskal's theorem and its related WOP, a series of Well Quasi-orders Principles (WQP) is considered. Given a set operation $G$ that preserves the property of being a wqo, its Well Quasi-orders closure Property, WQP$(G)$, is given by the principle $\forall Q\, [Q\, \mbox{wqo} \rightarrow G(Q)\, \mbox{wqo}]$. Conducting this study, unexpected connections with different principles arising from Ramsey and Computational theory, such as RT$^2_{<\infty}$, CAC, ADS, RT$^1_{<\infty}$, turn up. Lastly, extending and combining previous results, we achieve also the ordinal analysis of the collection schema $\mbox{B}\Sigma_n$.

math.LO↗

arXiv2025

Proof-Theoretic Relations between Higman's and Kruskal's theorem, and Independence Results for Tree-like Structures

Higman's lemma and Kruskal's theorem are two of the most celebrated results in the theory of well quasi-orders. In his seminal paper G. Higman obtained what is known as Higman's lemma as a corollary of a more general theorem, dubbed here Higman's theorem. While the lemma deals with finite sequences over a well quasi-order, the theorem is about abstract operations of arbitrary high arity. J.B. Kruskal was fully aware of this broader framework: in his seminal paper, he not only applied Higman's lemma at crucial points of his proof but also followed Higman's proof schema. At the conclusion of the paper, Kruskal noted that Higman's theorem is a special case, restricted to trees of finite degree, of his own tree theorem. Although he provided no formal reduction, he included a glossary translating concepts between the tree and algebraic settings. The equivalence between these versions was later clarified by D. Schmidt and M. Pouzet. In this work, we revisit that equivalence to illuminate the proof-theoretical relationships between the two theorems within the base system $RCA_0$, of reverse mathematics. Moreover, some independence results over first- and second-orders are treated. In particular, tree-like structures, involving either Ackermannian terms or exponential expressions, are studied unveiling well-foundedness properties that are independent from Peano arithmetic and relevant fragments of second-order arithmetic.

math.LO↗

arXiv2025

The fractal Goodstein principle

The original Goodstein process is based on writing numbers in hereditary $b$-exponential normal form: that is, each number $n$ is written in some base $b\geq 2$ as $n=b^ea+r$, with $e$ and $r$ iteratively being written in hereditary $b$-exponential normal form. We define a new process which generalises the original by writing expressions in terms of a hierarchy of bases $B$, instead of a single base $b$. In particular, the `digit' $a$ may itself be written with respect to a smaller base $b'$. We show that this new process always terminates, but termination is independent of Kripke-Platek set theory, or other theories of Bachmann-Howard strength.

math.LO↗

arXiv2024

Induction on Dilators and Bachmann-Howard Fixed Points

One of the most important principles of J.-Y. Girard's $\Pi^1_2$-logic is induction on dilators. In particular, Girard used this principle to construct his famous functor $\Lambda$. He claimed that the totality of $\Lambda$ is equivalent to the set existence axiom of $\Pi^1_1$-comprehension from reverse mathematics. While Girard provided a plausible description of a proof around 1980, it seems that the very technical details have not been worked out to this day. A few years ago, a loosely related approach led to an equivalence between $\Pi^1_1$-comprehension and a certain Bachmann-Howard principle. The present paper closes the circle. We relate the Bachmann-Howard principle to induction on dilators. This allows us to show that $\Pi^1_1$-comprehension is equivalent to the totality of a functor $\mathbb J$ due to P. P\"appinghaus, which can be seen as a streamlined version of $\Lambda$.

math.LO↗

arXiv2023

Optimal Image Transport on Sparse Dictionaries

In this paper, we derive a novel optimal image transport algorithm over sparse dictionaries by taking advantage of Sparse Representation (SR) and Optimal Transport (OT). Concisely, we design a unified optimization framework in which the individual image features (color, textures, styles, etc.) are encoded using sparse representation compactly, and an optimal transport plan is then inferred between two learned dictionaries in accordance with the encoding process. This paradigm gives rise to a simple but effective way for simultaneous image representation and transformation, which is also empirically solvable because of the moderate size of sparse coding and optimal transport sub-problems. We demonstrate its versatility and many benefits to different image-to-image translation tasks, in particular image color transform and artistic style transfer, and show the plausible results for photo-realistic transferred effects.

cs.CV↗

arXiv2022

Fundamental sequences and fast-growing hierarchies for the Bachmann-Howard ordinal

We prove that Buchholz's system of fundamental sequences for the $\vartheta$ function enjoys various regularity conditions, including the Bachmann property. We partially extend these results to variants of the $\vartheta$ function, including a version without addition for countable ordinals. We conclude that the Hardy functions based on these notation systems enjoy natural monotonicity properties and majorize all functions defined by primitive recursion along $\vartheta(\varepsilon_{\Omega+1})$.

math.LO↗

arXiv2021

Arithmetical and Hyperarithmetical Worm Battles

Japaridze's provability logic $GLP$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano aritmetic $(PA)$ and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies $(EWD)$ principle, a natural combinatorial statement independent of $PA$. Recently, Beklemishev and Pakhomov have studied notions of provability corresponding to transfinite modalities in $GLP$. We show that indeed the natural transfinite extension of $GLP$ is sound for this interpretation, and yields independent combinatorial principles for the second order theory $ACA$ of arithmetical comprehension with full induction. We also provide restricted versions of $EWD$ related to the fragments $I\Sigma_n$ of Peano arithmetic. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.

math.LO↗

arXiv2021

Fast Goodstein Walks

We define a variant of the Goodstein process based on fast-growing functions and show that it terminates, but this fact is not provable in Kripke-Platek set theory or other theories of strength the Bachmann-Howard ordinal. We moreover show that this Goodstein process is of maximal length, so that any alternative Goodstein process based on the same fast-growing functions will also terminate.

math.LO↗

arXiv2020

Ackermann and Goodstein go functorial

We present variants of Goodstein's theorem that are equivalent to arithmetical comprehension and to arithmetical transfinite recursion, respectively, over a weak base theory. These variants differ from the usual Goodstein theorem in that they (necessarily) entail the existence of complex infinite objects. As part of our proof, we show that the Veblen hierarchy of normal functions on the ordinals is closely related to an extension of the Ackermann function by direct limits.

math.LO↗

arXiv2020

Monadic second order limit laws for natural well orderings

By combining classical results of Büchi, some elementary Tauberian theorems and some basic tools from logic and combinatorics we show that every ordinal $α$ with $\varepsilon_0\geq α\geq ω^ω$ satisfies a natural monadic second order limit law and that every ordinal $α$ with $ω^ω>α\geq ω$ satisfies a natural monadic second order Cesaro limit law. In both cases we identify as usual $α$ with the class of substructures $\{β:β<α\}$. We work in an additive setting where the norm function $N$ assigns to every ordinal $α$ the number of occurrrences of the symbol $ω$ in its Cantor normal form. This number is the same as the number of edges in the tree which is canonically associated with $α$. For a given $α$ with $ω\leq α\leq \varepsilon_0$ the asymptotic probability of a monadic second order formula $φ$ from the language of linear orders is $\lim_{n\to\infty} \frac{\#\{β<α: Nβ=n\wedge β\models Φ\}}{\#\{β<α: Nβ=n\}}$ if this limit exists. If this limit exists only in the Cesaro sense we speak of the Cesaro asympotic probability of $φ$. Moreover we prove monadic second order limit laws for the ordinal segments below below $Γ_0$ (where the norm function is extended appropriately) and we indicate how this paper's results can be extended to larger ordinal segments and even to certain impredicative ordinal notation systems having notations for uncountable ordinals. We also briefly indicate how to prove the corresponding multiplicative results for which the setting is defined relative to the Matula coding. The results of this paper concerning ordinals not exceeding $\varepsilon_0$ have been obtained partly in joint work with Alan R. Woods.

math.LO↗

arXiv2020

Giant and illusionary giant Goodstein principles

We analyze several natural Goodstein principles which themselves are defined with respect to the Ackermann function and the extended Ackermann function. These Ackermann functions are well established canonical fast growing functions labeled by ordinals not exceeding $\varepsilon_0$. Among the Goodsteinprinciples under consideration, the giant ones, will be proof-theoretically strong (being unprovable in $\mathrm{PA}$ in the Ackermannian case and being unprovable in $\mathrm{ID}_1$ in the extended Ackermannian case) whereas others, the illusionary giant ones, will turn out to be comparatively much much weaker although they look strong at first sight.

math.LO↗

arXiv2020

Intermediate Goodstein principles

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 is unprovable in Peano arithmetic. In this paper we instead consider notations for natural numbers based on the Ackermann function. We define three new Goodstein processes, obtaining new independence results for $ {\sf ACA}_0$, ${\sf ACA}_0'$ and ${\sf ACA}_0^+$, theories of second order arithmetic related to the existence of Turing jumps.

math.LO↗

arXiv2020

A walk with Goodstein

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. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we explore notions of optimality for such notation systems and apply them to the classical Goodstein process, to a weaker variant based on multiplication rather than exponentiation, and to a stronger variant based on the Ackermann function. In particular, we introduce the notion of base-change maximality, and show how it leads to far-reaching extensions of Goodstein's result.

math.LO↗

arXiv2020

Minimal bad sequences are necessary for a uniform Kruskal theorem

The minimal bad sequence argument due to Nash-Williams is a powerful tool in combinatorics with important implications for theoretical computer science. In particular, it yields a very elegant proof of Kruskal's theorem. At the same time, it is known that Kruskal's theorem does not require the full strength of the minimal bad sequence argument. This claim can be made precise in the framework of reverse mathematics, where the existence of minimal bad sequences is equivalent to a principle known as $Π^1_1$-comprehension, which is much stronger than Kruskal's theorem. In the present paper we give a uniform version of Kruskal's theorem by relativizing it to certain transformations of well partial orders. We show that $Π^1_1$-comprehension is equivalent to our uniform Kruskal theorem (over $\mathbf{RCA}_0$ together with the chain-antichain principle). This means that any proof of the uniform Kruskal theorem must entail the existence of minimal bad sequences. As a by-product of our investigation, we obtain uniform proofs of several Kruskal-type independence results.

math.LO↗

arXiv2019

Maximum linearizations of lower sets in $\mathbb{N}^m$ with application to monomial ideals

We compute the type (maximum linearization) of the well partial order of bounded lower sets in $\mathbb{N}^m$, ordered under inclusion, and find it is $\omega^{\omega^{m-1}}$. Moreover we compute the type of the set of all lower sets in $\mathbb{N}^m$, a topic studied by Aschenbrenner and Pong, and find that it is equal to \[ \omega^{\sum_{k=1}^{m} \omega^{m-k}\binom{m}{k-1} }+ 1. \] As a consequence we deduce corresponding bounds on effectively given sequences of monomial ideals in $F[X,Y]$ where $F$ is a field.

math.LO↗