The 2022 Winter Meeting of the Association for Symbolic Logic was held on January 6–7, 2023, in conjunction with the annual Joint Mathematics Meeting. The program committee consisted of Dana Bartošová, Kirsten Eisenträger, James Freitag (chair), and Philipp Hieronymi.

The ASL program included six plenary speakers, a tutorial, two special sessions, and a contributed paper session. The ASL Special Sessions were Tame Geometry and Applications to Analysis organized by Alexi Block Gorman and Model-Theoretic and Higher Infinite Methods in Descriptive Set Theory Related Areas organized by Alexander Kechris, Rehana Patel, Alejandro Poveda, and Assaf Shani. The ASL Tutorial Hilberts’s Tenth Problem: between logic and number theory was given by Sylvy Anscombe. The plenary addresses at the meeting were:

• Jeremy Avigad (Carnegie Mellon), The promise of formal mathematics.

• Peter Cholak (Notre Dame), On Ramsey-like theorems on the rationals and the Rado graphs.

• Franziska Jahnke (Münster), Model theory of perfectoid fields.

• Sandra Müller (TU Wien), Universally Baire sets, determinacy, and inner models.

• Lynn Scow (Cal State San Bernardino), Semi-retractions and the Ramsey property.

• Assaf Shani (Harvard), Classifying invariants for Borel equivalence relations.

Abstracts of the invited talks and the contributed talks by members of the Association for Symbolic Logic follow.

Abstract of invited tutorial

▸SYLVY ANSCOMBE, Hilbert’s Tenth Problem: between logic and number theory.

Université Paris Cité and Sorbonne Université, CNRS, IMJ-PRG, F-75013 Paris, France. E-mail: sylvy.anscombe@imj-prg.fr.

The tenth of Hilbert’s Problems (H10), posed in 1900, asked for an algorithm to decide correctly whether or not a given polynomial $f\in \mathbb {Z}[X_{1},\ldots ,X_{n}]$ has a solution in $\mathbb {Z}$ . Culminating in 1970, work of Davis, Matiyasevich, Putnam, and Robinson showed that no such algorithm exists—a “negative solution” to H10. Since then, a body of work has developed tackling the analogous questions in a variety of other rings and fields, where one is interested in solutions in a ring R, and sometimes also with coefficients in R.

In these two tutorial lectures, I will focus on recent developments, both in the more “global” world of finitely generated fields (including the prominent open case $R=\mathbb {Q}$ ), and their subrings, and in the more “local” world of henselian valued fields, and their valuation rings.

Abstracts of invited plenary lectures

▸JEREMY AVIGAD, The promise of formal mathematics.

Department of Philosophy and Department of Mathematical Sciences, Carnegie Mellon University, Baker Hall 161, Pittsburgh, PA 15213, USA

E-mail: avigad@cmu.edu.

Since the early twentieth century, it has been understood that mathematical statements can be expressed in formal languages and that mathematical proofs can be represented in formal deductive systems with precise rules and semantics, at least in principle. Remarkably, the development of computational proof assistants over the last few decades has made it possible to do this in practice. The technology is firmly based on the methods and concepts of modern logic, and in many ways represents the contemporary embodiment of the foundational tradition.

I will give a brief overview of formally verified mathematics and the state of the field today. I will discuss a particular theorem prover, Lean, and its formal library, mathlib, which are attracting a growing community of users. I will explain why the technology is likely to have a transformative effect on mathematics, and I will explain why mathematical logicians might be interested in it.

▸PETER CHOLAK, On Ramsey-like theorems on the rationals and the Rado graph.

Department of Mathematics, University of Notre Dame, Notre Dame, IN, USA.

E-mail: cholak@nd.edu.

Ramsey theorem implies for every 2-coloring of pairs of naturals there is an infinite set H of naturals where all the pairs formed from H have the same color. We will explore how to extend this to the rationals, the Rado graph, and some other relational homogenous countable structures. One of the main tools used in these extensions is Milliken’s tree theorem and its recent modifications. Our goal is to try to understand the arithmetic complexity of the resulting “homogenous” set or structure, i.e., if the colorings are computable is there a “homogenous” structure within the arithmetical hierarchy and if so where.

▸FRANZISKA JAHNKE, Model theory of perfectoid fields.

Mathematical Institute and Institute for Mathematical Logic and Foundational Research, Department of Mathematics and Computer Science, University of Münster, Münster, Germany.

E-mail: franziska.jahnke@wwu.de.

Tilting perfectoid fields, developed by Scholze, allow to transfer results between certain henselian fields of mixed characteristic and their positive characteristic counterparts and vice versa. We present a model-theoretic approach to tilting via ultraproducts, which allows to transfer many first-order properties between a perfectoid field and its tilt (and conversely). In particular, our method yields a simple proof of the Fontaine–Wintenberger theorem which states that the absolute Galois group of a perfectoid field and its tilt are canonically isomorphic. This is joint work with Konstantinos Kartas.

▸SANDRA MÜLLER, Universally Baire Sets, determinacy, and inner models.

Institute of Discrete Mathematics and Geometry, TU Wien, Wiedner Hauptstrasse 8-10/104, 1040 Vienna, Austria.

E-mail: sandra.mueller@tuwien.ac.at.

URL Address: https://dmg.tuwien.ac.at/sandramueller/.

Computing the large cardinal strength of a given statement is one of the key research directions in set theory. Fruitful tools to tackle such questions are given by inner model theory. The study of inner models was initiated by Gödel’s analysis of the constructible universe L. Later, it was extended to canonical inner models with large cardinals, e.g., measurable cardinals, strong cardinals, or Woodin cardinals, which were introduced and studied by Jensen, Mitchell, Steel, Woodin, Sargsyan, and others. We will outline the role universally Baire sets play in the study of inner models and their connections to determinacy axioms. In particular, we will discuss recent results on $\mathsf {Sealing}$ , a formalization due to Woodin of the statement that the theory of the universally Baire sets cannot be changed by forcing.

▸DANA BARTOŠOVÁ AND LYNN SCOW $^*$ , Semi-retractions and the Ramsey property.

Department of Mathematics, University of Florida, Gainesville, FL, USA.

E-mail: dbartosova@ufl.edu.

Department of Mathematics, California State University, San Bernardino, CA, USA.

E-mail: lscow@csusb.edu.

Say that an injection $f:\mathcal {A} \rightarrow \mathcal {B}$ is quantifier-free type-respecting if finite tuples from $\mathcal {A}$ that share the same quantifier-free type in $\mathcal {A}$ are mapped by f to tuples in $\mathcal {B}$ that share the same quantifier-free type in $\mathcal {B}$ . For structures $\mathcal {A}$ and $\mathcal {B}$ in possibly different languages we say that $\mathcal {A}$ is a semi-retract of $\mathcal {B}$ if there are quantifier-free type-respecting injections $g: \mathcal {A} \rightarrow \mathcal {B}$ and $f: \mathcal {B} \rightarrow \mathcal {A}$ such that $f \circ g : \mathcal {A} \rightarrow \mathcal {A}$ is an embedding. Given a finitely generated substructure $A \subseteq C$ , define ${C \choose A}$ to be all substructures of C isomorphic to A. We say that an age $\mathcal {K}$ of finite structures has the Ramsey property $(RP)$ if for all $A, B \in \mathcal {K}$ and integers $k \geq 2$ there exists $C \in \mathcal {K}$ such that for any k-coloring $c : {C \choose A} \rightarrow k$ , there is $B' \in {C \choose B}$ such that for any $A', A" \in {B' \choose A \; }$ , $c(A') = c(A")$ . In [1], it was shown that if $\mathcal {A}$ and $\mathcal {B}$ are locally finite ordered structures and $\mathcal {A}$ is a semi-retract of $\mathcal {B}$ , then if the age of $\mathcal {B}$ has RP, the age of $\mathcal {A}$ has RP. In this talk we will present improvements on this result and comment on the connection to categorical notions in Ramsey theory.

[1] L. Scow, Ramsey transfer to semi-retractions. Annals of Pure and Applied Logic , vol. 172 (2021), no. 3, Article no. 102891, 18 pp.

▸ASSAF SHANI, Classifying invariants for Borel equivalence relations.

Department of Mathematics, Harvard University, Cambridge, MA, USA.

E-mail: shani@g.harvard.edu.

A classification problem is a pair $(X,E)$ where X is a collection of mathematical objects and E is a natural notion of equivalence (such as isomorphism). The theory of Borel equivalence relations provides a precise way to measure the complexity of various classification problems, and to study what types of invariants may, or may not, be available to successfully classify them.

In this talk I will focus on a hierarchy of complexity of classifying invariants, which was introduced by Hjorth, Kechris, and Louveau. After introducing the definitions and motivation, I will discuss its relevance in the study of natural classification problems, and some recent applications.

Abstracts of contributed talks

▸ATHAR ABDUL-QUADER, Arithmetically saturated models of $\mathsf {PA}$ and disjunctive triviality.

School of Natural and Social Sciences, SUNY Purchase College, 735 Anderson Hill Road, Purchase, NY 10577, USA.

E-mail: athar.abdulquader@purchase.edu.

Kotlarski, Krajewski, and Lachlan [3] showed that the theory $\mathsf {CT}^-$ of a model of $\mathsf {PA}$ augmented by a full truth predicate is conservative over $\mathsf {PA}$ . Recently, Enayat and Pakhomov [2] showed that the theory $\mathsf {CT}^- + \mathsf {DC}$ asserting that the full truth predicate is disjunctively correct is in fact equivalent to $\mathsf {CT}_0$ , the theory asserting $\Delta _0$ induction in the language augmented with the truth predicate. In the absence of $\Delta _0$ induction, however, various pathologies can emerge, including models in which the truth predicate evaluates all nonstandard disjunctions as true [1]. We show that such models must be arithmetically saturated. In fact, we show that a countable, recursively saturated $\mathcal {M} \models \mathsf {PA}$ has an expansion to a model of $\mathsf {CT}^-$ in which all nonstandard disjunctions are evaluated as true if and only if $\mathcal {M}$ is arithmetically saturated. This is joint work with Mateusz Łełyk, drawing heavily on an unpublished note by James Schmerl.

[1] C. Cieśliński, M. ŁEłyk, and B. Wcisło, The two halves of disjunctive correctness. Journal of Mathematical Logic , to appear. doi:10.1142/S021906132250026X.

[2] A. Enayat and F. Pakhomov, Truth, disjunction, and induction. The Archive for Mathematical Logic , vol. 58 (2019), pp. 753–766.

[3] H. Kotlarski, S. Krajewski, and A.H. Lachlan, Construction of satisfaction classes for nonstandard models. Canadian Mathematical Bulletin . vol. 24 (1981), pp. 283–293.

▸JANANAN ARULSEELAN, The undecidability of having the QWEP.

Department of Mathematics & Statistics, McMaster University, Hamilton, ON, Canada.

E-mail: arulseej@mcmaster.ca.

This talk will be about computability theoretic aspects of the continuous logic of operator algebras. We will discuss the uncomputability of the universal theories of Powers’ factors and the hyperfinite factor. We will then use this result to prove that there is no computable theory of C $^*$ -algebras (or W $^*$ -probability spaces) with the QWEP property.

▸KATALIN BIMBÓ, Embeddings of De Morgan monoids in Boolean lattices.

Department of Philosophy, University of Alberta, 2–40 Assiniboia Hall, Edmonton, AB T6G 2E7, Canada.

E-mail: bimbo@ualberta.ca.

URL Address: www.ualberta.ca/∖char126bimbo.

A distributive lattice can be embedded into a ring of sets, and a De Morgan lattice can be embedded into a Boolean algebra ( $\mathbf {BA}$ ). The Lindenbaum algebra of the relevance logic $\mathbf {R}^t$ is a De Morgan monoid ( $\mathbf {DM}$ ). A $\mathbf {DM}$ can be embedded into a (complete) $\mathbf {BA}$ via a ternary relation (defined from the $\mathbf {DM}$ ), the existential image of which defines the semi-group operation ( $\circ $ ). The properties of $\circ $ are retained in the $\mathbf {BA}$ , but the identity element might not function as an identity for all elements. I will explain (in terms of closure properties of the elements of the $\mathbf {BA}$ ) that the ternary relation encodes too much information about the $\mathbf {DM}$ and I will show how to amend the construction.

▸DANIEL MOURAD, Computing non-repetitive sequences using the Lovász local lemma.

University of Connecticut, Storrs, CT, USA.

E-mail: daniel.mourad@uconn.edu.

We discuss effective versions of classical results on the existence of certain non-repetitive sequences first proven using the Lovász local lemma, a non-constructive existence result from the probabilistic method. We outline the path to these constructions. First, a probabilistic resample algorithm by Moser and Tardos [1] converges to a witness to the local lemma in polynomial expected time. Then, Rumyantsev and Shen [2] show that the bound on the expectation is used to build a deterministic algorithm with computable convergence time. However, the resulting effective computation has constraints that make it unsuitable for constructing non-repetitive sequences. Sourcing from Pegden’s lefthanded local lemma [3], we modify the resample algorithm to relax these constraints.

[1] R. A. Moser and G. Tardos, A constructive proof of the general lovász local lemma. Journal of the Association for Computing Machinery , vol. 57 (2010), no. 2, pp. 1–12.

[2] A. Rumyantsev and A. Shen, Probabilistic constructions of computable objects and a computable version of Lovász local lemma. Fundamenta Informaticae , vol. 132 (2014), no. 2, pp. 1–14.

[3] W. Pegden, Highly nonrepetitive sequences: Winning strategies from the local lemma. Random Structures & Algorithms , vol. 38 (2011), nos. 1–2, pp. 140–161.

▸CARL MUMMERT, Reverse mathematics and Banach’s theorem.

Marshall University, Huntington, WV, USA.

E-mail: mummertc@marshall.edu.

Reverse mathematics is a field in mathematical logic that measures the set existence axioms needed to prove mathematical theorems, and the amount of noncomputability inherent in the theorems. To make this analysis precise, the theorems are formulated in systems of formal arithmetic. Much research in reverse mathematics has been carried out in second-order arithmetic. More recently, initial work on reverse mathematics in higher-order arithmetic has begun.

This talk focuses on one case: the higher-order reverse mathematics of a theorem of Banach that strengthens the Schroeder–Bernstein theorem. This result states that if $f\colon A \to B$ and $g \colon B \to A$ are injections, then there is a bijection $h \colon A \to B$ such that, for all $x \in A$ , either $h(x) = f(x)$ or $g(h(x)) = x$ .

The strength of Banach’s theorem formulated in second-order arithmetic, with $A = B = \mathbb {N}$ , has been studied by Remmel and by Hirst. We will discuss the strength of formulations of Banach’s result in higher order arithmetic, with $A= B = 2^{\mathbb {N}}$ or $A = B = {\mathbb {N}}^{\mathbb {N}}.$

This is joint work with Jeffry Hirst.

▸DAN TURETSKY, Limit complexities and minimal descriptions.

School of Mathematics and Statistics, Victoria University of Wellington, Wellington, New Zealand.

E-mail: dan.turetsky@vuw.ac.nz.

Building off a result of Bienvenu, Muchnik, Shen, and Vereshchagin, we study Kolmogorov complexity conditioned on minimal codes. With this, we obtain an oracle-free definition of $K^{0'}$ , and thus of 2-randomness.

[1] L. Bienvenu, An. A. Muchnik, A. Shen, and A. Vereschagin, Limit complexities revisited. Theory of Computing Systems , vol. 47 (2010), no. 3, pp. 720–736.

Abstracts of talks presented by title

▸JOACHIM MUELLER-THEYS, The Refutation of Alternativeism II.

Independent, Heidelberg, Germany.

E-mail: mueller-theys@gmx.de.

$\Phi \vdash \psi $ or $ \Phi \vdash \chi $ implies $ \Phi \vdash \psi \vee \chi $ . We call $ \vdash \ \subseteq \wp ( L ) \times L $ alternativeist if the converse is true (too). This specifies the intuitionist view that an alternation is provable only if some of its components is provable.

We say that $ \phi : = \psi \vee \chi $ is $\Phi $ -essential if $ \Phi \vdash \phi $ , but neither $ \Phi \models \psi $ nor $ \Phi \models \chi $ , whereby $ \models $ be sound for $ \vdash $ . The existence of essential alternations denies alternativeism.

Proof. (i) $x < c \vee x = c \vee x> c$ . If $ x < c $ , by $ c < d $ , $ x < d $ , whence $ x> c \vee x < d $ . If $ x = c $ , again $ x < d $ , whence the claim. If $ x> c $ , the claim. (ii) Let, e.g., $ | {\mathcal M} | : = \{ 0, 1 \} $ , $ c ^{\mathcal M} : = 0 $ , $ d ^{\mathcal M} : = 1 $ , $ < ^{\mathcal M} : = \{ ( 0 , 1) \} $ . Thence $ {\mathcal M} \models \Phi $ , but, for $ a : = 0 $ , $ b := 1 $ , $ {\mathcal M} \, ^x / _a \not \models x> c $ , $ {\mathcal M} \, ^x / _b \not \models x < d $ .

Our general, abstract refutation has been different. Cf. “The Refutation of Alternativeism,” XIX SLALM 2022 (CIMPA, Costa Rica), Résumenes (p. 58), to appear in The Bulletin of Symbolic Logic.

We now call $ \phi = \psi \vee \chi $ self-essential if(f) $ \phi $ is $ \{ \phi \} $ -essential. Since $ \phi \vdash \phi $ , $\phi $ is self-essential iff $ \phi \not \models \psi $ and $ \phi \not \models \chi $ iff $ \psi $ , $ \chi $ are logically independent, viz. $ \psi \not \models \chi $ and $ \chi \not \models \psi $ . For instance, sentential $ p \vee q $ has been (self-)essential.

Buchholz pushed the analysis further, which we included in a paper of the same name from August, stimulated by the symposium. With $ \neg $ : $ L \to L $ and $ {\mathcal I} \models \neg \psi $ iff $ {\mathcal I} \not \models \psi $ , curiously, $ \models \psi $ iff $\neg \psi \models \psi $ , $ \models \neg \psi $ iff $\psi \models \neg \psi $ , whereby $\psi $ , $\neg \psi $ are logically independent if and only if $\psi $ is logically contingent, viz. $\not \models \psi , \neg \psi $ . Hence, if $ \psi $ is logically contingent, $ \phi : = \psi \vee \neg \psi $ is self-essential, and vice versa. Thus, $ \vdash $ is not alternativeist given that, evidently, there is some logically contingent formula (Beziau Axiom). For instance, $ p $ , $ P ( c )$ are logically contingent.