BZPEERReading, trust and collaboration for researchDiscover
Workspaces
Network
Opportunities
Account
Researcher profile
Anton Freund contributes to research discovery and scholarly infrastructure.
Trust snapshot
Actions
Identity and collaboration
Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.
Log in to claimDirect collaboration
Claim this author entity first to unlock direct invitations.
Research graph
Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
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 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.
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.
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.
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.
Timothy Carlson's patterns of resemblance employ the notion of $Σ_1$-elementarity to describe large computable ordinals. It has been conjectured that a relativization of these patterns to dilators leads to an equivalence with $Π^1_1$-comprehension (Question 27 of A. Montalbán's "Open questions in reverse mathematics", Bull. Symb. Log. 17(3)2011, 431-454). In the present paper we prove this conjecture. The crucial direction (towards $Π^1_1$-comprehension) is reduced to a previous result of the author, which is concerned with relativizations of the Bachmann-Howard ordinal.
We present a new manifestation of Gödel's second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert's program. Specifically, we consider a proper extension of Peano arithmetic ($\mathbf{PA}$) by a mathematically meaningful axiom scheme that consists of $Σ^0_2$-sentences. These sentences assert that each computably enumerable ($Σ^0_1$-definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is important for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel's second incompleteness theorem. In contrast, Gödel's theorem is not needed for typical examples of $Π^0_2$-independence (such as the Paris-Harrington principle), since computational strength provides an extensional invariant on the level of $Π^0_2$-sentences.
We have previously established that $Π^1_1$-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann-Howard fixed point, over $\mathbf{ATR_0}$. In the present paper we show that the base theory can be lowered to $\mathbf{RCA_0}$. We also show that the minimal Bachmann-Howard fixed point of a dilator $T$ can be represented by a notation system $\vartheta(T)$, which is computable relative to $T$. The statement that $\vartheta(T)$ is well-founded for any dilator $T$ will still be equivalent to $Π^1_1$-comprehension. Thus the latter is split into the computable transformation $T\mapsto\vartheta(T)$ and a statement about the preservation of well-foundedness, over a system of computable mathematics.
Harvey Friedman's gap condition on embeddings of finite labelled trees plays an important role in combinatorics (proof of the graph minor theorem) and mathematical logic (strong independence results). In the present paper we show that the gap condition can be reconstructed from a small number of well-motivated building blocks: it arises via iterated applications of 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.
We show that arithmetical transfinite recursion is equivalent to a suitable formalization of the following: For every ordinal $α$ there exists an ordinal $β$ such that $1+β\cdot(β+α)$ (ordinal arithmetic) admits an almost order preserving collapse into $β$. Arithmetical comprehension is equivalent to a statement of the same form, with $β\cdotα$ at the place of $β\cdot(β+α)$. We will also characterize the principles that any set is contained in a countable coded $ω$-model of arithmetical transfinite recursion resp. arithmetical comprehension.
Let $\operatorname{Con}(\mathbf T)\!\restriction\!x$ denote the finite consistency statement "there are no proofs of contradiction in $\mathbf T$ with $\leq x$ symbols". For a large class of natural theories $\mathbf T$, Pudlák has shown that the lengths of the shortest proofs of $\operatorname{Con}(\mathbf T)\!\restriction\!n$ in the theory $\mathbf T$ itself are bounded by a polynomial in $n$. At the same time he conjectures that $\mathbf T$ does not have polynomial proofs of the finite consistency statements $\operatorname{Con}(\mathbf T+\operatorname{Con}(\mathbf T))\!\restriction\!n$. In contrast we show that Peano arithmetic ($\mathbf{PA}$) has polynomial proofs of $\operatorname{Con}(\mathbf{PA}+\operatorname{Con}^*(\mathbf{PA}))\!\restriction\!n$, where $\operatorname{Con}^*(\mathbf{PA})$ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen and Weiermann. We also obtain a new proof of the result that the usual consistency statement $\operatorname{Con}(\mathbf{PA})$ is equivalent to $\varepsilon_0$ iterations of slow consistency. Our argument is proof-theoretic, while previous investigations of slow consistency relied on non-standard models of arithmetic.
In previous work, the author has shown that $Π^1_1$-induction along $\mathbb N$ is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of J.-Y. Girard's dilators, which are particularly uniform transformations of well orders. The present paper works on the next type level and considers uniform transformations of dilators, which are called $2$-ptykes. We show that $Π^1_2$-induction along $\mathbb N$ is equivalent to the existence of fixed points for all $2$-ptykes that satisfy a certain normality condition. Beyond this specific result, the paper paves the way for the analysis of further $Π^1_4$-statements in terms of well ordering principles.
A dilator is a particularly uniform transformation $X\mapsto T_X$ of linear orders that preserves well-foundedness. We say that $X$ is a Bachmann-Howard fixed point of $T$ if there is an almost order preserving collapsing function $\vartheta:T_X\rightarrow X$ (precise definition to follow). In the present paper we show that $Π^1_1$-comprehension is equivalent to the assertion that every dilator has a well-founded Bachmann-Howard fixed point. This proves a conjecture of M. Rathjen and A. Montalbán.
Peter Aczel has given a categorical construction for fixed points of normal functors, i.e. dilators which preserve initial segments. For a general dilator $X\mapsto T_X$ we cannot expect to obtain a well-founded fixed point, as the order type of $T_X$ may always exceed the order type of $X$. In the present paper we show how to construct a Bachmann-Howard fixed point of $T$, i.e. an order $\operatorname{BH}(T)$ with an "almost" order preserving collapse $\vartheta:T_{\operatorname{BH}(T)}\rightarrow\operatorname{BH}(T)$. Building on previous work, we show that $Π^1_1$-comprehension is equivalent to the assertion that $\operatorname{BH}(T)$ is well-founded for any dilator $T$.
As Paris and Harrington have famously shown, Peano Arithmetic does not prove that for all numbers $k,m,n$ there is an $N$ which satisfies the statement $\operatorname{PH}(k,m,n,N)$: For any $k$-colouring of its $n$-element subsets the set $\{0,\dots,N-1\}$ has a large homogeneous subset of size $\geq m$. At the same time very weak theories can establish the $Σ_1$-statement $\exists_N\operatorname{PH}(\overline k,\overline m,\overline n,N)$ for any fixed parameters $k,m,n$. Which theory, then, does it take to formalize natural proofs of these instances? It is known that $\forall_m\exists_N\operatorname{PH}(\overline k,m,\overline n,N)$ has a natural and short proof (relative to $n$ and $k$) by $Σ_{n-1}$-induction. In contrast, we show that there is an elementary function $e$ such that any proof of $\exists_N\operatorname{PH}(\overline{e(n)},\overline{n+1},\overline n,N)$ by $Σ_{n-2}$-induction is ridiculously long. In order to establish this result on proof lengths we give a computational analysis of slow provability, a notion introduced by Sy-David Friedman, Rathjen and Weiermann. We will see that slow uniform $Σ_1$-reflection is related to a function that has a considerably lower growth rate than $F_{\varepsilon_0}$ but dominates all functions $F_α$ with $α<\varepsilon_0$ in the fast-growing hierarchy.
We describe a "slow" version of the hierarchy of uniform reflection principles over Peano Arithmetic ($\mathbf{PA}$). These principles are unprovable in Peano Arithmetic (even when extended by usual reflection principles of lower complexity) and introduce a new provably total function. At the same time the consistency of $\mathbf{PA}$ plus slow reflection is provable in $\mathbf{PA}+\operatorname{Con}(\mathbf{PA})$. We deduce a conjecture of S.-D. Friedman, Rathjen and Weiermann: Transfinite iterations of slow consistency generate a hierarchy of precisely $\varepsilon_0$ stages between $\mathbf{PA}$ and $\mathbf{PA}+\operatorname{Con}(\mathbf{PA})$ (where $\operatorname{Con}(\mathbf{PA})$ refers to the usual consistency statement).