Searcharxiv⌕ Search

arXiv subjects

Patrick Uftring

Publications and source records attributed to Patrick Uftring.

9 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↗
arXiv2025

Maximal order types for sequences with gap condition

Higman's lemma states that for any well partial order $X$, the partial order $X^*$ of finite sequences with members from $X$ is also well. By combining results due to Girard as well as Sch\"{u}tte and Simpson, one can show that Higman's lemma is equivalent to arithmetical comprehension over $\textsf{RCA}_0$, the usual base system of reverse mathematics. By incorporating Friedman's gap condition, Sch\"{u}tte and Simpson defined a slightly different order on finite number sequences with fewer comparisons. While it is still true that their definition yields a well partial order, it turns out that arithmetical comprehension is not enough to prove this fact. Gordeev considered a symmetric variation of this gap condition for sequences with members from arbitrary well orders. He could show, over $\textsf{RCA}_0$, that his partial order on sequences is well (for any underlying well order) if and only if arithmetical transfinite recursion is available. We present a new and simpler proof of this fact and extend Gordeev's results to weak and strong gap conditions as well as binary trees with weakly ascending labels. Moreover, we compute the maximal order types of all considered structures.

math.LO↗
arXiv2025

The uniform Kruskal theorem over RCA$_0$

Kruskal's theorem famously states that finite trees (ordered using an infima-preserving embeddability relation) form a well partial order. Freund, Rathjen, and Weiermann extended this result to general recursive data types with their uniform Kruskal theorem. They do not only show that this principle is true but also, in the context of reverse mathematics, that their theorem is equivalent to ${\Pi^1_1}$-comprehension, the characterizing axiom of ${\Pi^1_1\textsf{-CA}_0}$. However, their proof is not carried out directly over ${\textsf{RCA}_0}$, the usual base system of reverse mathematics. Instead, it additionally requires a weak consequence of Ramsey's theorem for pairs and two colors: the chain antichain principle. In this article, we show that this additional assumption is not necessary and the considered equivalence between the uniform Kruskal theorem and $\Pi^1_1$-comprehension already holds over ${\textsf{RCA}_0}$. For this, we improve Girard's characterization of arithmetical comprehension using ordinal exponentiation by showing that his result even remains correct if only a certain subclass of well orders is considered.

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↗
arXiv2023

On inverse Goodstein sequences

In the late 1980s, Abrusci, Girard and van de Wiele defined a variant of Goodstein sequences: the so-called inverse Goodstein sequence. In their work, they show that it terminates precisely at the Bachmann-Howard ordinal. This reveals that a proof of this fact requires substantial consistency strength. Moreover, the authors could show that sequences of this kind terminate even if the hereditary base change at the heart of their construction is replaced by a generalization using arbitrary dilators. It has been a conjecture by Andreas Weiermann that this more general result has a connection to Bachmann-Howard fixed points and is, therefore, equivalent to one of the most famous strong set existence principles from reverse mathematics: $\Pi^1_1$-comprehension. In this article, we prove this conjecture to be correct. Moreover, we show that the ordinal at which such sequences terminate is, in a fundamental way, isomorphic to the $1$-fixed point of their dilator, a new concept introduced by Freund and Rathjen. This yields explicit notation systems and a general method for specifying such ordinals. Also, using the notation systems provided by $1$-fixed points, we can reproduce the result that the Goodstein sequence terminates at the Bachmann-Howard ordinal in a weak system. Additionally, we perform a similar computation for a variant of Goodstein sequences, which terminates at a predicative ordinal.

math.LO↗
arXiv2023

Weihrauch degrees without roots

We answer the following question by Arno Pauly: "Is there a square-root operator on the Weihrauch degrees?". In fact, we show that there are uncountably many pairwise incomparable Weihrauch degrees without any roots. We also prove that the omniscience principles of LPO and LLPO do not have roots.

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

Weak and Strong Versions of Effective Transfinite Recursion

Working in the context of reverse mathematics, we give a fine-grained characterization result on the strength of two possible definitions for Effective Transfinite Recursion used in literature. Moreover, we show that $\Pi^0_2$-induction along a well-order $X$ is equivalent to the statement that the exponentiation of any well-order to the power of $X$ is well-founded.

math.LO↗