arXiv subjects

Anton Freund

Publications and source records attributed to Anton Freund.

At least 19 recordsLinked to original sources

arXiv2026

Avoiding logical strength in real analysis

In reverse mathematics, real numbers are traditionally represented by Cauchy sequences with a given rate of convergence. We work without rates and speak of slow Cauchy sequences. It turns out that almost all one-dimensional real analysis from the reverse mathematics book by Simpson can then be developed in theories that are conservative over $\mathsf{RCA}_0$. Specifically, we obtain clusters of equivalences with the infinite pigeonhole principle and the strong cohesive principle. The second cluster includes results like the Bolzano-Weierstrass and Arzel\`a-Ascoli theorems, which are traditionally associated with the stronger axiom of arithmetical comprehension, but also the Heine-Borel theorem, which is normally separated from these principles. This suggests two things: In elementary analysis, one can avoid logical strength to an extent that the traditional picture seems to forbid. And the division of the so-called reverse mathematics zoo into analytical and combinatorial principles may be less rigid than previously assumed.

math.LO↗

arXiv2026

Effective rates for continuous-time quasi-Fej\'er monotone dynamical systems

We provide quantitative convergence results for continuous-time dynamical systems in metric spaces that satisfy a continuous-time analog of quasi-Fej\'er monotonicity. More precisely, we provide a (strong) convergence result for such dynamical systems over compact metric spaces which is quantitatively outfitted with a continuous-time rate of metastability, which moreover can be explicitly and effectively constructed in a very uniform way, only depending on a few moduli representing quantitative witnesses to key properties of the dynamical system and a measure for the compactness of the space. We further show how this convergence result can be extended to non-compact spaces under a regularity assumption of the associated problem, where moreover rates of convergence can then be explicitly constructed which are similarly uniform. In both cases, already the associated ``infinitary'' convergence result is qualitatively novel in its present generality. Beyond this abstract quantitative theory for such dynamical systems, we motivate how the presently studied continuous-time variant of quasi-Fej\'er monotonicity naturally occurs as a unifying property of many dynamical systems and differential equations and inclusions, and in that way can be used to provide a comprehensive quantitative theory for many such dynamical systems. We illustrate this with three case studies for both classical first- and second-order dynamical systems in Hilbert spaces as well as (generalized) gradient flows and associated semigroups in nonlinear Hadamard spaces.

math.OC↗

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↗

arXiv2024

More conservativity for weak K\H{o}nig's lemma

We prove conservativity results for weak K\H{o}nig's lemma that extend the celebrated result of Harrington (for $\Pi^1_1$-statements) and are somewhat orthogonal to the extension by Simpson, Tanaka and Yamazaki (for statements of the form $\forall X\exists!Y\psi$ with arithmetical $\psi$). In particular, we show that $\mathsf{WKL}_0$ is conservative over $\mathsf{RCA}_0$ for well-ordering principles. We also show that compactness (which characterizes weak K\H{o}nig's lemma) is dispensable for certain results about continuous functions with isolated singularities.

math.LO↗

arXiv2024

Fra\"iss\'e's conjecture, partial impredicativity and well-ordering principles, part I

Fra\"iss\'e's conjecture (proved by Laver) is implied by the $\Pi^1_1$-comprehension axiom of reverse mathematics, as shown by Montalb\'an. The implication must be strict for reasons of quantifier complexity, but it seems that no better bound has been known. We locate such a bound in a hierarchy of Suzuki and Yokoyama, which extends Towsner's framework of partial impredicativity. Specifically, we show that Fra\"iss\'e's conjecture is implied by a principle of pseudo $\Pi^1_1$-comprehension. As part of the proof, we introduce a cofinite version of the $\Delta^0_2$-Ramsey theorem, which may be of independent interest. We also relate pseudo $\Pi^1_1$-comprehension to principles of pseudo $\beta$-model reflection (due to Suzuki and Yokoyama) and reflection for $\omega$-models of transfinite induction (studied by Rathjen and Valencia-Vizca\'ino). In a forthcoming companion paper, we characterize pseudo $\Pi^1_1$-comprehension by a well-ordering principle, to get a transparent combinatorial bound for the strength of Fra\"iss\'e's conjecture.

math.LO↗

arXiv2024

Dilators and the reverse mathematics zoo

A predilator is a particularly uniform transformation of linear orders. We have a dilator when the transformation preserves well-foundedness. Over the theory $\mathsf{ACA}_0$ from reverse mathematics, any $\Pi^1_2$-formula is equivalent to the statement that some predilator is a dilator. We show how this completeness result breaks down without arithmetical comprehension: over $\mathsf{RCA}_0+\mathsf{PA}$, the statements from a large part of the reverse mathematics zoo are not equivalent to some predilator being a dilator.

math.LO↗

arXiv2023

An Introduction to Mathematical Logic

This introduction begins with a section on fundamental notions of mathematical logic, including propositional logic, predicate or first-order logic, completeness, compactness, the L\"owenheim-Skolem theorem, Craig interpolation, Beth's definability theorem and Herbrand's theorem. It continues with a section on G\"odel's incompleteness theorems, which includes a discussion of first-order arithmetic and primitive recursive functions. This is followed by three sections that are devoted, respectively, to proof theory (provably total recursive functions and Goodstein sequences for $\mathsf{I\Sigma}_1$), computability (fundamental notions and an analysis of K\H{o}nig's lemma in terms of the low basis theorem) and model theory (ultraproducts, chains and the Ax-Grothendieck theorem). We conclude with some brief introductory remarks about set theory (with more details reserved for a separate lecture). The author uses these notes for a first logic course for undergraduates in mathematics, which consists of 28 lectures and 14 exercise sessions of 90 minutes each. In such a course, it may be necessary to omit some material, which is straightforward since all sections except for the first two are independent of each other.

math.LO↗

arXiv2023

Provable better quasi orders

It has recently been shown that fairly strong axiom systems such as $\mathsf{ACA}_0$ cannot prove that the antichain with three elements is a better quasi order ($\mathsf{bqo}$). In the present paper, we give a complete characterization of the finite partial orders that are provably $\mathsf{bqo}$ in such axiom systems. The result will also be extended to infinite orders. As an application, we derive that a version of the minimal bad array lemma is weak over $\mathsf{ACA_0}$. In sharp contrast, a recent result shows that the same version is equivalent to $\Pi^1_2$-comprehension over the stronger base theory $\mathsf{ATR}_0$.

math.LO↗

arXiv2023

Weak well orders and Fra\"iss\'e's conjecture

The notion of well order admits an alternative definition in terms of embeddings between initial segments. We use the framework of reverse mathematics to investigate the logical strength of this definition and its connection with Fra\"iss\'e's conjecture, which has been proved by Laver. We also fill a small gap in Shore's proof that Fra\"iss\'e's conjecture implies arithmetic transfinite recursion over ${\bf RCA}_0$, by giving a new proof of $\Sigma^0_2$-induction.

math.LO↗

arXiv2023

The logical strength of minimal bad arrays

This paper studies logical aspects of the notion of better quasi order, which has been introduced by C. Nash-Williams (Mathematical Proceedings of the Cambridge Philosophical Society 1965 & 1968). A central tool in the theory of better quasi orders is the minimal bad array lemma. We show that this lemma is exceptionally strong from the viewpoint of reverse mathematics, a framework from mathematical logic. Specifically, it is equivalent to the set existence principle of $\Pi^1_2$-comprehension, over the base theory $\mathsf{ATR_0}$.

math.LO↗

arXiv2022

Normal functions and maximal order types

Transformations of well partial orders induce functions on the ordinals, via the notion of maximal order type. In most examples from the literature, these functions are not normal, in marked contrast with the central role that normal functions play in ordinal analysis and related work from computability theory. The present paper aims to explain this phenomenon. In order to do so, we investigate a rich class of order transformations that are known as $\mathsf{WPO}$-dilators. According to a first main result of this paper, $\mathsf{WPO}$-dilators induce normal functions when they satisfy a rather restrictive condition, which we call strong normality. Moreover, the reverse implication holds as well, for reasonably well behaved $\mathsf{WPO}$-dilators. Strong normality also allows us to explain another phenomenon: by previous work of Freund, Rathjen and Weiermann, a uniform Kruskal theorem for $\mathsf{WPO}$-dilators is as strong as $\Pi^1_1$-comprehension, while the corresponding result for normal dilators on linear orders is equivalent to the much weaker principle of $\Pi^1_1$-induction. As our second main result, we show~that $\Pi^1_1$-induction is equivalent to the uniform Kruskal theorem for $\mathsf{WPO}$-dilators that are strongly normal.

math.LO↗

arXiv2022

The uniform Kruskal theorem: between finite combinatorics and strong set existence

The uniform Kruskal theorem extends the original result for trees to general recursive data types. As shown by A. Freund, M. Rathjen and A. Weiermann, it is equivalent to $\Pi^1_1$-comprehension, over $\mathsf{RCA_0}$ with the chain antichain principle ($\mathsf{CAC}$). This result provides a connection between finite combinatorics and abstract set existence. The present paper sheds further light on this connection. First, we show that the original Kruskal theorem is equivalent to the uniform version for data types that are finitely generated. Secondly, we prove a dichotomy result for a natural variant of the uniform Kruskal theorem. On the one hand, this variant still implies $\Pi^1_1$-comprehension over $\mathsf{RCA}_0+\mathsf{CAC}$. On the other hand, it becomes weak when $\mathsf{CAC}$ is removed from the base theory.

math.LO↗

arXiv2022

On the logical strength of the better quasi order with three elements

The notion of better quasi order ($\mathsf{BQO}$), due to Nash-Williams, is very fruitful mathematically and intriguing from the standpoint of logic, due to several long-standing open problems. In the present paper, we make a significant step towards one of these: Let $\mathbf 3$ be the discrete order with three elements. We show that arithmetical recursion along the natural numbers ($\mathsf{ACA}_0^+$) follows from $\mathbf 3$ being $\mathsf{BQO}$, over the base theory $\mathsf{RCA_0}$ from reverse mathematics. Also over the latter, we deduce arithmetical transfinite recursion ($\mathsf{ATR}_0$) from the assumption that $\mathbf 3$ is $\Delta^0_2\text{-}\mathsf{BQO}$, which plays a role in work of Montalb\'an.

math.LO↗

arXiv2022

Higman's lemma is stronger for better quasi orders

We prove that Higman's lemma is strictly stronger for better quasi orders than for well quasi orders, within the framework of reverse mathematics. In fact, we show a stronger result: the infinite Ramsey theorem (for tuples of all lengths) follows from the statement that any array $[\mathbb N]^{n+1}\to\mathbb N^n\times X$ for a well order $X$ and $n\in\mathbb N$ is good, over the base theory $\mathsf{RCA_0}$.

math.LO↗

arXiv2022

Impredicativity and Trees with Gap Condition: A Second Course on Ordinal Analysis

These lecture notes introduce central notions of impredicative ordinal analysis, such as the Bachmann-Howard ordinal and the method of collapsing, which transforms uncountable proof trees into countable ones. Specifically, we analyze parameter-free $\Pi^1_1$-comprehension and show that it cannot prove the extended Kruskal theorem due to Harvey Friedman (not even for two labels). In terms of prerequisites, we build on a previous lecture on the ordinal analysis of Peano arithmetic. The present material is intended for 12 lectures and 6 exercise sessions of 90 minutes each.

math.LO↗

arXiv2022

R.E. Bruck, proof mining and a rate of asymptotic regularity for ergodic averages in Banach spaces

We analyze a proof of Bruck to obtain an explicit rate of asymptotic regularity for Ces\`aro means in uniformly convex Banach spaces. Our rate will only depend on a norm bound and a modulus $\eta$ of uniform convexity. One ingredient for the proof by Bruck is a result of Pisier, which shows that every uniformly convex (in fact every uniformly nonsquare) Banach space has some Rademacher type $q>1$ with a suitable constant $C_q$. We explicitly determine $q$ and $C_q$, which only depend on the single value $\eta(1)$ of our modulus. Beyond these specific results, we summarize how work of Bruck has inspired developments in the proof mining program, which applies tools from logic to obtain results in various areas of mathematics.

math.DS↗

arXiv2021

Reverse mathematics of a uniform Kruskal-Friedman theorem

The Kruskal-Friedman theorem asserts: in any infinite sequence of finite trees with ordinal labels, some tree can be embedded into a later one, by an embedding that respects a certain gap condition. This strengthening of the original Kruskal theorem has been proved by I. K\v{r}\'i\v{z} (Ann. Math. 1989), in confirmation of a conjecture due to H. Friedman, who had established the result for finitely many labels. It provides one of the strongest mathematical examples for the independence phenomenon from G\"odel's theorems. The gap condition is particularly relevant due to its connection with the graph minor theorem of N. Robertson and P. Seymour. In the present paper, we consider a uniform version of the Kruskal-Friedman theorem, which extends the result from trees to general recursive data types. Our main theorem shows that this uniform version is equivalent both to $\Pi^1_1$-transfinite recursion and to a minimal bad sequence principle of K\v{r}\'i\v{z}, over the base theory $\mathsf{RCA_0}$ from reverse mathematics. This sheds new light on the role of infinity in finite combinatorics.

math.LO↗

arXiv2021

Well ordering principles for iterated $\Pi^1_1$-comprehension

We introduce ordinal collapsing principles that are inspired by proof theory but have a set theoretic flavor. These principles are shown to be equivalent to iterated $\Pi^1_1$-comprehension and the existence of admissible sets, over weak base theories. Our work extends a previous result on the non-iterated case, which had been conjectured in Montalb\'an's "Open questions in reverse mathematics" (Bull. Symb. Log. 17(3)2011). This previous result has already been applied to the reverse mathematics of combinatorial and set theoretic principles. The present paper is a significant contribution to a general approach that connects these fields.

math.LO↗