Contributed Talks 10
Chair: Fedor Pakhomov
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
14:00 
Alakh Dhruv Chopra, Strength of the hyperated finitary powerset operator 
The finitary powerset operator \(\mathsf{P_f}\) maps a quasiorder \(X\) to the collection of its finite subsets ordered by a certain domination quasiordering (also called the Hoare embedding) while preserving the property of being a wellquasiorder. This is a widely used and studied operator in mathematics and computer science. This is extended to its transfinite hyperation \(\mathsf{P^\alpha_f}\) for every ordinal \(\alpha\), a form of iteration that satisfies the compositional property \(\mathsf{P^{\alpha+\beta}_f}(X) = \mathsf{P^\alpha_f}(\mathsf{P^\beta_f}(X))\). Hyperations of ordinal functions were introduced by FernándezDuque and Joosten, and can extended to operators on quasiorders using techniques developed by Provenzano. If \(X\) is a wellquasiorder, then so is \(\mathsf{P^\alpha_f}(X)\) for every \(\alpha\). When \(X\) is a wellorder, this assertion is trivially provable. It explodes in reversemathematical strength as soon as the width of \(X\) is at least 2; for example, the statement for \(\mathsf{P^\omega_f}\) already reaches \(\mathsf{ACA^+_0}\). Using techniques from the study of maximal order types of wellquasiorders and of \(\mathsf{P_f}\) specifically, the order type of \(\mathsf{P^{\omega^\alpha}_f}\) is shown to have (fixpointfree) Veblenian lower bounds when considering quasiorders of the form \(\beta \oplus 1\) (aka, wellorders with one incomparable element). This is part of an ongoing project with Fedor Pakhomov, Philipp Provenzano, and Giovanni Soldà to study betterquasiorders and their reversemathematical strength, and can be considered a generalization of the \(\mathsf{H_f}\) operator previously studied by Anton Freund. Bibliography


14:25 
Thibaut Kouptchinsky, The limits of determinacy in thirdorder arithmetic 
Authors: Thibaut Kouptchinsky and Juan Aguilera This talk is about the foundations of mathematics, studying determinacy axioms derived from game theory, with a reverse mathematics point of view. Reverse Mathematics is an endeavour to compare theorems according to the “strength” of the axioms a mathematician needs to prove them (see [5]). We study a refined case of the proof from Martin of Borel determinacy [2], which showed how to use the existence of highorder objects when one wants to show that infinite games of increasing difficulty in the Borel hierarchy have winning strategies (and thus are called determined). The use of such principles had already been shown to be necessary by Friedmann [1]. In the terms that will be ours, Martin provided the final proof that \((2+\gamma)\)thorder arithmetic (\(\mathsf{Z}_{2+\gamma}\)) is the first to witness the determinacy of \(\Pi^0_{1+\gamma+2}\) GaleStewart games (\(\gamma < \omega_1^{\mathsf{CK}}\)). For our part, we will look in more detail at the situation in secondorder and thirdorder arithmetic, examining a paper by Montalbán and Shore [3]. We present a generalisation of their results, in some natural interpretation of thirdorder arithmetic about infinite games which complexity is described by the difference hierarchy of \(\Pi^0_4\) sets. Along the way, we underline a shift compared to the analogous situation in the countable case (about differences of \(\Pi^0_3\) sets), which is the object of the paper of Montalbán and Shore. Namely, we need less of the separation scheme than in the countable case. Finally, we use these generalisations following the results of Pacheco and Yokoyama to [4] show that, while \[\forall m \in \omega \mathsf{Z}_{2+\gamma} \vdash (\Pi^0_{1+\gamma+2})_m\text{}\mathsf{Det} \qquad \text{but} \qquad \mathsf{Z}_{2+\gamma} \not\vdash \forall m (\Pi^0_{1+\gamma+2})_m\text{}\mathsf{Det},\]the last theorem is equivalent to a form of reflection principle. Bibliography


14:50 
Gabriele Buriola, Phase Transition Thresholds for Generalized Goodstein Sequences, Hydra Games and Ackermannian Functions. 
Authors: Gabriele Buriola and Andreas Weiermann We extend previous results [2] regarding the phase transition thresholds for Goodstein Sequences and Hydra Games to a more general setting. In both cases, we substitute the original successor function with the iterations of a strictly increasing primitive recursive function \(g\) satisfying the condition \(g(x) \geq x+1\); more precisely, the steps of the Hydra Game, originally of type \(\alpha_{f\!,i+1}= \alpha_{f\!,i}[1+f(i)]\), are now of the form \(\alpha^{f\!,g}_{i+1}=\alpha^{f\!,g}_{i}[1+f(g^{i1}(1))]\), while the steps of Goodstein sequences are changed from \(m_{f\!,i+1}=m_{f\!,i}\left(1+f(i) \mapsto 1+f(i+1)\right) 1\) to \(m^{f\!,g}_{i+1}=m^{f\!,g}_i\left(1+f(g^{i1}(1)) \mapsto 1+f(g^{i}(1))\right) 1\). The new phase transition thresholds incorporate the starting function \(g\). These findings also allow a generalization of the phase transition threshold for Ackermannian functions [1] and fit within a rich literature regarding phase transitions in provability [3,4,5]. Bibliography


15:15 
Patrick Uftring, Sequences with gap condition and binary trees with ascending labels 
In the context of reverse mathematics, Gordeev could prove in \(\textsf{RCA}_0\) that the following statement is equivalent to arithmetical transfinite recursion: For each well order \(\alpha\), the partial order of finite sequences with members in \(\alpha\) ordered using a symmetric variant of Friedman’s gap condition is a well partial order (cf. [1]). We present a new and simpler proof for this result using a connection to binary trees with ascending labels, i.e., with labels from a well order \(\alpha\) that weakly ascend (from root to leaf). Moreover, we extend Gordeev’s characterization of \(\textsf{ATR}_0\) to both such trees and sequences ordered using stronger variants of the gap condition. Finally, we present the maximal order types of all discussed well partial orders for any given well order \(\alpha\). Bibliography


15:40 
Giovanni Solda, Better quasiorders and iterated ideals 
Authors: Giovanni Solda and Fedor Pakhomov The notion of better quasiorder (henceforth bqo) is a natural evolution of that of well quasiorder (henceforth wqo). Intuitively, a wqo is bqo if all of its iterated powersets are also wqo’s: this gives bqo’s much stronger closure properties than the ones wqo’s enjoy. In this talk, we give a new characterization of bqo’s. Inspired by the intuition we gave above, we look at the class of iterated ideals of a wqo: this produces a much smaller object than the iterated powerset. Our main result is that this smaller object still contains a lot of information on the original wqo: namely, a wqo \(Q\) is bqo if and only if the iterated ideals of \(Q\) form a wqo, and the formalization of this result in secondorder arithmetic is provable over \(\mathsf{ATR}_0\). We will then show some properties of the class of iterated ideals, and point at some (potential) applications. 