Logic Colloquium 2024

Contributed Talk

Contributed Talks 10

Chair: Fedor Pakhomov

  Wednesday, 14:00, J431 ! Live

Time allocation: 20 minutes per speaker; 5 minutes for each changeover

Talks in this session


Alakh Dhruv Chopra, Strength of the hyperated finitary powerset operator

The finitary powerset operator \(\mathsf{P_f}\) maps a quasi-order \(X\) to the collection of its finite subsets ordered by a certain domination quasi-ordering (also called the Hoare embedding) while preserving the property of being a well-quasi-order. 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ández-Duque and Joosten, and can extended to operators on quasi-orders using techniques developed by Provenzano.

If \(X\) is a well-quasi-order, then so is \(\mathsf{P^\alpha_f}(X)\) for every \(\alpha\). When \(X\) is a well-order, this assertion is trivially provable. It explodes in reverse-mathematical 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 well-quasi-orders and of \(\mathsf{P_f}\) specifically, the order type of \(\mathsf{P^{\omega^\alpha}_f}\) is shown to have (fixpoint-free) Veblen-ian lower bounds when considering quasi-orders of the form \(\beta \oplus 1\) (aka, well-orders with one incomparable element).

This is part of an ongoing project with Fedor Pakhomov, Philipp Provenzano, and Giovanni Soldà to study better-quasi-orders and their reverse-mathematical strength, and can be considered a generalization of the \(\mathsf{H_f}\) operator previously studied by Anton Freund.


  1. David Fernández-Duque, Joost J. Joosten, Hyperations, Veblen progressions and transfinite iteration of ordinal functions, Annals of Pure and Applied Logic, vol. 164, issues 7–8, pp. 785–801.
  2. Philipp Provenzano, The reverse mathematical strength of hyperations, Master’s Thesis, 2022, (Unpublished).

Thibaut Kouptchinsky, The limits of determinacy in third-order 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 high-order 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)\)th-order arithmetic (\(\mathsf{Z}_{2+\gamma}\)) is the first to witness the determinacy of \(\Pi^0_{1+\gamma+2}\) Gale-Stewart games (\(\gamma < \omega_1^{\mathsf{CK}}\)).

For our part, we will look in more detail at the situation in second-order and third-order arithmetic, examining a paper by Montalbán and Shore [3]. We present a generalisation of their results, in some natural interpretation of third-order 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.


  1. H. M. Friedmann,Higher set theory and mathematical practice,Annals of Mathematicsvol. 2 (1971), no. 3, pp. 352–357.
  2. D. A. Martin,Borel determinacy,Annals of Mathematics,vol. 102 (1975), no. 2, pp. 363–371.
  3. A. Montalbán, R. A. Shore,The limits of determinacy in second order arithmetic,Israel Journal of Mathematics,vol. 104 (2011), no. 2, pp. 223–252.
  4. L. Pacheco, Ke. Yokoyama,Determinacy and reflection principles in second-order arithmetic,Preprint, arXiv (2022).
  5. S. G. Simpson,Subsystems of second order arithmetic (Second edition),Perspectives in Logic,Association for Symbolic Logic,2009.

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^{i-1}(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^{i-1}(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].


  1. E. Omri, A. Weiermann,Classifying the phase transition threshold for Ackermannian functions,Journal of Pure and Applied Logic,Vol. 158, (2009), pp. 156–162.
  2. F. Meskens, A. Weiermann,Classifying phase transition thresholds for Goodstein sequences and Hydra games,Gentzen’s Centenary,Springer International Publishing, Cham, (2015), pp. 455–478.
  3. L. Carlucci, G. Lee, A. Weiermann,Sharp thresholds for hypergraph regressive Ramsey numbers,Journal of combinatorial theory. Series A,Vol. 118(2), (2011), pp. 558–585.
  4. M. De Smet, A. Weiermann,Sharp Thresholds for a Phase Transition Related to Weakly Increasing Sequences,Journal of logic and computation,Vol. 22(2), (2012), pp. 207–211.
  5. L. Gordeev, A. Weiermann,Phase transitions in Proof Theory,Discrete Mathematics and Theoretical Computer Science,(Proceedings), (2010), pp. 343–358.

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


  1. Lev Gordeev,Generalizations of the one-dimensional version of the Kruskal-Friedman theorems,The Journal of Symbolic Logic,vol. 54 (1989), no. 1, pp. 100–121.

Giovanni Solda, Better quasi-orders and iterated ideals

Authors: Giovanni Solda and Fedor Pakhomov

The notion of better quasi-order (henceforth bqo) is a natural evolution of that of well quasi-order (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 second-order 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.

 Overview  Program