arXiv subjects

Anton Freund

Publications and source records attributed to Anton Freund.

At least 37 records · Page 2Linked to original sources

arXiv2022

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říž (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ödel'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 $Π^1_1$-transfinite recursion and to a minimal bad sequence principle of Kříž, 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 $Π^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 $Π^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án'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↗

arXiv2021

Bounds for a nonlinear ergodic theorem for Banach spaces

We extract quantitative information (specifically, a rate of metastability in the sense of Terence Tao) from a proof due to Kazuo Kobayasi and Isao Miyadera, which shows strong convergence for Cesàro means of nonexpansive maps on Banach spaces.

math.DS↗

arXiv2021

Derivatives of normal functions in reverse mathematics

Consider a normal function $f$ on the ordinals (i. e. a function $f$ that is strictly increasing and continuous at limit stages). By enumerating the fixed points of $f$ we obtain a faster normal function $f'$, called the derivative of $f$. The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to normal functions $f:\aleph_1\rightarrow\aleph_1$ that are represented by dilators (i. e. particularly uniform endofunctors on the category of well-orders, as introduced by J.-Y. Girard). Due to a categorical construction of P. Aczel, each normal dilator $T$ has a derivative $\partial T$. We will give a new construction of the derivative, which shows that the existence and fundamental properties of $\partial T$ can already be established in the theory $\mathbf{RCA}_0$. The latter does not prove, however, that $\partial T$ preserves well-foundedness. Our main result shows that the statement ``for every normal dilator $T$, its derivative $\partial T$ preserves well-foundedness'' is $\mathbf{ACA}_0$-provably equivalent to $Π^1_1$-bar induction (and hence to $Σ^1_1$-dependent choice and to $Π^1_2$-reflection for $ω$-models).

math.LO↗

arXiv2021

How strong are single fixed points of normal functions?

In a recent paper by M. Rathjen and the present author it has been shown that the statement ``every normal function has a derivative'' is equivalent to $Π^1_1$-bar induction. The equivalence was proved over $\mathbf{ACA_0}$, for a suitable representation of normal functions in terms of dilators. In the present paper we show that the statement ``every normal function has at least one fixed point'' is equivalent to $Π^1_1$-induction along the natural numbers.

math.LO↗

arXiv2021

Set-theoretic reflection is equivalent to induction over well-founded classes

We show that induction over $Δ(\mathbb R)$-definable well-founded classes is equivalent to the reflection principle which asserts that any true formula of first order set theory with real parameters holds in some transitive set. The equivalence is proved in primitive recursive set theory (which is weaker than Kripke-Platek set theory) extended by the axiom of dependent choice.

math.LO↗

arXiv2021

A note on ordinal exponentiation and derivatives of normal functions

Michael Rathjen and the present author have shown that $Π^1_1$-bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in $\mathbf{ACA_0}$. In this note we show that the base theory can be weakened to $\mathbf{RCA_0}$. Our argument makes crucial use of a normal function $f$ with $f(α)\leq 1+α^2$ and $f'(α)=ω^{ω^α}$. We will also exhibit a normal function $g$ with $g(α)\leq 1+α\cdot 2$ and $g'(α)=ω^{1+α}$.

math.LO↗

arXiv2021

What is effective transfinite recursion in reverse mathematics?

In the context of reverse mathematics, effective transfinite recursion refers to a principle that allows us to construct sequences of sets by recursion along arbitrary well orders, provided that each set is $Δ^0_1$-definable relative to the previous stages of the recursion. It is known that this principle is provable in $\mathbf{ACA}_0$. In the present note, we argue that a common formulation of effective transfinite recursion is too restrictive. We then propose a more liberal formulation, which appears very natural and is still provable in $\mathbf{ACA}_0$.

math.LO↗

arXiv2021

Bachmann-Howard Derivatives

It is generally accepted that H. Friedman's gap condition is closely related to iterated collapsing functions from ordinal analysis. But what precisely is the connection? We offer the following answer: In a previous paper we have shown that the gap condition arises from an iterative construction on transformations of partial orders. Here we show that the parallel construction for linear orders yields familiar collapsing functions. The iteration step in the linear case is an instance of a general construction that we call `Bachmann-Howard derivative'. In the present paper, we focus on the unary case, i.e., on the gap condition for sequences rather than trees and, correspondingly, on addition-free ordinal notation systems. This is partly for convenience, but it also allows us to clarify a phenomenon that is specific to the unary setting: As shown by van der Meeren, Rathjen and Weiermann, the gap condition on sequences admits two linearizations with rather different properties. We will see that these correspond to different recursive constructions of sequences.

math.LO↗

arXiv2021

Patterns of resemblance and Bachmann-Howard fixed points

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.

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

Predicative collapsing principles

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.

math.LO↗

arXiv2020

Computable Aspects of the Bachmann-Howard Principle

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.

math.LO↗

arXiv2020

Well ordering principles and $Π^1_4$-statements: a pilot study

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.

math.LO↗

arXiv2020

A mathematical commitment without computational strength

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.

math.LO↗

arXiv2020

Short Proofs for Slow Consistency

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.

math.LO↗

arXiv2020

From Kruskal's theorem to Friedman's gap condition

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.

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↗