The studies of Weihrauch degrees and reverse mathematics share many ideas, and many similar results and close relations are known. The studies of Weihrauch degrees of the arithmetical transfinite recursion (ATR) and their relation to reverse mathematics are developed, e.g., in [1,2,3]. Typically, principles which are provable from $ATR_0$ (in the setting of reverse mathematics) by way of the pseudo-hierarchy method have various strengths. In this talk, we overview these situations and study the structure between ATR and the choice principle on the Baire space. This is joint work with Yudai Suzuki.
T. Kihara, A. Marcone and A. Pauly. Searching for an analogue of $ATR_0$ in the Weihrauch lattice. J. Symb. Log., 85(3):1006–1043, 2020.
Jun Le Goh. Some computability-theoretic reductions between principles around ATR0. arXiv preprint arXiv:1905.06868, 2019.
Paul-Elliot Anglès d'Auriac. Infinite Computations in Algorithmic Randomness and Reverse Mathematics. PhD thesis, Université Paris-Est, 2019.
Y. Suzuki and K. Yokoyama. Searching problems above arithmetical transfinite recursion. In preparation.
Location: MALL
Title: A proof theorist's job: transfinite induction in a finitary context
This talk will be about ordinal analysis, a technique at the core of a proof theorist's toolchain. Using Tait calculus as the formal proof system for arithmetic, we will replicate Gentzen's famous consistency proof as the seemingly useless statement "enough of set theory ⊢ Con(PA)". Hopefully, I will convince the audience that the left-hand side of the turnstile can be weakened to a theory of transfinite induction formalised in primitive recursive arithmetic, and this proof thus measures the proof-theoretic strength of a formal theory using the linear ordering in a given ordinal representation system.
Location: MALL
Title: Formalising Erdős and Larson: Ordinal Partition Theory
NOTE date and time change: Tue 11am
A number of results in infinitary combinatorics have been formalised in the proof assistant Isabelle/HOL. These include results on ordinal partition relations by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s 1973 proof that for all $m$ in $ℕ$, $ω^ω → (ω^ω,m)$. This material is available online; here we discuss some of the most challenging aspects of the formalisation process, and wider issues in the formalisation of research-grade mathematics. See also the paper in Experimental Mathematics 31:2, 2022.
Location: MALL
Title: The Axiom of Determinacy and Large Cardinals — Part 2: Not So Large After All
This is the second and final talk in this survey of the Axiom of Determinacy (AD) and its implications on large cardinals. In the first talk, we looked at some first properties of AD and defined the cardinal Θ, which will play a prominent role in the rest of this series. In this talk, we will begin by defining some large cardinal properties — properties that cannot be provably exhibited by cardinals under ZFC — measurability, strong compactness, and supercompactness. We will then state results by Solovay which show that under ZF + AD (or its stronger counterpart ZF + ADR), ω1 satisfies these properties at least partially. We will sketch proofs for some (time permitting, all) of these results.
Although this talk builds on the first one, we will recall all relevant definitions and results from there, so that this talk will be accessible even if the audience has not attended the first one.
Location: MALL 1
Title: Purity in chains of modules
The model theory of modules extends naturally to certain functor categories. One such category is that of representations of the biinfinite quiver $A_{\infty}^{\infty}$, where each object can be thought of as a biinfinite chain of $R$-modules. This raises the question of how the objects and morphisms of (model theoretic) interest for this category relate to those of $\operatorname{Mod}\ R$. In the simplest case, we take $R$ to be von Neumann regular.
Location: MALL
Title: The Axiom of Determinacy and Large Cardinals - Part 1: Strange Beginnings
The Axiom of Determinacy (AD) was proposed by Mycielski and Steinhaus in 1962. By then, it was already known that the Axiom of Choice (AC) implies the falsehood of AD, causing AD to be sidelined by many set-theorists. However, in 1967, Solovay showed that AD implies the measurability of ω1, and the new-found realisation that large cardinal properties are exhibited by small cardinals under AD contributed to the induction of AD into mainstream set-theoretic research.
This is a two-talk series that will culminate in Solovay’s results on some large cardinal properties exhibited by ω1 under AD (and its stronger counterpart ADR). In the first talk, we will lay the groundwork by introducing infinite games and defining AD, then discussing some of its pop-culture properties, such as its annihilation of the Banach-Tarski Paradox as well as its surprising implications on the real numbers (including the Continuum Hypothesis). If time permits, we will define a cardinal Θ that equals the successor of the continuum under AC, but can be much larger under AD.
