arXiv subjects

Giovanni Soldà

Publications and source records attributed to Giovanni Soldà.

8 recordsLinked to original sources

arXiv2026

Infinitary provability logic

Gödel-Löb provability logic $\GL$ is a propositional modal system that on one hand enjoys completeness with respect to conversely well-founded Kripke frames and on the other hand captures all modal principles about $\PA$-provability that are provable in $\PA$ itself. In the present paper we carry out an initial investigation into the question of what the infinitary counterpart of $\GL$ is. We develop a non-well-founded deep inference proof system $\dgla$ for the modal language with at most countably infinite conjunctions and disjunctions. We show that the calculus is sound and complete for well-founded transitive Kripke frames. Using Kripke-Platek set theory we develop an interpretation of the infinitary modal language in terms of infinitary provability over admissible sets. Then we show that a natural Hilber-style variant of infinitary $\GL$ is sound for this interpretation. We leave open, however, the question if $\dgla$ proves any additional theorems in comparison with the Hilbert-style calculus. Nevertheless, under certain conditions we do show that the infinitary provability logic arising from certain admissible sets lies between the set of theorems of the Hilbert-style calculus and the non-well-founded deep inference system.

math.LO↗

arXiv2025

Generalized Higman's Theorem and iterated ideals

Generalized Higman's Theorem is the direct counterpart of Higman's Theorem that asserts the closure of the class of \emph{better} quasi-orders, instead of the class of \emph{well} quasi-orders, under the construction $P\mapsto P^{<ω}$ of the embeddability order on finite sequences. Traditionally, this result is obtained as a consequence of very powerful and general techniques of Nash-Williams. In this paper, we propose a new proof of this result that is based on an explicit characterization of the underlying orders. In particular, this new technique allows us to formalize the proof of the result in the formal theory $\mathsf{atr}_0$, thus resolving a long-standing open problem in the field of reverse mathematics. The main ingredient of our proof is the introduction of a transfinite hierarchy of orders $\dot I^*_α(P)$ starting with $\dot I^*_0(P)=P$ and $\dot I^*_{α+1}(P)$ being the inclusion order on ideals of $\dot I^*_α(P)$. On one hand, we show that a quasi-order $P$ is a bqo if and only if all $\dot I^*_α(P)$ are wqos. On the other hand, under the assumption that $P$ is a bqo, we show that the $\dot I^*_α(P^{<ω})$ are wqos, and furthermore give a characterization of their structure in terms of a transfinite iteration of a Higman-like construction. The sufficiently explicit character of this proof allows us to formalize it in a rather straightforward manner.

math.LO↗

arXiv2024

On Nash-Williams' Theorem regarding sequences with finite range

The famous theorem of Higman states that for any well-quasi-order (wqo) $Q$ the embeddability order on finite sequences over $Q$ is also wqo. In his celebrated 1965 paper, Nash-Williams established that the same conclusion holds even for all the transfinite sequences with finite range, thus proving a far reaching generalization of Higman's theorem. In the present paper we show that Nash-Williams' Theorem is provable in the system $\mathsf{ATR}_0$ of second-order arithmetic, thus solving an open problem by Antonio Montalbán and proving the reverse-mathematical equivalence of Nash-Williams' Theorem and $\mathsf{ATR}_0$. In order to accomplish this, we establish equivalent characterization of transfinite Higman's order and an order on the cumulative hierarchy with urelements from the starting wqo $Q$, and find some new connection that can be of purely order-theoretic interest. Moreover, in this paper we present a new setup that allows us to develop the theory of $α$-wqo's in a way that is formalizable within primitive-recursive set theory with urelements, in a smooth and code-free fashion.

math.LO↗

arXiv2024

Sequential discontinuity and first-order problems

We explore the low levels of the structure of the continuous Weihrauch degrees of first-order problems. In particular, we show that there exists a minimal discontinuous first-order degree, namely that of $\accn$, without any determinacy assumptions. The same degree is also revealed as the least sequentially discontinuous one, i.e. the least degree with a representative whose restriction to some sequence converging to a limit point is still discontinuous. The study of games related to continuous Weihrauch reducibility constitutes an important ingredient in the proof of the main theorem. We present some initial additional results about the degrees of first-order problems that can be obtained using this approach.

math.LO↗

arXiv2023

Provable better quasi orders

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

math.LO↗

arXiv2023

The logical strength of minimal bad arrays

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

math.LO↗

arXiv2022

(Extra)ordinary equivalences with the ascending/descending sequence principle

We analyze the axiomatic strength of the following theorem due to Rival and Sands in the style of reverse mathematics. "Every infinite partial order $P$ of finite width contains an infinite chain $C$ such that every element of $P$ is either comparable with no element of $C$ or with infinitely many elements of $C$." Our main results are the following. The Rival-Sands theorem for infinite partial orders of arbitrary finite width is equivalent to $\mathsf{I}Σ^0_2 + \mathsf{ADS}$ over $\mathsf{RCA}_0$. For each fixed $k \geq 3$, the Rival-Sands theorem for infinite partial orders of width $\leq\! k$ is equivalent to $\mathsf{ADS}$ over $\mathsf{RCA}_0$. The Rival-Sands theorem for infinite partial orders that are decomposable into the union of two chains is equivalent to $\mathsf{SADS}$ over $\mathsf{RCA}_0$. Here $\mathsf{RCA}_0$ denotes the recursive comprehension axiomatic system, $\mathsf{I}Σ^0_2$ denotes the $Σ^0_2$ induction scheme, $\mathsf{ADS}$ denotes the ascending/descending sequence principle, and $\mathsf{SADS}$ denotes the stable ascending/descending sequence principle. To our knowledge, these versions of the Rival-Sands theorem for partial orders are the first examples of theorems from the general mathematics literature whose strength is exactly characterized by $\mathsf{I}Σ^0_2 + \mathsf{ADS}$, by $\mathsf{ADS}$, and by $\mathsf{SADS}$. Furthermore, we give a new purely combinatorial result by extending the Rival-Sands theorem to infinite partial orders that do not have infinite antichains, and we show that this extension is equivalent to arithmetical comprehension over $\mathsf{RCA}_0$.

math.LO↗

arXiv2021

An inside/outside Ramsey theorem and recursion theory

Inspired by Ramsey's theorem for pairs, Rival and Sands proved what we refer to as an inside/outside Ramsey theorem: every infinite graph $G$ contains an infinite subset $H$ such that every vertex of $G$ is adjacent to precisely none, one, or infinitely many vertices of $H$. We analyze the Rival-Sands theorem from the perspective of reverse mathematics and the Weihrauch degrees. In reverse mathematics, we find that the Rival-Sands theorem is equivalent to arithmetical comprehension and hence is stronger than Ramsey's theorem for pairs. We also identify a weak form of the Rival-Sands theorem that is equivalent to Ramsey's theorem for pairs. We turn to the Weihrauch degrees to give a finer analysis of the Rival-Sands theorem's computational strength. We find that the Rival-Sands theorem is Weihrauch equivalent to the double jump of weak König's lemma. We believe that the Rival-Sands theorem is the first natural theorem shown to exhibit exactly this strength. Furthermore, by combining our result with a result of Brattka and Rakotoniaina, we obtain that solving one instance of the Rival-Sands theorem exactly corresponds to simultaneously solving countably many instances of Ramsey's theorem for pairs. Finally, we show that the uniform computational strength of the weak Rival-Sands theorem is weaker than that of Ramsey's theorem for pairs by showing that a number of well-known consequences of Ramsey's theorem for pairs do not Weihrauch reduce to the weak Rival-Sands theorem. We also address an apparent gap in the literature concerning the relationship between Weihrauch degrees corresponding to the ascending/descending sequence principle and the infinite pigeonhole principle.

math.LO↗