arXiv subjects
Publications and source records attributed to Anton Freund.
We exhibit a well-ordering principle that is equivalent to a theory of partial impredicativity. The latter goes back to Towsner and relates to recent work of Suzuki and Yokoyama. Together with part I of the present paper, this yields a combinatorial upper bound on the axiomatic strength of Fraïssé's conjecture.
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à-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.
We provide quantitative convergence results for continuous-time dynamical systems in metric spaces that satisfy a continuous-time analog of quasi-Fejér 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ér 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.
We prove conservativity results for weak Kőnig's lemma that extend the celebrated result of Harrington (for $Π^1_1$-statements) and are somewhat orthogonal to the extension by Simpson, Tanaka and Yamazaki (for statements of the form $\forall X\exists!Yψ$ with arithmetical $ψ$). 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őnig's lemma) is dispensable for certain results about continuous functions with isolated singularities.
One of the most important principles of J.-Y. Girard's $Π^1_2$-logic is induction on dilators. In particular, Girard used this principle to construct his famous functor $Λ$. He claimed that the totality of $Λ$ is equivalent to the set existence axiom of $Π^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 $Π^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 $Π^1_1$-comprehension is equivalent to the totality of a functor $\mathbb J$ due to P. Päppinghaus, which can be seen as a streamlined version of $Λ$.
Fraïssé's conjecture (proved by Laver) is implied by the $Π^1_1$-comprehension axiom of reverse mathematics, as shown by Montalbán. 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ïssé's conjecture is implied by a principle of pseudo $Π^1_1$-comprehension. As part of the proof, we introduce a cofinite version of the $Δ^0_2$-Ramsey theorem, which may be of independent interest. We also relate pseudo $Π^1_1$-comprehension to principles of pseudo $β$-model reflection (due to Suzuki and Yokoyama) and reflection for $ω$-models of transfinite induction (studied by Rathjen and Valencia-Vizcaíno). In a forthcoming companion paper, we characterize pseudo $Π^1_1$-comprehension by a well-ordering principle, to get a transparent combinatorial bound for the strength of Fraïssé's conjecture.
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 $Π^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.
This introduction begins with a section on fundamental notions of mathematical logic, including propositional logic, predicate or first-order logic, completeness, compactness, the Löwenheim-Skolem theorem, Craig interpolation, Beth's definability theorem and Herbrand's theorem. It continues with a section on Gödel'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Σ}_1$), computability (fundamental notions and an analysis of Kő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.
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 $Π^1_2$-comprehension over the stronger base theory $\mathsf{ATR}_0$.
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ïssé's conjecture, which has been proved by Laver. We also fill a small gap in Shore's proof that Fraïssé's conjecture implies arithmetic transfinite recursion over ${\bf RCA}_0$, by giving a new proof of $Σ^0_2$-induction.
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 $Π^1_2$-comprehension, over the base theory $\mathsf{ATR_0}$.
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 $Π^1_1$-comprehension, while the corresponding result for normal dilators on linear orders is equivalent to the much weaker principle of $Π^1_1$-induction. As our second main result, we show~that $Π^1_1$-induction is equivalent to the uniform Kruskal theorem for $\mathsf{WPO}$-dilators that are strongly normal.
We analyze a proof of Bruck to obtain an explicit rate of asymptotic regularity for Cesàro means in uniformly convex Banach spaces. Our rate will only depend on a norm bound and a modulus $η$ 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 $η(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.
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 $Π^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.
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 $Δ^0_2\text{-}\mathsf{BQO}$, which plays a role in work of Montalbán.
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 $Π^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 $Π^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.
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}$.
These are the lecture notes of an introductory course on ordinal analysis. Our selection of topics is guided by the aim to give a complete and direct proof of a mathematical independence result: Kruskal's theorem for binary trees is unprovable in conservative extensions of Peano arithmetic (note that much stronger results of this type are due to Harvey Friedman). Concerning prerequisites, we assume a solid introduction to mathematical logic but no specialized knowledge of proof theory. The material in these notes is intended for 12 lectures and 6 exercise sessions of 90 minutes each.