arXiv subjects

Anton Freund

Publications and source records attributed to Anton Freund.

43 records · Page 3Linked to original sources

arXiv2019

A Categorical Construction of Bachmann-Howard Fixed Points

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$.

math.LO↗

arXiv2019

$Π^1_1$-Comprehension as a Well-Ordering Principle

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.

math.LO↗

arXiv2018

A Higher Bachmann-Howard Principle

We present a higher well-ordering principle which is equivalent (over Simpson's set theoretic version of $\text{ATR}_0$) to the existence of transitive models of Kripke-Platek set theory, and thus to $Π^1_1$-comprehension. This is a partial solution to a conjecture of Montalbán and Rathjen: partial in the sense that our well-ordering principle is less constructive than demanded in the conjecture.

math.LO↗

arXiv2018

A Note on Iterated Consistency and Infinite Proofs

Schmerl and Beklemishev's work on iterated reflection achieves two aims: It introduces the important notion of $Π^0_1$-ordinal, characterizing the $Π^0_1$-theorems of a theory in terms of transfinite iterations of consistency; and it provides an innovative calculus to compute the $Π^0_1$-ordinals for a range of theories. The present note demonstrates that these achievements are independent: We read off $Π^0_1$-ordinals from a Schütte-style ordinal analysis via infinite proofs, in a direct and transparent way.

math.LO↗

arXiv2017

Slow Reflection

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).

math.LO↗

arXiv2017

Proof Lengths for Instances of the Paris-Harrington Principle

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.

math.LO↗

arXiv2015

A Uniform Characterization of $Σ_1$-Reflection over the Fragments of Peano Arithmetic

We show that the theory $IΣ_1$ of $Σ_1$-induction proves the following statement: For all $n\geq 2$, the uniform $Σ_1$-reflection principle over the theory $IΣ_n$ is equivalent to the totality of the function $F_{ω_n}$ at stage $ω_n$ of the fast-growing hierarchy. The method applied is a formalization of infinite proof theory. The literature contains several proofs which place the quantification over $n$ in the meta-theory (and also prove the separate cases $n=0,1$). In contrast, the author knows of no explicit argument that would allow us to internalize the quantification while keeping the meta-theory as low as $IΣ_1$. It is well possible that this has been considered before. Our aim is merely to provide a detailed exposition of this important result.

math.LO↗