The 2025 North American Annual Meeting of the Association for Symbolic Logic was held at New Mexico State University in Las Cruces, New Mexico, May 13–16, 2025. There were six plenary talks, two tutorials, six special sessions, and four sessions of contributed talks. A welcoming reception was held on Tuesday, May 13.

The program committee consisted of Uri Andrews, Valeria de Paiva, Ilya Shapirovsky, Caroline Terry, and Simon Thomas (chair). The local organizing committee consisted of John Harding (chair), Andre Kornell, Joel Lucero-Bryan, Patric Morandi, Bruce Olderding, Ilya Shapirovsky, and Son Tran.

There were 130 participants at the meeting, of which 57 were graduate students. Generous financial support was provided by the Association for Symbolic Logic, the National Science Foundation, and numerous entities at New Mexico State University including the College of Arts and Sciences, the NMSU Provost, the Charles and Nita Swartz Endowment, and the Kist Endowment. The plenary addresses given at the meeting were:

Sergei Artemov (Graduate Center CUNY), Consistency of PA is a serial property, and it is provable in PA .

Benjamin Castle (University of Illinois), Reconstruction problems in geometry via model theory.

Patrick Lutz (UC Berkeley), Measure hyperfiniteness and lossless expansion.

Maryanthe Malliaris (University of Chicago), New perspectives on model-theoretic complexity.

Alejandro Poveda (Harvard University), Recent developments on the theory of supercompact cardinals.

Felix Weilacher (UC Berkeley), Separating complexity classes of LCL problems on grids.

There were two tutorials, each consisting of three 50-minute sessions.

Mariya Soskova (University of Wisconsin), Enumeration reducibility and effective mathematics.

Julia Wolf (University of Cambridge), An introduction to higher order stability.

The special sessions at this meeting were Combinatorics and Logic (Artem Chernikov, Damir Dzhafarov, and Andrew Marks), Computability Theory (Turbo Ho and Manlio Valenti), Modal Logic (Wesley Holliday and Ilya Shapirovsky), Model Theory (Gabe Conant and Nick Ramsey), Proof Assistants (Patricia Johann and Jon Weinberger), and Set Theory (Dima Sinapova and Clinton Conley). The program included ten contributed talks.

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

For the Program Committee

Simon Thomas

Abstract of invited tutorial

▸MARIYA I. SOSKOVA, Enumeration reducibility and effective mathematics.

University of Wisconsin–Madison, 480 Lincoln Dr, Madison WI 53706, USA.

E-mail: soskova@wisc.edu.

Relative computability allows us to compare incomputable sets with respect to their algorithmic complexity. The most widely studied way to do this was introduced by Turing [3]: a set of natural numbers X is Turing reducible to a set of natural numbers Y if there is an algorithm to determine whether $n\in X$ when given Y as data.

Turing reducibility between sets of natural numbers allows us to gauge the algorithmic content of a mathematical object, such as a real number or a continuous function. For example, Moschovakis [2] observed that every continuous function is computable relative to some fixed Turing oracle, thus understanding relatively computable functions gives a different perspective on the study of continuous functions on the reals. This point of view belongs to effective mathematics. However, Turing reducibility is not well suited to handle partial information: suppose that instead of total access to the membership in the oracle, we are only given access to the positive information. Friedberg and Rogers [1] capture this extended model of relative computability: X is enumeration reducible to Y if there is an algorithm to enumerate X given any enumeration of Y.

Each reducibility induces a partial order, its degree structure, in which we identify sets that are reducible to each other. There is a way to express Turing reducibility using enumeration reducibility and so we can view the Turing degrees $\mathcal {D}_T$ as a proper substructure of the enumeration degrees $\mathcal {D}_e$ . Understanding the algebraic profile of the larger structure results in a better understanding of the smaller one. We need both Turing and enumeration reducibility to study effective mathematics. In this tutorial, we will explore various aspects of enumeration reducibility, the induced degree structure, as well as its relationship to the Turing degrees and to effective mathematics.

[1] R. M. Friedberg and H. Rogers, Jr., Reducibility and completeness for sets of integer. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , vol. 5 (1959), pp. 117–125.

[2] Y. N. Moschovakis, Descriptive Set Theory , Studies in Logic and the Foundations of Mathematics, North-Holland, 1980.

[3] A. M. Turing, Systems of logic based on ordinals. Proceedings of the London Mathematical Society , vol. 45 (1939), no. 3, pp. 161–228.

▸JULIA WOLF, An introduction to higher arity stability.

Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, Centre for Mathematical Sciences, Wilberforce Road, Cambridge CB3 0WB, UK.

E-mail: julia.wolf@dpmms.cam.ac.uk.

For more than half a century, the model-theoretic notion of stability has played a fundamental role in describing tame behaviour, with numerous manifestations across algebra, number theory, and combinatorics. In the latter setting, Malliaris and Shelah showed in 2014 that graphs whose edge relation is stable satisfy a particularly strong version of Szemerédi’s regularity lemma, a key tool in extremal combinatorics and theoretical computer science since the late 1970s. In this tutorial, I will explain how higher-order generalisations of Szemerédi’s regularity lemma, which emerged in the early 2000s in groundbreaking work of Gowers and independently Rödl–Nagle–Skokan–Schacht, have recently pointed the way towards a long-sought generalisation of stability, beyond the case of binary formulas.

We begin by recalling the definitions of stability and $\mathrm {NIP}$ , before surveying a cascade of results inspired by Malliaris–Shelah, both in the setting of graphs and finite groups. In particular, we aim to draw out the distinct roles that stability and $\mathrm {NIP}$ play in the context of regularity decompositions, as well as the connection between regularity decompositions of finite groups and the model-theoretic “connected component”.

We then motivate the ternary notions $\mathrm {NIP}_2$ , introduced by Shelah in 2017, and $\mathrm {NFOP}_2$ , introduced in joint work with Terry in 2021, and show how their implications in the setting of regularity lemmas for 3-uniform hypergraphs provide compelling evidence for the claim that these two notions do indeed constitute higher-arity analogues of $\mathrm {NIP}$ and stability, respectively.

If time permits, we will give an overview of the most recent literature on $\mathrm {NFOP}_k$ , including work of Abd-Aldaim–Conant–Terry and Boissonneau–Papadopoulos–Touchard.

Abstracts of invited plenary lectures

▸SERGEI ARTEMOV, Consistency of PA is a serial property, and it is provable in PA.

Graduate Center CUNY, 365 Fifth Ave., New York City, NY 10016, USA.

E-mail: sartemov@gc.cuny.edu.

We revisit the question of whether the consistency of Peano Arithmetic PA can be established in PA. First, we show that Gödel’s Second Incompleteness theorem, G2, does not imply a negative answer to this question. Then, we reconfigure Hilbert’s epsilon-substitution method of proving consistency and use partial truth definitions to establish PA consistency in PA.

The consistency of a theory means that all its formal derivations are free of contradictions. Derivations are finite syntactic objects, and their Gödel codes are all standard natural numbers. Such numbers can be identified with numerals $\overline {0},\overline {1},\overline {2},\ldots ,\overline {n}\ldots $ in the language of PA (we’ll drop overlines for better readability). Let $x\!:\!y$ denote the standard primitive recursive proof predicate in PA “x is code of a proof of a formula having code y” and $\bot $ stand for the formula $(0\!=\!1)$ . Consider the series of formulas, consistency scheme, $\mathsf {Con}^S_{\mathsf {PA}}$ :

Since Gödel numbering and proof predicate represent the structure of proofs adequately, $\mathsf {Con}^S_{\mathsf {PA}}$ holds iff PA is consistent.

Although the scheme $\mathsf {Con}^S_{\mathsf {PA}}$ fairly represents PA consistency in the form compatible with the language of PA, $\mathsf {Con}^S_{\mathsf {PA}}$ is not within the scope of the usual provability in PA defined for individual formulas. To address the provability of consistency question, we have either

1. 1. to reformulate consistency as a single PA-formula or

2. 2. to extend the notion of PA-proofs to serial properties in a way formalizable in PA.

For (1), logicians have traditionally considered the consistency formula $\mathsf {Con}_{\mathsf {PA}}$ :

in which the informal quantifier “for all numerals” hidden in $\mathsf {Con}^S_{\mathsf {PA}}$ is replaced by the formal PA-quantifier “ $\forall x$ .” The problem with the consistency formula is that in PA, $\mathsf {Con}_{\mathsf {PA}}$ is strictly stronger than $\mathsf {Con}^S_{\mathsf {PA}}$ , hence than PA consistency. Here are some justifications for this claim.

• • Conceptual: “for all numerals” quantifies over standard numbers $0,1,2,\ldots ,n\ldots $ and PA consistency is known to hold for each of them. The range of “ $\forall x$ ” includes also nonstandard numbers and, by G2, “ $ \neg (x\!:\!\bot )$ ” can fail on some nonstandard x.

• • Proof theoretic: $\mathsf {Con}_{\mathsf {PA}}$ yields all of $\mathsf {Con}^S_{\mathsf {PA}}$ , but PA + $\mathsf {Con}^S_{\mathsf {PA}}$ does not yield $\mathsf {Con}_{\mathsf {PA}}$ .

• • Model theoretic: in the context of PA provability, we have to consider all models of PA, not just the standard model. $\mathsf {Con}^S_{\mathsf {PA}}$ holds in all models whereas $\mathsf {Con}_{\mathsf {PA}}$ , by G2, fails in some nonstandard models of PA.

Therefore, the unprovability of $\mathsf {Con}_{\mathsf {PA}}$ in PA does not answer the question about the provability of PA consistency in PA.

For (2), extending the notion of finite proof to serial properties in PA is imperative. The one formula provability is not directly applicable in metamathematics, where many basic principles are serial properties. We cannot even directly prove in PA its own induction principle or that the product of any two polynomials is a polynomial. For these and similar serial properties F, mathematicians de facto accept corresponding contentual selector proofs: PA proves that each instance of F is provable. When selector proofs are defined rigorously, the consistency scheme $\mathsf {Con}^S_{\mathsf {PA}}$ becomes provable in PA.

Other reference points for selector proofs are Hilbert’s epsilon substitution method and Brouwer–Heyting–Kolmogorov proofs of universal statements (cf. the detailed discussion in [2]).

This work refutes the Unprovability of Consistency thesis, UoC, and it removes a principal roadblock of Hilbert’s consistency program.

The selector proof of PA consistency was given in [1, 2]. Selector proofs in a general setting have been discussed in [2, 3, 6]. Some technical results useful for the theory of selector proofs were found in [5]. Selector proofs have also been explored by Elijah Gadsby, whose presentation was submitted for this conference. In [4] and in further publications, Detlefsen rejected the G2-based justification of UoC from philosophical finitistic positions. Our work refutes UoC on mathematical grounds and proves PA consistency in PA.

[1] S. Artemov, The provability of consistency, preprint, 2019, arXiv:1902.07404.

[2] ———, Serial properties, selector proofs and the provability of consistency. Journal of Logic and Computation , 2024, p. exae034.

[3] Y. Cheng, Current research on Gödel’s incompleteness theorems. The Bulletin of Symbolic Logic , vol. 27 (2021), no. 2, pp. 113–167.

[4] M. Detlefsen, On interpreting Gödel’s second theorem. Journal of Philosophical Logic , vol. 8 (1979), pp. 297–313.

[5] A. Ignjatović, Hilbert’s program and the omega-rule. The Journal of Symbolic Logic , vol. 59 (1994), no. 1, pp. 322–343.

[6] P. G. Santos, W. Sieg, and R. Kahle, A new perspective on completeness and finitist consistency. Journal of Logic and Computation , vol. 34 (2024), no. 6, pp. 1179–1198, exad021.

▸BENJAMIN CASTLE, Reconstruction Problems in Geometry via Model Theory.

Department of Mathematics, University of Illinois Urbana–Champaign, Urbana, IL, USA.

E-mail: btcastl2@illinois.edu.

In algebraic geometry, reconstruction problems ask for the recovery of an algebraic variety from a restricted set of data. The idea is to determine when a smaller amount of algebraic structure is enough to recover all algebraic structure. Geometers typically formulate such problems categorically—however, a natural equivalent formulation is often possible using definability in a certain first-order language. In this talk, I will explain the basic set up of relics and full relics of a first-order structure, and show how—by observations of Zilber—reconstruction problems really amount to determining which relics of a field are full. I will then discuss how powerful tools in stability theory have recently led to a series of classification theorems for relics of fields. Time permitting, I will then give a survey of a new reconstruction theorem in algebraic geometry which was proven using the model-theoretic setup above.

▸PATRICK LUTZ, Measure hyperfiniteness and lossless expansion.

Department of Mathematics, University of California Berkeley, Berkeley, CA, USA.

E-mail: pglutz@berkeley.edu.

The structure of the class of countable Borel equivalence relations under Borel reducibility has been a major focus of descriptive set theory over the past few decades. However, many open questions remain, a number of which involve the class of hyperfinite equivalence relations (essentially the simplest nontrivial countable Borel equivalence relations). In order to better understand these questions, Conley and Miller introduced a weakening of Borel reducibility, known as measure reducibility. They then answered the analogues for measure reducibility of several open questions involving hyperfinite equivalence relations. However, they left open at least one such question. Namely, is there a minimal non-hyperfinite equivalence relation under the relation of measure reducibility? Such an object is called a “measure successor of $E_0$ .” In ongoing work, Jan Grebík and I have isolated a combinatorial property of group actions on Polish spaces which implies that the associated orbit equivalence relation is a measure successor of $E_0$ . We have also identified several examples of group actions which are plausible candidates for satisfying this condition. The combinatorial property we have identified is a strong form of graph expansion which we call “lossless expansion” after a similar property studied in computer science and combinatorics. I will explain the context for Conley and Miller’s question and the combinatorial condition that Grebík and I have isolated and then sketch the main ideas which relate this combinatorial condition to hyperfiniteness.

▸MARYANTHE MALLIARIS, New perspectives on model-theoretic complexity.

Department of Mathematics, University of Chicago, 5734 S. University Avenue, Chicago IL 60637, USA.

E-mail: mem@math.uchicago.edu.

Part of the power of model-theoretic dividing lines comes from having many different equivalent definitions. The talk will discuss several recent theorems in which certain model-theoretic dividing lines appear inherently in other fields, and consider what this means on both sides.

▸ALEJANDRO POVEDA, Recent developments on the theory of supercompact cardinals.

Department of Mathematics and Center of Mathematical Sciences and Applications, Harvard University, 20 Garden St, Cambridge, MA, USA.

E-mail: alejandro@cmsa.fas.harvard.edu.

In this presentation, we will report on some recent progress on the theory of supercompact cardinals. We will begin presenting various consistency results as well as a conjecture about how the large-cardinal hierarchy of Woodin’s Ultimate-L looks like at these latitudes. One of our main theorems is the consistency of every supercompact cardinal being supercompact with inaccessible targets, which answers questions by Bagaria and Magidor. This configuration follows from a new axiom we introduce (Axiom $\mathcal {A}$ ) which is shown to be consistent with all known large cardinals. We will show that axiom $\mathcal {A}$ yields a Scott-like theorem for Ultimate-L.

▸FELIX WEILACHER, Separating complexity classes of LCL problems on grids.

Department of Mathematics, University of California Berkeley, 970 Evans Hall, MC 3840 Berkeley, CA 94720, USA.

E-mail: weilacher@berkeley.edu.

A locally checkable labeling (LCL) problem on a finitely generated group $\Gamma $ asks one to find a labeling of Cayley graph of $\Gamma $ satisfying a fixed, finite set of “local” constraints. Such a labeling can equivalently be described as an element of some $\Gamma $ -subshift of finite type.

How hard is it to solve a particular LCL problem? We consider this question from the point of view of several fields that might be lumped together under the term definable combinatorics. The common theme is that we are given a free action of $\Gamma $ , and want to solve the LCL problem in a “uniform” way on the orbits. For example, in descriptive set theory, we might have a continuous action of $\Gamma $ on a Polish space and wish to solve the problem in a continuous, Borel, etc. way. In computability theory, we might have an action of $\Gamma $ on $\mathbb {N}$ and wish to solve the problem in a computable way.

We study the case $\Gamma = \mathbb {Z}^n$ , where we separate various “complexity classes” in definable combinatorics which were not previously known to be distinct. For example, we construct LCL problems on $\mathbb {Z}^n$ which $\ldots $

• • Have measurable solutions but not necessarily Borel solutions for actions on standard probability spaces.

• • Have computable solutions but not necessarily Baire measurable solutions.

• • Can be solved as a factor of i.i.d. variables on $\mathbb {Z}^n$ , but not as a so-called “finitary” factor.

The first and third items resolve questions of Grebík and Rozhoň. The second and third items are the first examples of such separation for any group.

This is joint work with Katalin Berlow, Anton Bernshteyn, and Clark Lyons.

Abstracts of invited talks in the Special Session on Combinatorics and Logic Theory

▸SAUGATA BASU AND DEEPAM PATEL, Cohomological VC-density: bounds and applications.

Department of Mathematics, Purdue University, 150 N. University st., West Lafayette, IN 47907, USA.

E-mail: sbasu@math.purdue.edu.

E-mail: patel471@purdue.edu.

The concept of Vapnik–Chervonenkis (VC) density is pivotal across various mathematical fields, including model theory, discrete geometry, and probability theory. In this article, we introduce a topological generalization of VC-density. Let Y be a topological space and $\mathcal {X},\mathcal {Z}^{(0)},\ldots ,\mathcal {Z}^{(q-1)}$ be families of subspaces of Y. We define a two parameter family of numbers, $\mathrm {vcd}^{p,q}_{\mathcal {X},\overline {\mathcal {Z}}}$ , which we refer to as the degree p, order q, VC-density of the pair

The classical notion of VC-density within this topological framework can be recovered by setting $p=0, q=1$ . For $p=0, q> 0$ , we recover Shelah’s notion of higher-order VC-density for q-dependent families [4]. Our definition introduces a new notion when $p>0$ .

We examine the properties of $\mathrm {vcd}^{p,q}_{\mathcal {X},\overline {\mathcal {Z}}}$ when the families $\mathcal {X}$ and $\mathcal {Z}^{(i)}$ are definable in structures with some underlying topology (for instance, the analytic topology over $\mathbb {C}$ , the etale site for schemes over arbitrary algebraically closed fields, or the Euclidean topology for o-minimal structures over $\mathbb {R}$ ). Our main result establishes that in any model of these theories

This result generalizes known VC-density bounds in these structures [3, 2, 1], extending them in multiple ways, as well as providing a uniform proof paradigm applicable to all of them. We give examples to show that our bounds are optimal. Moreover, our bounds on $0/1$ -patterns actually goes beyond model-theoretic contexts: they apply to arbitrary correspondences of schemes with respect to singular, étale, or $\ell $ -adic cohomology theories. A particular consequence of our results is the extension of the bound on $0/1$ -patterns for definable families in affine spaces over arbitrary fields, as initially proven in [3], to general schemes.

We present combinatorial applications of our higher-degree VC-density bounds, deriving topological analogs of well-known results such as the existence of $\varepsilon $ -nets and the fractional Helly theorem. We show that with certain restrictions, these results extend to our higher-degree topological setting.

[1] M. Aschenbrenner, A. Dolich, D. Haskell, D. Macpherson, and S. Starchenko, Vapnik-Chervonenkis density in some theories without the independence property, I. Transactions of the American Mathematical Society , vol. 368 (2016), no. 8, pp. 5889–5949.

[2] S. Basu, Combinatorial complexity in o-minimal geometry. Proceedings of the London Mathematical Society. Third Series , vol. 100 (2010), no. 2, pp. 405–428.

[3] L. Rónyai, L. Babai, and M. Ganapathy, On the number of zero-patterns of a sequence of polynomials. Journal of the American Mathematical Society , vol. 14 (2001), no. 3, pp. 717–735.

[4] S. Shelah, Strongly dependent theories. Israel Journal of Mathematics , vol. 204 (2014), no. 1, pp. 1–83.

▸CHRIS CONIDIS, The computability of the uniform Krull intersection theorem.

College of Staten Island, 2800 Victory Boulevard, Staten Island, NY 10314, USA.

E-mail: chris.conidis@csi.cuny.edu.

The Krull intersection theorem ( $\mathsf {KIT}$ ) [1, Theorem 8.9] says that if I is an ideal in a Noetherian integral domain R, then $0$ is the only element contained in every power of I. We examine the computability properties of $\mathsf {KIT}$ , especially in the uniform context. More precisely, we can show that while the classical proof of uniform Krull implies comprehension for two quantifier predicates, there is also logically simpler argument.

[1] H. Matsumura, Commutative Ring Theory , Cambridge University Press, 2006.

▸DAVID GONZALEZ, Ramsey-theor etic statements motivated by generic computability.

Department of Mathematics, University of California Berkeley, Evans Hall, University Dr, Berkeley, CA 94720, USA.

E-mail: david_gonzalez@berkeley.edu.

Calvert, Cenzer, and Harizanov introduced several notions of dense computability for countable structures. These tools are used to understand the computable structure theory for weaker, approximate forms of computability. That said, a turn in recent work has revealed that understanding some of these notions is far more structural than initially expected. Efforts in the area have moved in part to studying the substructure relation and its stronger, more elementary counterparts. In particular, looking for well-behaved substructures and elementary substructures of a class of structures in a manner analogous to Ramsey’s theorem is key to understanding the generic computability of those structures.

This talk will focus on the structural Ramsey-like theorems that have emerged from this line of research. We will also discuss how and to what extent these results are related to questions regarding generic computability. New results regarding notions of generic categoricity will be emphasized.

This talk is based on joint work with Wesley Calvert, Doug Cenzer, and Valentina Harizanov.

▸CECELIA HIGGINS, Complexity of finite Borel asymptotic dimension.

Department of Mathematics, University of California Los Angeles, 520 Portola Plaza, Los Angeles, CA 90095, USA.

E-mail: ceceliahiggins@math.ucla.edu.

A Borel graph is hyperfinite if it can be written as a countable increasing union of Borel graphs with finite components. It is a major open problem in descriptive set theory to determine the complexity of the set of hyperfinite Borel graphs. In a recent paper, Conley, Jackson, Marks, Seward, and Tucker-Drob introduce the notion of Borel asymptotic dimension, a definable version of Gromov’s classical notion of asymptotic dimension, which strengthens hyperfiniteness and implies several nice Borel combinatorial properties. We show that the set of locally finite Borel graphs having finite Borel asymptotic dimension is $\boldsymbol {\Sigma }^1_2$ -complete. This is joint work with Jan Grebík.

▸SAM MURRAY, Borel fractional perfect matchings in quasi-transitive amenable graphs.

Department of Mathematics and Statistics, McGill University, 845 Sherbrooke St W, Montreal, QC, Canada.

E-mail: samuel.murray@mail.mcgill.ca.

In this talk, we show that if a locally finite Borel graph with quasi-transitive amenable components admits a fractional perfect matching, it will admit a Borel fractional perfect matching. In particular, if a countable amenable quasi-transitive graph admits a fractional perfect matching then its Bernoulli graph admits a Borel fractional perfect matching.

▸REHANA PATEL, Countable infinitary theories admitting an invariant measure.

Department of Mathematics and Computer Science, Wesleyan University, 265 Church Street, Middletown, CT 06459, USA.

E-mail: rpatel@wesleyan.edu.

The notion of “probabilistic structure” has a long history going back at least to Gaifman in 1964. In a modern framing, these probabilistic structures are closely related to probability measures on the class of structures in a fixed countable language with underlying set $\mathbb {N}$ that are invariant under the logic action. The ergodic such invariant measures, which we call ergodic structures, are of particular interest because they admit a satisfaction relation with respect to sentences of the infinitary logic $L_{\omega _1\omega }$ . In this talk, we will describe some aspects of a model theory for this satisfaction relation. This is joint work with Nathanael Ackerman and Cameron Freer.

▸THEODORE A. SLAMAN, Cauchy subsequences and the cohesiveness principle.

Department of Mathematics, University of California Berkeley, Berkeley, CA, USA.

E-mail: slaman@berkeley.edu.

One of the tenets of Reverse Math is that every basic theorem in a typical undergraduate mathematics curriculum is equivalent to one of the “Big Five”: Recursive Comprehension, Weak Kőnig’s Lemma, Arithmetic Comprehension, Arithmetic Transfinite Recursion, or $\Pi ^1_1$ -comprehension. The restriction to typical undergraduate mathematics is necessary since there is a well-documented zoo of combinatorial counter-examples, especially within Ramsey Theory. Counter to the Big-Five-Tenet, one of these combinatorial examples, the Cohesiveness Principle, is formally equivalent to the statement “Every totally bounded sequence of rational numbers has a Cauchy subsequence.” This same statement can be used to highlight the role of non-effective methods within a first undergraduate course on Mathematical Logic.

▸ATTICUS STONESTROM, An arithmetic algebraic regularity lemma.

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

E-mail: atticusstonestrom@yahoo.com.

In [6], Tao proved an ‘algebraic regularity lemma’ for families of graphs uniformly definable in finite fields, which improves the conclusions of Szemerédi’s regularity lemma in that setting. I will present an ‘arithmetic’ version of this theorem, i.e., a version for uniformly definable subsets of uniformly definable groups; this follows in the vein of papers, such as [1], [2], [3], [7], and [8] in giving good structure theorems for subsets of groups satisfying additional combinatorial hypotheses.

The precise statement of the theorem is the following: for any $M>0$ , any finite field $\mathbf {F}$ , and any definable group $(G,\cdot )$ in $\mathbf {F}$ and definable subset $D\subseteq G$ , each of complexity at most M, there is a normal definable subgroup $H\leqslant G$ , of index and complexity $O_M(1)$ , such that the following holds: for any cosets $V,W$ of H, the bipartite graph $(V,W,xy^{-1}\in D)$ is $O_M(|\mathbf {F}|^{-1/2})$ -quasirandom.

When G is the additive group of the field, this result relates in a similar way to Green’s theorem from [5] as Tao’s result relates to Szemerédi regularity. On the opposite end of the spectrum, when G is the $\mathbf {F}$ -points of a simply-connected semisimple algebraic group over $\mathbf {F}$ , the result is connected to and largely subsumed by Gowers’ work in [4].

This is joint work with Anand Pillay.

[1] N. Alon, J. Fox, and Y. Zhao, Efficient arithmetic regularity and removal lemmas for induced bipartite patterns. Discrete Analysis , vol. 3 (2019).

[2] G. Conant, A. Pillay, and C. Terry, A group version of stable regularity. Mathematical Proceedings of the Cambridge Philosophical Society , vol. 168, (2020), no. 2, pp. 405–413.

[3] G. Conant, A. Pillay, and C. Terry, Structure and regularity for subsets of groups with finite VC-dimension. Journal of the European Mathematical Society , vol. 24 (2022), no. 2, pp. 583–621.

[4] T. Gowers, Quasirandom groups. Combinatorics, Probability, and Computing , vol. 17 (2008), no. 3, pp. 363–387.

[5] B. Green, A Szemeredi-type regularity lemma in abelian groups, with applications. Geometric and Functional Analysis , vol. 15 (2005), pp. 340–376.

[6] T. Tao, Expanding polynomials over finite fields of large characteristic and a regularity lemma for definable sets. Contributions to Discrete Mathematics , vol. 10 (2015), no. 1, pp. 22–98.

[7] C. Terry and J. Wolf, Stable arithmetic regularity in the finite field model. Bulletin of the London Mathematical Society , vol. 51 (2019), no. 1, pp. 70–88.

[8] ———, Quantitative structure of stable sets in finite abelian groups. Transactions of the American Mathematical Society , vol. 373 (2020), pp. 3885–3903.

▸ANDY ZUCKER, Enumerations of Boolean algebras.

Department of Pure Mathematics, University of Waterloo, Waterloo, ON, Canada.

E-mail: a3zucker@uwaterloo.ca.

When attempting to prove big Ramsey results for new structures, exploring recurrent expansions can be a fruitful place to start. We consider the countable atomless Boolean algebra and expansions of it by an enumeration order. While we are far from settling the question of whether or not this structure has finite big Ramsey degrees, we can see by studying its enumerations that it behaves very differently from any Fraisse limit of a relational class with strong amalgamation. For Fraisse limits of strong amalgamation classes, all enumerations are recurrent and in the same recurrence class. For countable atomless Boolean algebras, some enumerations are not recurrent, and among those that are, we describe several different recurrence classes. Joint work with Barbara Csima, Jan Hubicka, and Joey Lakerdas-Gayle.

Abstracts of invited talks in the Special Session on Computability Theory

▸ANDREW DELAPO, Computability and countable second-countable spaces.

Department of Mathematics, University of Connecticut, 341 Mansfield Rd, Storrs, CT 06269, USA.

E-mail: andrew.delapo@uconn.edu.

The study of countable second-countable (CSC) topological spaces within computability theory was initiated by Dorais in 2011 in the context of reverse mathematics. By restricting to CSC spaces, we can analyze the computability-theoretic content of several theorems and constructions in point-set topology. For example, we can consider the fact that every infinite Hausdorff topological space has an infinite discrete subspace. In this talk, we will examine this principle for CSC spaces from multiple perspectives, including computable structure theory, reverse mathematics, and the Weihrauch degrees.

▸JACOB FIEDLER, Extending affine subspaces in higher dimensions.

Department of Mathematics, University of Wisconsin–Madison, Madison, WI, USA.

E-mail: jbfiedler2@wisc.edu.

In geometric measure theory, one often seeks to understand how geometric properties or operations influence the size of sets. Suppose $E\subset \mathbb {R}^n$ is the union of a collection of large subsets of k-dimensional planes. If each subset is replaced with the entire k-plane, how does this affect the size of the union? We discuss some recent work on this (classical) problem that uses algorithmic information theory and the point-to-set principle.

▸JULIA KNIGHT, KAREN LANGE, AND CHARLES MCCOY CSC, Computable $\Pi _2$ Scott sentences.

Department of Mathematics, University of Notre Dame, 255 Hurley, Notre Dame, IN 46556, USA.

E-mail: knight.1@nd.edu.

Department of Mathematics, Wellesley College, Science Center, 106 Central Street, Wellesley, MA 02481, USA.

E-mail: klange2@wellesley.edu.

Department of Mathematics, University of Portland, 5000 N. Willamette Blvd., Portland, OR 97203, USA.

E-mail: mccoy@up.edu.

By a result of Scott [4], each countable structure for a countable language L is described up to isomorphism by an $L_{\omega _1\omega }$ -sentence, known as a Scott sentence. We consider structures that are countably infinite. By a result of A. Miller [2], no such structure has a $\Sigma _2$ Scott sentence, so having a $\Pi _2$ Scott sentence is as simple as possible. A result of Montalbán [3] yields a nice characterization of the structures (for a fixed countable language) with a $\Pi _2$ Scott sentence. Computable infinitary formulas involve c.e. disjunctions and conjunctions, so they are in a sense comprehensible. We set out to characterize the structures (for a fixed computable language) with a computable $\Pi _2$ Scott sentence. We found some examples and proved some partial results. However, it turns out that there is no nice characterization of the class. The index set is $\Pi ^1_1$ -complete. Rachael Alvir, Barbara Csima, and Harrison-Trainor [1] have also shown this. The two groups worked independently, and the proofs are different.

[1] R. Alvir, B. Csima, and M. Harriston-Trainor, On the computability of optimal Scott sentences. manuscript, 2024.

[2] A. Miller, The Borel classification of the isomorphism class of a countable model. Notre Dame Journal of Formal Logic , vol. 24 (1983), no. 1, pp. 22–34.

[3] A. Montalbán, A robuster Scott rank. Proceedings of the American Mathematical Society , vol. 143 (2015), no. 12, pp. 5427–5436.

[4] D. Scott, Logic with denumerably long formulas and finite strings of quantifiers, The Theory of Models (John Addison, Leon Henkin, and Alfred Tarski, editors) North-Holland, Amsterdam, 1965, pp. 329–341.

▸STEFFEN LEMPP, Chains and antichains in the Weihrauch lattice.

Department of Mathematics, University of Wisconsin–Madison, Madison, WI, 53706 USA.

E-mail: lempp@math.wisc.edu.

We study the existence and the distribution of “long” chains in the Weihrauch degrees, mostly focusing on chains of uncountable cofinality. We characterize when such chains have an upper bound and prove that there are no cofinal chains (of any order type) in the Weihrauch degrees. Furthermore, we show that the existence of coinitial sequences of non-zero degrees is equivalent to CH. Finally, we explore the extendibility of antichains, providing some necessary conditions for maximality.

This is joint work with Marcone and Valenti.

▸ANG LI, Countable Ordered Groups and Weihrauch Reducibility.

Department of Mathematics, University of Wisconsin–Madison, 480 Lincoln Drive, Madison, WI, USA.

E-mail: ali233@wisc.edu.

This article continues to study the connection between reverse mathematics and Weihrauch reducibility. In particular, we study the problems formed from Maltsev’s theorem [1] on the order types of countable ordered groups. Solomon [2] showed that the theorem is equivalent to $\mathsf {\Pi _1^1}$ - $\mathsf {CA_0}$ , the strongest of the big five subsystems of second-order arithmetic. We show that the strength of the theorem comes from having a dense linear order without endpoints in its order type. Then, we show that for the related Weihrauch problem to be strong enough to be equivalent to $\mathsf {\widehat {WF}}$ (the analog problem of $\mathsf {\Pi _1^1}$ - $\mathsf {CA_0}$ ), an order-preserving function is necessary in the output. Without the order-preserving function, the problems are very much to the side compared to analog problems of the big five.

[1] A. Mal’tsev, On ordered groups. Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya , vol. 13 (1949), no. 6, pp. 473–482.

[2] R. Solomon, $\mathsf {\Pi _1^1}$ - $\mathsf {CA_0}$ and order types of countable ordered groups. The Journal of Symbolic Logic , vol. 66 (2001), no. 1, pp. 192–206.

▸ALEXANDER MELNIKOV, The space of continuous functions: a playground for logic.

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

E-mail: alexander.g.melnikov@gmail.com.

In my talk, I will present a sequence of results concerning computability-theoretic and descriptive properties of the space $C([0,1]; \mathbb {R})$ of continuous functions on $[0,1]$ , as well as of spaces $C(K; \mathbb {R})$ , where K is compact Polish. I will discuss results that are local (i.e., describe interesting classes of functions) as well as global (i.e., describe the space itself). The results are joint with many co-authors and span over 5+ years of work. They include the characterisation of $C([0,1]; \mathbb {R})$ among all separable Banach spaces, the primitive recursive universality of $C([0,1]; \mathbb {R})$ , an unexpected characterisation of regular (automatic) real functions, and several very recent results related to the effective content of Banach–Stone Duality between $C(K; \mathbb {R})$ and K.

▸REED SOLOMON, Strong indivisibility for graphs.

Department of Mathematics, University of Connecticut, Storrs, CT 06269, USA.

E-mail: david.solomon@uconn.edu.

A graph is strongly indivisible if whenever it is partitioned into two pieces, one of the pieces is isomorphic to the original graph. Peter Cameron showed there are exactly three strongly indivisible graphs: the countable complete graph, the countable completely disconnected graph, and the random graph. In this talk, I will discuss joint work with Damir Dzhafarov and Andrea Volpi on various effective versions of this classification theorem and connections to reverse mathematics.

▸KESHAV SRINIVASAN, Effective ultrapowers of algebraic extensions of $\mathbb {Q}$ .

Department of Mathematics, George Washington University, Washington, DC, USA.

E-mail: ksrinivasan@gwmail.gwu.edu.

We consider a computability-theoretic ultrapower construction for structures. We start with a computable structure, and consider its countable ultrapower over a cohesive set of natural numbers. A cohesive set is an infinite set of natural numbers that is indecomposable with respect to computably enumerable sets. It plays the role of an ultrafilter, and the elements of a cohesive power are the equivalence classes of certain partial computable functions. Thus, unlike many classical ultrapowers, a cohesive power is a countable structure. We focus on the cohesive powers of fields, specifically algebraic extensions of $\mathbb {Q}$ . We analyze the algebraic properties of these cohesive powers, and determine just how far their first-order theory is from the original field, utilizing the latest results of number theorists working on generalizations of Hilbert’s Tenth Problem to $\mathbb {Q}$ and related fields.

▸JAVA DARLEEN VILLANO, Computable categoricity relative to a generic degree.

Department of Mathematics, University of Connecticut, 341 Mansfield Rd, Storrs, CT 06269, USA.

E-mail: javavill@uconn.edu.

A computable structure $\mathcal {A}$ is said to be computably categorical relative to a degree $\mathbf {d}$ if and only if for all $\mathbf {d}$ -computable copies $\mathcal {B}$ of $\mathcal {A}$ , there is a $\mathbf {d}$ -computable isomorphism $f:\mathcal {A}\to \mathcal {B}$ . This relativization of categoricity behaves chaotically in the c.e. degrees, and so a natural inquiry which arises is to investigate how it behaves in non-c.e. degrees. In this talk, we discuss how we can build a computable graph which is not computably categorical but is computably categorical relative to a $1$ -generic degree $\mathbf {d}$ , and how this result is optimal.

Abstracts of invited talks in the Special Session on Modal Logic

▸ANDREW BACON, What is the logic of logical necessity?

Department of Philosophy, University of Southern California, Los Angeles, CA, USA.

E-mail: ajbacon2@gmail.com.

Consider an interpreted modal propositional language in which $\Box $ expresses logical necessity, and let $\Delta $ be the set of logical truths in this language; i.e., the logic of logical necessity. What can we say about $\Delta $ ? Since every element of $\Delta $ is a logical truth, every element of $\Delta $ should be true. Moreover, since $\Box A$ expresses logical necessity, a sentence of the form $\Box A$ should be true simpliciter if and only if $A\in \Delta $ .

This naturally leads one to the study of models M such that $M\models \Delta $ and $M\models \Box A$ if and only if $A\in \Delta $ , and of logics for which such models exist. I distinguish several special types of logics with this property, and will present some recent joint work with Kit Fine on their existence and their properties.

▸ALEXANDRU BALTAG, The topology of surprise.

Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands.

E-mail: thealexandrubaltag@gmail.com.

I present a topological modal logic, motivated by a famous epistemic puzzle: the Surprise Exam Paradox. It is an epistemic logic, with modalities for ‘knowledge’ (modeled as the universal modality), ‘knowability’ (represented by the topological interior operator), and ‘surprise’ (i.e., unknowability of the actual world). The last notion has both a non-self-referential reading (modeled by Cantor’s derivative: the set of limit points of a given set) and a self-referential one (modeled by Cantor’s perfect core of a given set: its largest subset without isolated points). I present a complete axiomatization of this logic, showing that it is decidable and PSPACE-complete, and I apply it to the analysis of the Surprise Exam Paradox (in both its non-self-referential and its self-referential versions).

The results are based on joint work with N. Bezhanishvili and D. Fernandez Duque [1], and the same method was applied in [2] to prove completeness and decidability of full topological mu-calculus (based on Cantor’s derivative, interior, and universal modality).

[1] A. Baltag, N. Bezhanishvili, and D. Fernandez-Duque, The topology of surprise, 19th International Conference of Knowledge Representation and Reasoning ( Haifa, Israel ), (G. Kern-Isberner, G. Lakemeyer, and T. Meyer, editors), International Joint Conference on Artificial Intelligence Organization, 2022, pp. 33–42.

[2] A. Baltag, N. Bezhanishvili, and D. Fernandez-Duque, The topological mu-calculus: Completeness and decidability. Journal of the Association for Computing Machinery , vol. 70 (2023), no. 5, pp. 1–38.

▸AHMEE CHRISTENSEN, First-order Fischer Servi logic.

Department of Mathematics, University of California Berkeley, Berkeley, CA, USA.

E-mail: achris@berkeley.edu.

The Fischer Servi logic $\mathsf {FS}$ is a particularly natural intuitionistic analogue of the minimal classical normal modal logic $\mathsf {K}$ . We prove the completeness of a first-order analogue of $\mathsf {FS}$ with respect to its expected birelational semantics by introducing a novel model construction, the trace model, and proving a truth lemma. Finally, we consider a number of extensions of the logic for which completeness results can also be obtained with trace model constructions. Among these extensions are first-order intuitionistic analogues of popular normal modal logics like $\mathsf {KD}$ and $\mathsf {S4}$ .

▸JOEL LUCERO-BRYAN, On modal logics arising from the Čech–Stone compactification of ordinals.

Department of Mathematical Sciences, New Mexico State University, 1780 E University Ave, Las Cruces, NM, USA.

E-mail: jglb@nmsu.edu.

Topological semantics of modal logic interprets modal diamond as topological closure, and hence modal box as topological interior. Its roots can be traced back to the late 1930s and early 1940s in the work of Stone, Tarski, and others. As a consequence of Kuratowski’s closure axioms holding in each topological space, Lewis’s well-known modal system S4 is the basic modal logic under these semantics. The celebrated McKinsey–Tarski theorem states that S4 is the modal logic of any separable dense-in-itself metrizable space [3]. Utilizing the Axiom of Choice, Rasiowa and Sikorski showed that the McKinsey–Tarski theorem remains true without the separability assumption [4]. But further dropping the dense-in-itself assumption introduces modal logics other than S4. A complete description of such logics was given in [1].

Much less is known beyond metrizable spaces. In [2], it was shown that S4.1.2 is the modal logic of the Čech–Stone compactification $\beta (\omega )$ of the ordinal $\omega $ equipped with the interval topology. In 2020, Valentin Shehtman posed two related problems:

1. P1: For each nonzero $n\in \omega $ , axiomatize the modal logic $\mathsf {L_n}$ of the Čech–Stone compactification $\beta (\omega ^n)$ of the ordinal $\omega ^n$ equipped with the interval topology.

2. P2: Describe the modal logics arising from the Čech–Stone compactification of an arbitrary ordinal under the interval topology.

This talk provides partial solutions to both P1 and P2. Specifically, we use the Continuum Hypothesis to provide a finite axiomatization of the modal logic $\mathsf {L}_2$ of $\beta (\omega ^2)$ . This solves P1 for the case $n=2$ under the Continuum Hypothesis. We also utilize the Cantor normal form of an ordinal to demonstrate the key role of the logics $\mathsf {L}_n$ in solving P2.

This is joint work with Guram Bezhanishvili, Nick Bezhanishvili, and Jan van Mill.

[1] G. Bezhanishvili, D. Gabelaia, and J. Lucero-Bryan, Modal logics of metric spaces. Review of Symbolic Logic , vol. 8 (2015), no. 1, pp. 178–191.

[2] G. Bezhanishvili and J. Harding, The modal logic of $\beta (\mathbb N)$ . Archive for Mathematical Logic , vol. 48 (2009), no. 3–4, pp. 231–242.

[3] J. C. C. McKinsey and A. Tarski, The algebra of topology. Annals of Mathematics , vol. 45 (1944), no. 2, pp. 141–191.

[4] H. Rasiowa and R. Sikorski, The Mathematics of Metamathematics , Monografie Matematyczne, 41, Państwowe Wydawnictwo Naukowe, 1963.

▸JOSEPH MCDONALD, Monadic ortholattices: completions and duality.

Department of Philosophy, University of Alberta, Edmonton, AB, Canada.

E-mail: jsmcdon1@ualberta.ca.

An ortholattice is a bounded lattice equipped with an order-inverting involutive complementation. A monadic ortholattice is an ortholattice equipped with a closure operator, known as a quantifier, whose closed elements form a sub-ortholattice. Monadic ortholattices generalize monadic Boolean algebras—the algebraic model of the classical predicate calculus in a single variable. Janowitz [5] first considered quantifiers on orthomodular lattices, and Harding [3] studied them, as well as cylindric ortholattices, for their connections to von Neumann algebras, in particular, to subfactors.

We show that the variety of monadic ortholattices is closed under MacNeille and canonical completions. In each case, the completion of A is obtained by forming an associated dual space $X_A$ that is a monadic orthoframe. This is a set equipped with an orthogonality relation and an additional binary relation satisfying certain conditions. For the MacNeille completion, $X_A$ is formed from the non-zero elements of A, and for the canonical completion, $X_A$ is formed from the proper filters of A. The corresponding completion of A is then obtained as the complete ortholattice of bi-orthogonally closed subsets of $X_A$ with an additional operation defined through the binary relation on $X_A$ .

With the introduction of a suitable topology on a monadic orthoframe, we obtain a dual equivalence between the category of monadic ortholattices and homomorphisms and the category of monadic orthospaces and certain continuous frame morphisms.

This talk is based on joint work with John Harding and Miguel Peinado [4].

[1] K. Bimbó, Functorial duality for ortholattices and De Morgan lattices. Logica Universalis , vol. 1 (2007), no. 2, pp. 311–333.

[2] R. Goldblatt, The Stone space of an ortholattice. Bulletin of the London Mathematical Society , vol. 7 (1975), no. 1, pp. 45–48.

[3] J. Harding, Quantum monadic algebras. Journal of Physics A: Mathematical and Theoretical , vol. 55 (2023). no. 39

[4] J. Harding, J. McDonald, and M. Peinado, Monadic ortholattices: completions and duality, Algebra Universalis (2025). Forthcoming.

[5] M. Janowitz, Quantifiers and orthomodular lattices. Pacific Journal of Mathematics , vol. 13 (1963), no. 4, pp. 1241–1249.

[6] D. MacLaren, Atomic orthocomplemented lattices. Pacific Journal of Mathematics , vol. 14 (1964), no. 2, pp. 597–612.

▸ERIC PACUIT AND LEO YANG, Common p-belief and plausibility measures.

Department of Philosophy, University of Maryland, College Park, MD, USA.

E-mail: epacuit@umd.edu

URL: pacuit.org

Department of Philosophy, University of Maryland, College Park, MD, USA.

E-mail: leoyang@umd.edu.

Aumann’s famous Agreeing to Disagree Theorem [1] states that if a group of agents share a common prior, update their beliefs by Bayesian conditioning based on private information, and have common knowledge of their posterior beliefs regarding some event, these posteriors must be identical. There is an elegant generalization of this theorem by Monderer and Samet [4], later refined by Neeman [5]: if a group of agents share a common prior, update their beliefs using Bayesian conditioning on private information, and have common p-belief of their posteriors, these posteriors must be close (i.e., they cannot differ by more than $1 - p$ ). Here, common p-belief generalizes the concept of common knowledge to probabilistic beliefs: agents commonly p-believe an event E if everyone believes E to at least degree p, everyone believes to at least degree p that everyone believes E to at least degree p, and so on.

This article further extends the Monderer–Samet–Neeman Agreement Theorem from classical probability measures to plausibility measures—a very general framework introduced by Halpern [2, 3] that unifies many formal models of belief. To facilitate this extension, we provide a new proof of the Monderer–Samet–Neeman theorem. Building upon both the original proof and our new proof, we offer two different generalizations of the theorem to plausibility-based structures.

Our generalized version of the Monderer–Samet–Neeman theorem, based on conditional plausibility measures, provides a unified framework that identifies the key properties of belief essential for demonstrating that common belief in the posterior probabilities of an event implies that these probabilities must be close. This result deepens our theoretical understanding of agreement theorems. We apply these generalized results to various non-classical belief models, including conditional probability structures and lexicographic probability structures. Furthermore, we demonstrate that whenever the conditions of our generalized theorems are not met, the Monderer–Samet–Neeman Agreement Theorem does not hold. Consequently, our findings suggest that we have identified the minimal conditions required for a belief model to satisfy the Monderer–Samet–Neeman Agreement Theorem.

[1] R. J. Aumann, Agreeing to disagree. Annals of Statistics , vol. 4 (1976), no. 6, pp. 1236–1239.

[2] N. Friedman and J. Y. Halpern, Plausibility measures: A user’s guide, Proceedings of the Eleventh Conference on Uncertainty in Artificial Intelligence (First Last and First2 Last2, editors), Morgan Kaufmann Publishers Inc., 1995, pp. 175–184.

[3] J. Y. Halpern, Plausibility measures: A general approach for representing uncertainty, International Joint Conference on Artificial Intelligence Morgan Kaufmann Publishers Inc., 2001, pp. 1474–1483.

[4] D. Monderer and D. Samet, Approximating common knowledge with common beliefs. Games and Economic Behavior , vol. 1 (1989), no. 2, pp. 170–190.

[5] Z. Neeman, Approximating agreeing to disagree results with common p-beliefs. Games and Economic Behavior , vol. 12 (1996), no. 1, pp. 162–164.

▸FEDOR PAKHOMOV AND JUAN P. AGUILERA, The logic of correct models.

University of Ghent, Ghent, Belgium and Steklov Mathematical Institute, Moscow, Russia.

E-mail: fedor.pakhomov@ugent.be.

Vienna University of Technology, Vienna, Austria and University of Ghent, Ghent, Belgium.

E-mail: aguilera@logic.at.

The present talk is based on the paper [1]. The provability interpretation of modal logic has been classically considered. R. Solovay [2] proved that if we interpret $\Box \varphi $ as “ $\varphi $ is provable in $\mathsf {PA}$ ”, then Gödel-Löb logic $\mathsf {GL}$ precisely axiomatizes all universally provable facts in $\mathsf {PA}$ about such an interpretation. Although less widely known, this article by Solovay also studied an analogous question for the set-theoretic interpretation of $\Box \varphi $ as “ $\varphi $ is true in all models $V_\kappa $ , where $\kappa $ is a strongly inaccessible cardinal”.

In the present talk, I will discuss a set-theoretic interpretation of a polymodal language with modalities $\Box _n$ indexed by natural numbers, where each $\Box _n\varphi $ is interpreted as “ $\varphi $ holds in all $\Sigma _{n+1}$ -correct transitive sets”. For $\mathsf {ZFC}$ as the base theory, such an interpretation is correct for the polymodal provability logic $\mathsf {GLP}$ introduced by G. Japaridze [3] to characterize the logic of graded families of provability predicates in formal arithmetic (although the question of completeness remains open). We focus our attention on the case of the constructible universe, i.e., the theory $\mathsf {ZFC}+L=V$ as the base theory. In this case, we show that the logic of this set-theoretic interpretation is the logic $\mathsf {GLP}.3$ , which is the logic $\mathsf {GLP}$ extended by the axiom of linearity $3$ for each $\Box _n$ .

The key result about the logic $\mathsf {GLP}.3$ that allows us to prove this completeness is that $\mathsf {GLP}.3$ is the maximal normal extension of $\mathsf {GLP}$ that does not prove $\Box _n \bot $ for any n. It should also be noted that $\mathsf {GLP}.3$ coincides with the logic of closed substitutions of $\mathsf {GLP}$ . Since the axiom of constructivity trivially implies the axioms of linearity, the maximality of $\mathsf {GLP}.3$ ensures that it is precisely the logic of the correct model interpretation over $\mathsf {ZFC}+L=V$ . Thus, the technical complexities of the result lie mainly within the domain of modal logic, for which we develop a technique based on the use of the sublogic $\mathsf {J}.3$ of $\mathsf {GLP}.3$ , which is Kripke-complete, unlike the Kripke-incomplete $\mathsf {GLP}.3$ .

[1] J. P. Aguilera and F. Pakhomov, The logic of correct models. Journal of Mathematical Logic , vol. 25 (2025), no. 1, pp. 1–24. (accepted for publication).

[2] R. M. Solovay, Provability interpretations of modal logic. Israel Journal of Mathematics , vol. 28 (1976), no. 1, pp. 33–71.

[3] G. Japaridze, The polymodal logic of provability, Intensional Logics and Logical Structure of Theories , Metsniereba, Tbilisi, 1988, pp. 16–48 (Russian).

▸KONSTANTINOS PAPAFILIPPOU, Parametric Unification: When Projectivity meets Uniform Post-Interpolants.

WE16, Gent University, Krijgslaand 281, Ghent, Belgium.

E-mail: Konstantinos.Papafilippou@ugent.be.

A notion of relativised admissibility has proven itself useful in the characterisation of the provability logic of Heyting Arithmetic [1]. A generalisation of this notion arises from studying a parametric form of Unification. In this context, we found a surprising interplay between projectivity (in the sense introduced by S. Ghilardi [4]) and the uniform post-interpolant for the classical and intuitionistic propositional logic. In particular, we explore whether a projective substitution of a formula is equivalent to its uniform post-interpolant, assuming the substitution leaves the variables of the interpolant unchanged. We show that in classical logic, this holds for all formulas. Although such a nice property is missing in intuitionistic logic, we provide a Kripke semantic characterisation for propositions with this property.

A study on a distinct type of parametric unification was performed recently by R. Nicolau Almeida and S. Ghilardi [3] found similar results. All of this suggests a deeper connection between Uniform Interpolation and Unification style notions warranting further study.

[1] M. Mojtahedi, On provability logic of HA, preprint, 2022, arXiv:2206.00445.

[2] M. Mojtahedi and K. Papafilippou, Projectivity meets uniform post-interpolant: Classical and intuitionistic logic, Advances in Modal Logic, vol. 15 , (A. Ciabattoni, D. Gabelaia, and I. Sedlár, editors), College Publications, 2024, pp. 549–564.

[3] R. N. Almeida and S. Ghilardi, Unification with simple variable restrictions and admissibility of $\Pi _2$ -rules, Advances in Modal Logic, vol. 15 , (Agata Ciabattoni, David Gabelaia, and Igor Sedlár, editors), College Publications, 2024, pp. 79–100.

[4] S. Ghilardi, Unification in intuitionistic logic. The Journal of Symbolic Logic , vol. 64 (1999), no. 2, pp. 859–880.

▸VLADISLAV SLIUSAREV, Criteria of local tabularity of products of modal logics.

Department of Mathematics, New Mexico State University, 1780 E University Ave, Las Cruces, NM 88003, USA.

E-mail: vnvdvc@gmail.com.

A logic is locally tabular, if each of its finite-variable fragments contains only a finite number of pairwise nonequivalent formulas. It is well known that for unimodal transitive logics, local tabularity is equivalent to finite height [8], [7]. In the non-transitive unimodal, and in the polymodal case, no axiomatic criterion of local tabularity is known.

We study locally tabular products of modal logics. For frames $F=(X,R)$ and $G = (Y,S)$ , the product frame $ F\times G$ is the frame $(X\times Y,\, R^h, R^v)$ , where

The product $L_1\times L_2$ of logics $L_1,L_2$ is the bimodal logic of the class of products

Local tabularity is established for some families of products. The products with the logic of equivalence relations $S{5}$ provide a valuable example: N. Bezhanishvili [5] showed that every extension of $S{5}\times S{5}$ is locally tabular, while $S{5}\times S{5}$ itself lacks the local tabularity [6]. V. Shehtman [9] identified a family of locally tabular modal products. For closed systems, intuitionistic modal logics, G. Bezhanishvili et al. described several locally tabular families in [1], [3], [2], and a recent manuscript [4].

In the product $L_1\times L_2$ of two Kripke complete consistent logics, local tabularity of $L_1$ and $L_2$ is necessary for local tabularity of $L_1\times L_2$ . However, the product of two locally tabular logics cannot be locally tabular. The simplest example is the logic $S{5}\times S{5}$ [6]. We provide extra semantic and axiomatic conditions which give criteria of local tabularity of the product of two locally tabular logics: bounded cluster property of one of the factors; a condition we call product reducible path property; finiteness of the one-variable fragment of the product.

We discuss several applications of the criteria. We describe new families of locally tabular product logics. We show that the local tabularity is not sufficient for the product finite model property. We give an axiomatic criterion of local tabularity for all extensions of the logic $S4.1BD_2 \times S5$ and introduce a new prelocally tabular logic above $S4 \times S5.$

This talk is based on a joint work with Ilya Shapirovsky, which can be accessed as a preprint at http://arxiv.org/abs/2404.01670.

[1] G. Bezhanishvili, Varieties of monadic Heyting algebras—Part I. Studia Logica , vol. 61 (1998), no. 3, pp. 367–402.

[2] G. Bezhanishvili, Locally finite varieties. Algebra Universalis , vol. 46 (2001), no. 4, pp. 531–548.

[3] G. Bezhanishvili and R. Grigolia, Locally tabular extensions of MIPC, Advances in Modal Logic (M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, editors), CSLI Publications, 1998, pp. 101–120.

[4] G. Bezhanishvili and C. Meadors, Local finiteness in varieties of MS4-algebras, The Journal of Symbolic Logic , Published online, (2024).

[5] N. Bezhanishvili, Varieties of two-dimensional cylindric algebras. Part I: Diagonal-free case. Algebra Universalis , vol. 48 (2002), no. 1, pp. 11–42.

[6] L. Henkin, J. D. Monk, and A. Tarski, Cylindric Algebras, Part 1 , Elsevier Science, 1971.

[7] L. Maksimova, Modal logics of finite slices. Algebra and Logic , vol. 14 (1975), no. 3, pp. 304–319.

[8] K. Segerberg, An essay in classical modal logic. Filosofiska studier utgivna av Filosofiska institutionen vid Stockholms universitet , vol. 13 (1971), no. 1.

[9] V. B. Shehtman, Squares of modal logics with additional connectives. Uspekhi Matematicheskikh Nauk , vol. 67 (2012), pp. 129–186.

[10] V. B. Shehtman, Segerberg squares of modal logics and theories of relation algebras, Larisa Maksimova on Implication, Interpolation, and Definability (S. Odintsov, editor), Springer International Publishing, Switzerland, 2018, pp. 245–296.

▸SONJA SMETS, Reasoning about quantum information: the probabilistic logic of quantum programs.

Institute of Logic, Language and Computation, University of Amsterdam, Amsterdam,The Netherlands.

E-mail: s.j.l.smets@uva.nl.

To reason about quantum information, I introduce a probabilistic extension of the logic of quantum programs (LQP) in [2]. This framework is capable of expressing important features of quantum measurements and unitary evolutions of multipartite states. The logic [1, 3] includes dynamic modalities [ $\pi $ ] (for quantum programs $\pi $ ), spatial modalities (to talk about subsystems and local information) and a probabilistic modality to capture the probability that a given test (of a quantum-testable property) will succeed. The probabilistic ingredient greatly enhances the expressivity of the logic, allowing us to use it for the specification and verification of probabilistic quantum protocols. In this presentation, I will explain the main ingredients of the logical system, illustrate its application in quantum information theory and show that the logic, when interpreted on finite-dimensional Hilbert spaces, is decidable. The results in this presentation are based on joint work with A. Baltag et al. in [1] and the decidability result itself extends on an idea employed in the proof of [4].

[1] A. Baltag, J. Bergfeld, K. Kishida, J. Sack, S. Smets, and S. Zhong, PLQP & Company: Decidable logics for quantum algorithms. International Journal of Theoretical Physics , vol. 53 (2014), no. 10, pp. 3628–3647.

[2] A. Baltag and S. Smets, LQP: The dynamic logic of quantum information, Special Issue on Quantum Programming Languages, Mathematical Structures in Computer Science , vol. 16 (2006), no. 3, pp. 491–525.

[3] A. Baltag and S. Smets, Reasoning about quantum information: An overview of quantum dynamic logic, Applied Sciences , Special Issue on Quantum Logics, vol. 12 (2022), no. 9, p. 4458.

[4] M. Dunn, T. J. Hagge, L. S. Moss, and Z. Wang, Quantum logic as motivated by quantum computing. The Journal of Symbolic Logic , vol. 70 (2005), no. 2, pp. 353–359.

Abstracts of invited talks in the Special Session on Model Theory

▸AARON ANDERSON, Examples of distal metric structures.

Department of Mathematics, University of Pennsylvania, 209 South 33rd Street, Philadelphia, PA, 19104, USA.

E-mail: awanders@sas.upenn.edu

URL: awainverse.github.io

We identify several examples of distal metric structures and examine several consequences of distality, such as the existence of distal cell decompositions, in each. These results include joint work with Itaï Ben Yaacov and with Diego Bejarano.

One class of examples starts with finding a metric structure whose automorphism group is the group of increasing homeomorphisms of the unit interval. We will discuss some properties of this structure and extrapolate to other models of its theory, which we call “dual linear continua.”

Another source of examples includes real closed metric valued fields. These give rise to a notion of ordered metric structure, providing a viewpoint to study o-minimality in continuous logic.

▸MICHELE BAILETTI, A walk on the wild side.

Mathematics and Computer Science Department, Wesleyan University, 265 Church Street Middletown, CT, 06459, USA.

E-mail: mbailetti@wesleyan.edu.

The tame sides of dividing lines are often defined by the absence of local combinatorial properties. Using the concept of patterns of consistency and inconsistency, we describe a general framework for talking about dividing lines. Taking this idea to its limit, we introduce and study various notions of maximal complexity for first-order theories.

▸DIEGO BEJARANO, Definability and Scott rank in separable metric structures.

University of California Berkeley, Berkeley, CA, USA.

E-mail: bejarano@berkeley.edu.

In [2], Ben Yaacov et al. extended the basic ideas of Scott analysis to metric structures in infinitary continuous logic. These include back-and-forth relations, Scott sentences, and the Lopez–Escobar theorem to name a few.

In this talk, I will talk my work connecting the ideas of Scott analysis to the definability of automorphism orbits and a notion of isolation for types within separable metric structures.

Our results are a continuous analogue of the robuster Scott rank developed by Montalbán in [3] for countable structures in discrete infinitary logic. However, there are some differences arising from the subtleties behind the notion of definability in continuous logic.

[1] D. Bejarano, Definability and Scott rank in separable metric structures, preprint, arXiv.2411.01017.

[2] I. B. Yaacov, M. Doucha, A. Nies, and T. Tsankov, Metric Scott analysis. Advances in Mathematics, vol. 318 (2017), pp. 46–87.

[3] Antonio Montalbán, A robuster Scott rank, Proceedings of the American Mathematical Society , vol. 143 (2015), no. 12, pp. 5427–5436.

▸BLAISE BOISSONNEAU, ARIS PAPADOPOULOS, AND PIERRE TOUCHARD, Mekler’s construction and Murphy’s law for 2-nilpotent groups.

Faculty of Mathematics and Natural Sciences, Heinrich Heine University Düsseldorf, Düsseldorf, Germany.

E-mail: blaise.boissonneau@hhu.de.

Department of Mathematics, University of Maryland, College Park, MD, USA.

E-mail: aris@umd.edu.

Institut für Algebra, Technische Universität Dresden, Dresden, Germany.

E-mail: pierre.touchard@tu-dresden.de.

Given a model-theoretic dividing line admitting a combinatorial definition (think “independence property”), it is relatively easy to construct a purely combinatorial structure (by which I, of course, mean a graph) which lies precisely on one side of the divide. However, constructing a purely algebraic structure (say a group) with the same model-theoretic behaviour is, a priori, a somewhat more mysterious task.

Mekler’s construction comes to the rescue, allowing us to build (2-nilpotent) groups from (nice) graphs in a way that preserves the combinatorial complexity of the graph we started with. This is, of course, ancient news.

In joint work with Boissonneau and Touchard, we prove that the fact that Mekler’s construction preserves dividing lines, such as stability and NIP, is no accident. These are special cases of a more general theorem: Mekler’s construction preserves all dividing lines admitting a definition through an “indiscernible collapse”.

The goal of my talk is to recall Mekler’s construction, gloss over a key relative quantifier-elimination result, and discuss how when things can go wrong, they do.

▸CHRISTINE EAGLES, A uniqueness condition for composition analyses.

Pure Mathematics, University of Waterloo, 200 University Avenue West, Waterloo, ON, Canada.

E-mail: ceagles@uwaterloo.ca.

It is well known that in stable theories, we can understand finite dimensional types in terms of minimal types. We will talk about one such method which we call a composition analysis. We explore a uniqueness condition for a set of minimal types we associate with a type through the composition analysis. This is based on current work in progress.

▸LÉO JIMENEZ, Internality of autonomous systems of differential equations.

Department of Mathematics, The Ohio State University, 100 Math Tower, 231 W 18th Ave, Columbus, OH 43210, USA.

E-mail: jimenez.301@osu.edu.

When solving a differential equation, one sometimes finds that solutions can be expressed using a finite number of fixed, particular solutions, and some complex numbers. As an example, the set of solutions of a linear differential equation is a finite-dimensional complex vector space. This is an incarnation of the model-theoretic phenomenon of internality to the constants in a differentially closed field of characteristic zero. In this talk, I will discuss some recent progress, joint with Christine Eagles, on finding methods to determine whether or not the solution set of a differential equation is internal. A corollary of our method also gives criteria for solutions to be orthogonal to the constants, and in particular not Liouvillian. I will show a concrete application to Lotka–Volterra systems.

▸MICHAEL C. LASKOWSKI AND DANIELLE S. ULRICH, Equivalents of NOTOP.

Department of Mathematics, University of Maryland, College Park, MD, USA.

E-mail: laskow@umd.edu.

E-mail: ds_ulrich@hotmail.com.

A countable theory T is classifiable if it is superstable and has both NDOP and NOTOP. For such theories, every model is determined up to isomorphism by an independent tree of countable, elementary substructures. Historically, superstable theories with NOTOP were only studied under the assumption of NDOP, but we prove that countable, superstable theories with NOTOP are extremely well behaved. In particular, models of such theories determined by an independent tree of countable, elementary substructures up to back-and-forth equivalence.

Many equivalents of NOTOP are given, and we prove that for countable, superstable theories, NOTOP implies PMOP, which was previously only known for theories with NDOP.

▸DAVID MERETZKY, Differential Galois theory with new algebraic constants.

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

E-mail: dmeretzk@nd.edu.

A well-known counterexample due to Seidenberg shows that Picard–Vessiot extensions need not exist for arbitrary ordinary homogeneous linear differential equations over arbitrary differential fields. A positive result from Kolchin’s school at around the same time (1955–1956) shows that inside of a differential closure one can always find a fundamental system of solutions to such an equation over the base field which introduces a Galois extension’s worth of new constants. I will give a model-theoretic account of the structure of differential field extensions generated by fundamental systems of solutions which introduce a finite (algebraic) extension’s worth of new constants, detailing the relationship to the Galois groupoid arising from internality data, and describing a partial Galois correspondence.

▸LYNN SCOW, The modeling property.

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

E-mail: lscow@csusb.edu.

The term the modeling property was coined in [1] to pull together different instances of this phenomenon in the literature and thus create a general object of study. This talk will give an overview of how this study has developed in the author’s own work and indicate some new directions.

[1] L. Scow, Characterization theorems by generalized indiscernibles , Ph.D. thesis, ProQuest LLC, 2010.

Abstracts of invited talks in the Special Session on Proof Assistants

▸MARIO CARNEIRO, NIKOLAI KUDASOV, EMILY RIEHL, DOMINIC VERITY, AND JONATHAN WEINBERGER, Prospects for formalizing the theory of weak infinite-dimensional categories.

Computer Science and Engineering Department, Chalmers University of Technology, 412 96 Gothenburg, Sweden

Computer Science and Engineering Department, Innopolis University, 1 Universitetskaya Str, 420500 Innopolis, Russia

Mathematics Department, Johns Hopkins University, 3400 N Charles Street, Baltimore, MD 21218, USA.

E-mail: eriehl@jhu.edu

URL: emilyriehl.github.io

Mathematical Sciences Institute, Australian National University, Hanna Neumann Building #145, Science Road, Canberra, ACT 2601, Australia.

Fowler School of Engineering and Center of Excellence in Computation, Algebra, and Topology (CECAT), Chapman University, 1 University Drive, Orange, CA 92866, USA.

A peculiarity of the $\infty $ -categories literature is that proofs are often written without reference to a concrete definition of the concept of an $\infty $ -category, a practice that creates an impediment to formalization. We describe three broad strategies that would make $\infty $ -category theory formalizable, which may be described as “analytic,” “axiomatic,” and “synthetic.” We then highlight two parallel ongoing collaborative efforts to formalize $\infty $ -category theory in two different proof assistants: the “axiomatic” theory in Lean and the “synthetic” theory in Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each approach and explain how you could contribute to this effort.

[1] N. Kudasov, E. Riehl, and J. Weinberger, Formalizing the $\infty $ -categorical Yoneda lemma, CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs , 2024, pp. 274–290.

[2] E. Riehl and D. Verity, Elements of $\boldsymbol {\infty }$ -Category Theory , Cambridge Studies in Advanced Mathematics, 194, Cambridge University Press, 2022.

[3] E. Riehl, Could $\infty $ -category theory be taught to undergraduates. Notices of the American Mathematical Society , vol. 70 (2023), no. 5, pp. 727–736.

▸TALITHA HOLCOMBE, A common abstract syntax for total functional programming and interactive theorem provers.

Fowler School of Engineering, Chapman University, 1 University Dr, Orange, CA, USA.

E-mail: holcombe@chapman.edu.

In this work, we introduce a program conversion tool, hs-to-lean, that uses GHC’s ghc-lib-parser API to translate Haskell programs into Lean code, which is then validated by the Lean compiler. The repo can be found at https://github.com/holcombet/hs-to-lean/tree/main. The result is a successful compilation of a fragment of Haskell into correct and executable Lean code that users can prove theorems about. Our approach is inspired by recent advances in formal verification of Haskell programs in Coq and, following [1], we currently restrict our attention to total Haskell.

Our compiler produces an AST that serves as a common level of abstraction between a fragment of Haskell and various other theorem provers, including Lean, Coq, and Agda. This allows a given Haskell program or fragment to be translated to a selection of proof assistants, making it portable and accessible to a range of verification efforts. The compilation of code fragments is bidirectional, supporting the translation of Haskell code to a target proof assistant and vice versa. This method exposes an interesting level of abstraction that is applicable to all of the languages involved and produces a more maintainable compiler.

These results contribute to the ongoing work in the formalization and verification of mathematics and programming and present a viable approach to unifying the formal systems of different proof assistants.

[1] A. Spector-Zabusky, J. Brietner, C. Rizkalla, and S. Weirich, Total Haskell is reasonable Coq, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs ( Los Angeles, CA, USA ), Association for Computing Machinery, 2018, pp. 14–27.

▸PETER JIPSEN, Representability and formalization of relation algebras.

Mathematics, Chapman University, 1 University Dr, Orange, CA 92866, USA.

E-mail: jipsen@chapman.edu

URL: www1.chapman.edu/~jipsen

Abstract relation algebras were defined by Alfred Tarski in 1941 to capture the algebraic properties of binary relations. An interesting question is whether a given relation algebra is representable as an algebra of binary relations. Donald Monk proved in 1964 that the theory of representable relation algebras is not finitely based, and Robin Hirsch and Ian Hodkinson in 2001 showed that it is an undecidable problem whether a finite relation algebra is representable. However, Roger Maddux’s concept of n-dimensional bases and Steve Comer’s one-point extension method can prove (non)representability for various small algebras. Both methods are based on a two-player game for representability, and we revisit implementations of these algorithms and apply them to relation algebras with up to 32 elements. In particular, to decide representability for all relation algebras with 16 elements, the n-dimensional bases implementation was used in 1993 to prove the nonrepresentability for the last two such algebras. Checking these proofs by hand is rather laborious but can now be done with the help of proof assistants.

Lean is an interactive theorem prover that uses a formal language based on dependent type theory to represent mathematics. Its library of definitions and theorems spans many areas of mathematics, including parts of algebra, logic, order theory, and category theory. In joint work with Pace Nelson, we develop the theory of relation algebras in the Lean proof assistant. Lean is also an efficient functional programming language, hence this is a useful platform for implementing algorithms and checking mathematical results obtained by computer calculations. We report on the current state of our project without assuming any background about Lean.

▸PATRICIA JOHANN AND EDWARD MOREHOUSE, Deep induction for advanced data types.

Department of Computer Science, Appalachian State University, Boone, NC 28608, USA.

E-mail: johannp@appstate.org.

Deep induction provides induction rules for deep data types, i.e., data types that are defined over, or mutually recursively with, (other) such data types. Whereas structural induction traverses only the top-level structure of a data type, leaving any data internal to the top-level structure untouched, deep induction inducts over all of the structured data present. Deep induction was originally developed for the generalization of algebraic data types (ADTs) known as nested types in order to define structural induction rules for bushes and other so-called truly nested types. In addition to solving this long-standing problem, deep induction also gives genuinely useful induction rules for deep ADTs such as rose trees. Deep induction has more recently been extended to generalized ADTs (GADTs), such as exist in Haskell and Agda. This talk will show how to further extend deep induction to even more advanced data types like inductive families and inductive-inductive types. It will also explain how deep induction can lead to simpler proofs in practice.

▸LEONARDO DE MOURA, Verified collaboration: low Lean is transforming mathematics, programming, and AI.

Automated Reasoning Group, Amazon Web Services, Seattle, WA, USA.

E-mail: leodemoura0@gmail.com.

Imagine a world where mathematicians, programmers, and AI systems can collaborate with complete trust in each other’s work. This is the promise of Lean, an open-source project that’s transforming how we approach mathematics, software development, and artificial intelligence. Lean provides machine-checkable proofs, eliminating the need for manual verification and allowing humans and AI to build upon each other’s work with unprecedented confidence. By addressing the “Trust Bottleneck,” Lean opens doors to cross-disciplinary collaboration. In this talk, we’ll explore how Lean is impacting these fields. We’ll see how it’s providing mathematicians with a new way to construct and verify complex proofs, enabling software developers to rigorously verify critical systems, and creating a foundation for more reliable AI for science and mathematics. We’ll also discuss the role of the Lean Focused Research Organization (FRO), a non-profit dedicated to advancing Lean and growing its community. The FRO is driving Lean’s development as both a proof assistant and an extensible programming language, empowering users to customize its capabilities for diverse applications. Through real-world examples from academia and industry, we’ll discover how Lean is paving the way for a more efficient, reliable, and collaborative future in mathematics, software development, and AI.

▸WOJCIECH NAWROCKI, STEVE AWODEY, MARIO CARNEIRO, SINA HAZRATPOUR, JOSEPH HUA, AND SPENCER WOOLFSON, Compiling homotopy type theory with Lean: syntax and interpretation.

Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA.

E-mail: wjnawrocki@cmu.edu

URL: https://voidma.in/

Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA.

Computing Science, Chalmers University of Technology, Gothenburg, Sweden.

Harmonic, USA.

Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA.

Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA.

Synthetic theories simplify mathematical developments by providing domain-specific languages and reasoning principles in which certain constructions become more direct. They have also been found to facilitate strong automated reasoning [1]. Homotopy type theory (HoTT) is a synthetic framework for abstract homotopy theory and higher category theory [2]. Although many proof assistants, such as Cubical Agda, support reasoning with synthetic theories, very few of the intended models of these synthetic constructions have been formalized in a proof assistant. This makes it impossible to formally establish results in classical mathematics using synthetic methods. Furthermore, interpretations of complex synthetic constructions can be difficult to compute by hand.

To demonstrate that proof assistants can assist in interpreting synthetic proofs, we are formalizing the model theory of $\text {HoTT}0$ , a simplified fragment of HoTT (with a restricted univalence axiom), in Lean. The system $\text {HoTT}0$ can be interpreted in the category of groupoids, a construction known as the groupoid model [3]. In this talk, we present ongoing work that implements $\text {HoTT}0$ as an embedded domain-specific language in Lean. Using the prover’s extensible syntax and metaprogramming facilities [4], our aim is to provide users with a library of macros that allow unfolding synthetic $\text {HoTT}0$ constructions into elements of the model, and soundly transferring $\text {HoTT}0$ proofs to classical proofs of statements about groupoids. Our code is available at https://sinhp.github.io/groupoid_model_in_lean4/.

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009.

[1] T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong, Solving olympiad geometry without human demonstrations. Nature , vol. 625 (2024), no. 7995, pp. 476–482.

[2] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics , Institute for Advanced Study, 2013. https://homotopytypetheory.org/book.

[3] M. Hofmann and T. Streicher, The groupoid interpretation of type theory, Twenty-Five Years of Constructive Type Theory (Venice, 1995) , vol. 36, pp. 83–111, 1998.

[4] S. Ullrich and L. de Moura, Beyond notations: Hygienic macro expansion for theorem proving languages, Automated Reasoning—10th International Joint Conference, IJCAR 2020 ( Paris, France, July 1–4, 2020 ), 2020, pp. 167–182.

▸EGBERT RIJKE, Mathematical structures from a univalent point of view.

Department of Mathematics, Johns Hopkins University, Baltimore, MD, USA.

E-mail: e.m.rijke@gmail.com.

Libraries of formalized mathematics, as well as the communities working on them, are rapidly growing. Such libraries are written in computer programs called proof assistants, which help the user with verifying the correctness of constructions and proofs. However, most of the modern proof assistants are based on a foundational system called type theory, which is somewhat different from the de facto foundational system of mathematics, first-order logic. Type theory allows for new ways of thinking about mathematics, and one of these ways is using an axiom of Vladimir Voevodsky, the univalent axiom. This axiom expands the notion of equality of mathematical objects so that it coincides with isomorphisms. Mathematicians are used to considering isomorphic objects to be the same for practical purposes, and the univalent axiom formalizes this principle. The univalent axiom changes the way we should think of some mathematical concepts, and in this talk, I will explore some of the basic ways in which mathematics is done from a univalent point of view.

▸MICHAEL SHULMAN, An observational proof assistant for higher-dimensional mathematics.

Department of Mathematics, University of San Diego, 5998 Alcala Park, San Diego, CA 92110, USA.

E-mail: shulman@sandiego.edu

URL: http://www.sandiego.edu/~shulman

In higher-dimensional type theories, each type has not just ordinary terms but also a structure of higher-dimensional terms, such as an $\infty $ -groupoid or homotopy space (homotopy type theory [6]), a cubical set (parametric type theory [2]), or a semi-simplicial set (displayed type theory [5]). These theories provide new and powerful reasoning tools for formalizing and working with higher structures.

Existing computational higher-dimensional type theories (e.g., [4, 3, 7]) are interval-based, meaning the higher structure is detected by mapping out of an “interval type”. An alternative is an observational theory, in which the higher structure is defined separately type-by-type; e.g., in homotopy type theory, a path in a product type is a pair of paths, while a path between functions is a homotopy, and a path between types is an equivalence (the univalence axiom).

In this talk, I will introduce a prototype proof assistant called Narya that implements observational higher-dimensional type theories, including higher observational type theory (the observational version of homotopy type theory), and sketch what we know about its metatheory (e.g., [1]). This is joint work with Thorsten Altenkirch and Ambrus Kaposi.

[1] T. Altenkirch, Y. Chamoun, A. Kaposi, and M. Shulman, Internal parametricity, without an interval, Principles of Programming Languages 2024 , Proceedings of the ACM on Programming Languages , vol. 8, (M. Hicks, editor), 2024, pp. 2340–2369.

[2] J.-P. Bernardy and G. Moulin, A computational interpretation of parametricity, Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science , IEEE Computer Society, 2012, pp. 135–144.

[3] E. Cavallo and R. Harper, Internal parametricity for cubical type theory, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) (M. Fernández and A. Muscholl, editors), Leibniz International Proceedings in Informatics (LIPIcs), 152, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, 2020, pp. 13:1–13:17.

[4] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical type theory: A constructive interpretation of the univalence axiom, preprint, 2016, arXiv:1611.02108.

[5] A. Kolomatskaia and M. Shulman, Displayed type theory and semi-simplicial types, preprint, 2023, arXiv:2311.18781.

[6] Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics , 2013. http://homotopytypetheory.org/book/

[7] A. Vezzosi, A. Mörtberg, and A. Abel, Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Proceedings of the ACM an Programming Languages , vol. 3 (2019), pp. 87:1–87:29.

▸AEACUS SHENG, Formally verifying automata for trusted decision procedures.

Department of Philosophy, Carnegie Mellon University, 5000 Forbes Ave, Pittsburgh, PA 15213, USA.

E-mail: zhaobos@andrew.cmu.edu.

Automata-theoretic decision procedures date back to Büchi’s work, leveraging finite automata to decide sentences of Presburger arithmetic [1], [2]. Extensions of the original procedure are now used to check and discover theorems in combinatorics and number theory [4]. However, unlike SAT solvers, which provide verifiable proof certificates, automata-based decision procedures do not generate formal correctness guarantees as they run. As a result, despite their practical success, concerns remain regarding the reliability and trustworthiness of results obtained using automata-based decision procedures.

Towards addressing this issue, we present our ongoing effort to implement and formally verify automata in Lean [3], which is both a proof assistant and a programming language. By formalizing efficiently-executable automata and proving their properties, we want to ensure that automata-theoretic decision procedures are both provably correct and practically useful.

We begin by introducing the mathematical logic contents behind these decision procedures and provide motivating examples on the type of problems they can solve. Then, we present and explain our implementation and verification of automata in Lean. In the end, we give a preliminary demonstration of how to use our work to prove theorems in Lean.

[1] J. R. Büchi, Weak second-order arithmetic and finite automata, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , vol. 6 (1960), pp. 66–92. Reprinted in S. Mac Lane and D. Siefkes, editors, The Collected Works of J. Richard Büchi , Springer-Verlag, 1990, pp. 398–424.

[2] J. R. Büchi, On a decision method in restricted second-order arithmetic, Logic, Methodology and Philosophy of Science ( Proc. 1960 International Congress ), Stanford University Press, 1962, pp. 1–11.

[3] L. de Moura and S. Ullrich, The Lean 4 Theorem Prover and Programming Language, Automated Deduction—CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings ( Berlin, Heidelberg ), Springer-Verlag, 2021, pp. 625–635.

[4] J. Shallit, The Logical Approach to Automatic Sequences: Exploring Combinatorics on Words with Walnut , London Mathematical Society Lecture Note Series, Cambridge University Press, Cambridge, 2022.

▸SPENCER WOOLFSON, STEVE AWODEY, MARIO CARNEIRO, SINA HAZRATPOUR, JOSEPH HUA, AND WOJCIECH NAWROCKI, Compiling homotopy type theory with Lean: the groupoid model of HoTT0.

Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA.

E-mail: swoolfso@andrew.cmu.edu.

Homotopy type theory (HoTT) is a powerful system for formal mathematics [1]. Yet, without invoking metamathematics, its theorems are detached from classical mathematics, limiting their applicability. Our collaborative project aims to bridge this gap by developing a formal compiler that automatically translates HoTT proofs into Lean theorems.

We focus on a fragment of HoTT, termed $\text {HoTT}0$ , with a semantic interpretation into the category of 1-groupoids. $\text {HoTT}0$ restricts the univalence axiom to only hold on subuniverses of 0-truncated types (i.e., sets). Despite its limiting appearance, this suffices to develop significant portions of univalent, set-level mathematics expressible in HoTT. Building on prior work that modeled type theory in 1-groupoids using categories with families [2], we adapt this approach to natural model semantics [3] based on polynomial functors [4]. The natural model semantics are modular, allowing for implementations of other models of HoTT. This project also lays the groundwork for compiling other type theories in Lean.

In this talk, I plan to discuss the formal system $\text {HoTT}0$ , its 1-groupoid model, and show how some syntactic statements can be translated into classical proofs. I will also discuss what is gained by working in $\text {HoTT}0$ , as opposed to extensional Martin-Löf type theory. I hope this talk can demonstrate how Lean can be adapted to work in novel ways to fit the needs of different researchers.

[1] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics , Institute for Advanced Study, 2013. https://homotopytypetheory.org/book.

[2] M. Hofmann and T. Streicher, The groupoid interpretation of type theory, Twenty-Five Years of Constructive Type Theory (Venice, 1995) , vol. 36, pp. 83–111, 1998.

[3] S. Awodey, Natural models of homotopy type theory. Mathematical Structures in Computer Science , vol. 28, no. 2, pp. 241–286, 2018.

[4] N. Gambino and J. Kock, Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society , vol. 154, no. 1, pp. 153–192, Cambridge University Press, 2013.

Abstracts of invited talks in the Special Session on Set Theory

▸WILLIAM ADKISSON, Tree properties at successors of singulars of many different cofinalities.

Department of Mathematics, University of California Los Angeles, 520 Portola Plaza, Los Angeles, CA, USA.

E-mail: adkisson@math.ucla.edu.

An old problem of Magidor is to obtain the tree property at every regular cardinal greater than $\aleph _1$ . This question can also be posed for strengthenings of the tree property. If there is to be a positive answer to this question, we must obtain the tree property at many successors of singular cardinals; in particular, we must obtain the tree property at successors of singular cardinals of many different cofinalities. Motivated by this problem, from many supercompacts, we build a model in which the tree property holds at $\aleph _{\omega +\omega +1}$ and $\aleph _{\omega _i+1}$ for all $0<i<\omega $ simultaneously. This construction can be modified to obtain the strong tree property, a strengthening of the tree property that is closely linked with strongly compact cardinals; it can be modified further to obtain these properties for much longer sequences of desired cofinalities.

▸ANTON BERNSHTEYN, Borel Local Lemma for graphs of slow growth.

Department of Mathematics, University of California Los Angeles, Los Angeles, CA, USA.

E-mail: bernshteyn@math.ucla.edu.

The Lovász Local Lemma is an important tool in probabilistic combinatorics. Roughly speaking, it shows the existence of a function satisfying certain combinatorial constraints by checking a set of numerical conditions. In addition to its importance in combinatorics, the Local Lemma has recently found applications in many other fields, such as ergodic theory. In this talk, we address the following question: When can we choose the function whose existence is guaranteed by the Local Lemma to be Borel? Csóka, Grabowski, Máthé, Pikhurko, and Tyros proved a Borel version of the Local Lemma under the assumption that a certain auxiliary graph is of subexponential growth. Unfortunately, their proof only works when the range of the desired function is finite. Using a different approach, we extend their result to the case of continuous range as well as to graphs of limited exponential growth. This is joint work with Jing Yu.

▸FILIPPO CALDERONI, Idealistic equivalence relations remastered.

Department of Mathematics, Rutgers University, Hill Center for the Mathematical Sciences, 110 Frelinghuysen Rd., Piscataway, NJ 08854, USA.

E-mail: filippo.calderoni@rutgers.edu

URL: https://sites.math.rutgers.edu/~fc327/

Howard Becker [1] proved that under analytic determinacy, there exists an idealistic equivalence relation that is not an orbit equivalence relation. In this talk, we discuss a strengthening of Becker’s result.

This work aims at better understanding the nuances between idealistic and orbit equivalence relations. Along the way, we explain how this is related to the long-standing $E_1$ conjecture initially formulated by Kechris and Louveau [2]. This is joint work with Luca Motto Ros.

[1] H. Becker, Idealistic equivalence relations, Unpublished notes, 2001.

[2] A. S. Kechris and A. Louveu, The classification of hypersmooth Borel equivalence relations. Journal of the American Mathematical Society , vol. 10 (1997), no. 1, pp. 215–242.

▸RUIYUAN CHEN, Topology versus Borel structure for actions, equivalence relations, and groupoids.

Department of Mathematics, University of Michigan, 530 Church St., Ann Arbor, MI, USA.

E-mail: ruiyuan@umich.edu.

The Becker–Kechris theorem characterizes the topological rigidity intrinsic to a Borel action of a Polish group as consisting of precisely the quotient topologies on each orbit. We show that conversely, every Borel equivalence relation (or more generally, standard Borel groupoid) equipped with a “Borel family” of Polish topologies on each class, satisfying suitable axioms, may be represented in terms of a Polish group action.

▸JAMES CUMMINGS, Linear orderings and singular cardinal combinatorics.

Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, PA 15213, USA.

E-mail: jcumming@andrew.cmu.edu.

We prove some results about linear orderings with cardinality the successor of a singular cardinal, using ideas from singular cardinal combinatorics.

▸NATASHA DOBRINEN, Ramsey spaces and their ultrafilters.

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

E-mail: ndobrine@d.edu.

Many classes of topological Ramsey spaces give rise to ultrafilters with partition properties. On the flip side, sometimes forcings that produce ultrafilters with partition properties harbor a topological Ramsey space as a dense subset. The added clarity of Ramsey space techniques allows for fine analysis of the properties of such ultrafilters. In this talk, we will discuss special properties of such ultrafilters, such as initial Rudin–Keisler and Tukey structures, complete combinatorics, barren extensions, and preservation under Sacks forcing. We will touch on works of Di Prisco, Dobrinen, Hathaway, Mijares, Nieto, Navarro Flores, Özalp, Todorcevic, Trujillo, and Zheng, and discuss ongoing work of the speaker.

▸EYAL KAPLAN, Failure of GCH on a measurable with the Ultrapower Axiom.

Department of Mathematics, University of California Berkeley, University Dr, Berkeley, CA, USA.

E-mail: eyalkaplan@berkeley.edu.

The ultrapower axiom (UA) states that any pair of ultrapowers can be compared by internal ultrapowers. The Axiom was extensively studied by Gabriel Goldberg, leading to a series of striking results.

Goldberg asked whether UA is consistent with a measurable cardinal that violates GCH. The main challenge is that UA is not easily preserved under forcing constructions, especially ones that achieve violation of GCH on a measurable from large cardinal assumptions. For example, such forcings might create normal measures which are incomparable in the Mitchell order—a property that negates UA.

In this talk, we will present a recent result that shows that the failure of GCH on the least measurable cardinal can indeed be forced while preserving UA, starting from the minimal canonical inner model carrying a $(\kappa , \kappa ^{++})$ -extender. This is a joint work with Omer Ben-Neria.

▸MAXWELL LEVINE, Namba Forcing and Singular Cardinals.

Department of Mathematics, University of Freiburg, Freiburg im Breisgau, Germany.

E-mail: maxwell.levine@mathematik.uni-freiburg.de.

One way to study the properties of the infinite cardinals is to examine the extent to which they can be changed by forcing, and the extent to which this process can be controlled. In 1969 and 1970, Bukovský and Namba independently showed that $\aleph _2$ can be forced to be an ordinal of cofinality $\aleph _0$ without collapsing $\aleph _1$ . The forcings they used and their variants are now known as Namba forcing. We will discuss some surprising connections between Namba forcing and the theory of singular cardinals like $\aleph _\omega $ .

▸CHRISTIAN ROSENDAL AND JENNA ZOMBACK, Asymptotically spherical groups.

Department of Mathematics, University of Maryland, College Park, MD, USA.

E-mail: zomback@umd.edu.

A length function $\ell $ on a group G is a function from G to the nonnegative real numbers satisfying the following for all group elements x and y: $\ell (x)=0$ if and only if $x=1_G$ , $\ell (x^{-1}) = \ell (x)$ , and $\ell (xy) \leq \ell (x)+\ell (y)$ .

In this talk, we will investigate the asymptotic behavior of compatible length functions on Polish groups, and in particular, the extent to which a sphere of large radius with respect to one length function looks spherical with respect to another. This is joint work with Christian Rosendal.

▸RILEY THORNTON, Measurable nibbling and hypergraph limits.

Department of Mathematics, Carnegie Mellon University, 5000 Forbes Ave, Pittsburgh, PA, USA.

E-mail: rthornto@andrew.cmu.edu.

The Frankl–Rödl matching theorem says that, in any sparse enough regular hypergraph of large enough degree, there’s matching that covers almost all of the vertices. It was one of the first applications of Rödl’s (now ubiquitous) nibble method. In this talk, I will prove a measurable version of the Frankl–Rödl theorem using a measurable version of the nibble method and some results about weak containment for hypergraphs.

[1] R. Thornton, Limits of sparse hypergraphs, preprint, 2024, arXiv.2410.17483.

Abstracts of contributed talks

▸SAPIR BEN-SHAHAR, ROD DOWNEY, AND MARIYA SOSKOVA, On Quasi-reducibility for c.e. sets.

Department of Mathematics, University of Wisconsin–Madison, 480 Lincoln Drive, Madison, WI 53706, USA.

E-mail: sbenshahar@wisc.edu.

Department of Mathematics, Victoria University of Wellington, Kelburn Parade, Kelburn, Wellington 6012, New Zealand.

E-mail: rod.downey@vuw.ac.nz.

Department of Mathematics, University of Wisconsin–Madison, 480 Lincoln Drive, Madison, WI 53706, USA.

E-mail: soskova@wisc.edu.

Strong reducibilities naturally arise in the combinatorics of reductions in classical mathematics. They are important for at least two reasons: they give insight into exactly how reductions work in practice; and in many cases, a strong reducibility may be more appropriate for a specific area. Quasi-reducibility was introduced by Tennenbaum in the 1960s. On c.e. sets it coincides with $*$ -reducibility, which was shown to be relevant to existentially closed groups in the work of Belegradek [1]. Strong Quasi-reducibility was introduced and studied by Omanadze [2]. I will introduce Quasi-reducibility and strong Quasi-reducibility and discuss some recent results on the structures of the c.e. degrees that arise from these reducibilities. This is joint work with Rod Downey and Mariya Soskova.

[1] O. V. Belegradek, Algebraically closed groups. Algebra i Logika , vol. 13 (1974), pp. 239–255, 363.

[2] R. H. Omanadze, Quasi-degrees of recursively enumerable sets, Computability and Models , Kluwer/Plenum, New York, 2003, pp. 289–319.

▸MORGAN BRYANT, Merges of smooth classes and their properties.

Department of Mathematics, University of Maryland, 4176 Campus Drive, College Park, MD, USA.

E-mail: mbryant7@umd.edu.

Given two Fraïssé-like classes, known as smooth classes, each with countable generic limits (a generalization of a Fraïssé limit), we ask whether we can merge the two classes into a new smooth class with a generic limit. We then study which model-theoretic properties of the generics of the original classes transfer to the generic of the new class, when it exists. In a different direction, we discuss how merges of smooth classes connect to structural Ramsey theory and the Hrushovski property (also known as EPPA). Generalizing work done in [1], we give some examples of merges of smooth classes which have EPPA and the Ramsey property.

[1] D. Evans, J. Hubička, and J. Nešetřil, Automorphism groups and Ramsey properties of sparse graphs. Proceedings of the London Mathematical Society , vol. 119 (2019), no. 2, pp. 515–546.

▸ELIJAH GADSBY, Properties of selector proofs.

Graduate Center CUNY, 365 Fifth Ave., New York City, NY 10016, USA.

E-mail: egadsby@gradcenter.cuny.edu.

A serial property is a suitably enumerated sequence $\{F_n\}$ of sentences and is called selector provable in $PA$ if there is a $PA$ -recursive function $s(x)$ such that $PA\vdash \forall x (s(x){:} \ulcorner F_x\urcorner ),$ where $x{:} y$ is a suitable proof predicate. These notions were introduced by Artemov in his analysis of the formalization of metamathematics, the topic of his plenary talk. In particular, he argues that the consistency of $PA$ is best represented as a serial property and, as such, is selector provable in $PA$ .

This talk will give an overview of the mathematical properties of selector proofs, focusing on the case where the serial property consists of all instances of a single formula. Along the way, it will be seen that iterated selector proofs can be collapsed into single ones, so that natural attempts to extend Artemov’s program along these lines cannot succeed. Furthermore, while primitive recursive selectors are more than sufficient in natural cases, serial properties can be constructed that require arbitrarily complex selectors. Finally, a brief survey of some relevant results from the literature will be given. From these, it can be seen that while $PA$ cannot selector prove the consistency of $PA+Con(PA)$ , there are infinitely many proper extensions of $PA$ whose consistency is selector provable in $PA$ .

▸ARZHANG KAMAREI, Using paradoxical conditionals to reify and imply a semantic fixed point for Godel’s G in first-order arithmetic.

Kamarei Advisory, Spaces, 41 Flatbush Avenue, Brooklyn, NY 11217, USA.

E-mail: ak@kamareiadvisory.com.

Computational models of consciousness do not seem to adequately address the potential logical impossibility of non-Tarskian, Cogito-style, self-referential truth predicates (e.g., “I think, therefore I am”). To address this gap, this article attempts to push the envelope on first-order arithmetic (FOA) self-referential logic, targeting a semantic fixed point for Gödel’s G. We first assume two semantic conditionals, reifying the semantic logical ontology of G: (a) $\neg \text {Prov}(\ulcorner G \urcorner ) \rightarrow \text {Prov}(\ulcorner G \urcorner )$ and (b) $\text {Prov}(\ulcorner G \urcorner ) \rightarrow \neg \text {Prov}(\ulcorner G \urcorner )$ . We next show these can only be satisfied by a unique syntactic fixed point, $G = \neg \text {Prov}(\ulcorner G \urcorner )$ . Since this fixed point is paradoxical and self-referential, it’s syntax and semantics cannot be determined by a consistent system P and G will not characterize $\text {Prov}(x)$ for any such $x \neq G$ . This then creates a unique syntactic-semantic tuple or fixed point characterized as $G \equiv \neg \text {Prov}(\ulcorner G \urcorner )$ , where: (i) the semantic conditionals only match this syntactic definition, (ii) the syntax also implies the semantic conditions, and (iii) whose syntactic definition matches Godel’s G. Because the semantics are not derived from the syntax, we can formalize this equivalence in FOA without violating the Hilbert–Bernays–Löb conditions or conflicting with Löb’s Theorem. This creates a constructive version of Gödel’s First Incompleteness Theorem in FOA. Given that G is a unique fixed point, we can then take the complement or negation of G, which may imply the existence of “normal” formulas, i.e., $\neg \neg \text {Prov}(\ulcorner G \urcorner )$ implies Prov. If so, this implies constructively that $P \vdash \text {Prov}(\ulcorner x \urcorner ) \rightarrow x$ for all such $x \neq G$ , i.e., $\neg G \rightarrow [\text {Prov}(x) \rightarrow x]$ . This thus bifurcates the universe of formulas into G and $\neg G$ , showing that they can have differently determined relationships between truth and proof and which are constructible. This may help open the door to self-referential logics which may be necessary for the digitization of Cogito.

▸BJØRN KJOS-HANSSEN, The Shannon effect.

Department of Mathematics, University of Hawai‘i at Mānoa, Honolulu, HI 96822, USA.

E-mail: bjoernkh@hawaii.edu.

In many settings, almost all objects have nearly the same complexity as the hardest objects. Specifically, Claude Shannon conjectured [3] that almost all Boolean functions have nearly the same circuit complexity as the hardest function. It was proved by Lupanov [2]. Similar statements hold for plain and prefix-free Kolmogorov complexity. The phenomenon was named the Shannon effect by Lupanov in 1970.

For nondeterministic automatic complexity, the effect follows from an upper bound by Hyde from 2013 and an almost sure lower bound by Kjos-Hanssen in 2021.

The nondeterministic automatic complexity also has an “exact” version, in which a single accepting path is not required, merely a single accepted word of a given length. For this notion, a Shannon effect has been proved as well [1].

Whether the effect pertains to deterministic automatic complexity is not known.

[1] J. Chen, B. Kjos-Hanssen, I. Koswara, L. Richter, and F. Stephan, Languages of words of low automatic complexity are hard to compute, submitted, 2025.

[2] O. B. Lupanov, The synthesis of contact circuits, Doklady Akademii Nauk SSSR (N.S.) , vol. 119 (1958), pp. 23–26.

[3] C. E. Shannon, The synthesis of two-terminal switching circuits. Bell System Technical Journal , vol. 28 (1949), pp. 59–98.

▸CONNOR LOCKHART, Model theory of the Farey graph via smooth classes.

Department of Mathematics, University of Maryland, 4176 Campus Dr, College Park, MD, USA.

E-mail: connorl@umd.edu.

We study the model theory of the Farey graph F by realizing it as the generic of a smooth class $(K,\leq )$ . By varying the relation $\leq $ we may obtain distinct generics that are either atomic or saturated. This will allow us to demonstrate a quantifier elimination for $Th(F)$ . The Farey graph is also the simplest nontrivial curve complex of a surface, where $F=C(\Sigma _{1,1})$ . Modifications of this technique to obtain results for the general model theory of the curve complex $C(\Sigma _{g,n})$ will be discussed.

▸JUAN AGUILERA AND ROBERT S. LUBARSKY, On strategies for player II in $\Sigma ^0_2$ games.

Institute of Discrete Mathematics and Geometry, Vienna University of Technology, Vienna, Austria, and Department of Mathematics, Ghent University, Ghent, Belgium.

E-mail: aguilera@logic.at.

Department of Mathematical Sciences, Florida Atlantic University, 777 Glades Rd., Boca Raton, FL 33431, USA.

E-mail: robertlubarsky@att.net.

That certain strategies for Player II in $\Sigma ^0_2$ games are always winning can be witnessed in L by certain ordinals. There is already a known description of these ordinals. What is less understood is where the strategies themselves appear. What is also not understood is the model theory Player II would use in these strategies. This talk is an introduction to this topic, with the goal of conveying these open questions and some of the ideas around them.

[1] F. Abramson and G. Sacks, Uncountable Gandy ordinals. Journal of the London Mathematical Society , vol. 14 (1976), no. 2, pp. 387–392.

[2] J. Aguilera and R. Lubarsky, On winning strategies for $F_\sigma $ games, The Journal of Symbolic Logic , to appear.

[3] R. Gostanian, The next admissible ordinal. Annals of Mathematical Logic , vol. 17 (1979), pp. 171–203.

[4] C. Heinatsch and M. Möllerfeld, The determinacy strength of $\Pi ^1_2$ -comprehension. Annals of Pure and Applied Logic , vol. 161 (2010), pp. 1462–1470.

[5] Y. Moschovakis, Descriptive Set Theory , second ed., American Mathematical Society, 2009.

[6] P. Wolfe, The strict determinateness of certain infinite games. Pacific Journal of Mathematics , vol. 5 (1955), pp. 841–847.

▸TAN OZALP, Initial Tukey structure below a stable ordered-union ultrafilter.

Department of Mathematics, 255 Hurley Building, Notre Dame, IN 46556, USA.

E-mail: aozalp@nd.edu.

For arbitrary partial orders $(\mathbb {P}, \leq _{\mathbb {P}})$ and $(\mathbb {Q}, \leq _{\mathbb {Q}})$ , $(\mathbb {P}, \leq _{\mathbb {P}})$ is said to be Tukey reducible to $(\mathbb {Q}, \leq _{\mathbb {Q}})$ , written $(\mathbb {P}, \leq _{\mathbb {P}}) \leq _T (\mathbb {Q}, \leq _{\mathbb {Q}})$ , if there is a map $f:\mathbb {Q} \to \mathbb {P}$ which sends cofinal subsets of $\mathbb {Q}$ to cofinal subsets of $\mathbb {P}$ . In particular, we can restrict our attention to directed partial orders of the form $(\mathcal {U}, \supseteq )$ , where $\mathcal {U}$ is an ultrafilter. In this case, Tukey reducibility generalizes RK-reducibility.

A detailed study of the Tukey order of ultrafilters on countable sets was initiated by Dobrinen and Todorcevic in [2]. Later, Todorcevic proved that Ramsey ultrafilters are Tukey-minimal [5]. This study continued with Dobrinen and Todorcevic’s classification of isomorphism classes of ultrafilters Tukey reducible to a weakly Ramsey ultrafilter [3]. The rest of this line of work and more detailed information can be found in [1]

Dobrinen and Todorcevic asked the question of classification of ultrafilters Tukey reducible to a stable ordered-union ultrafilter [2]. The goal of this talk will be to introduce stable ordered-union ultrafilters on $\mathrm {FIN}$ , and state the classification of all ultrafilters Tukey reducible to a stable ordered-union $\mathcal {U}$ . This is the main result of [4], and answers a question from [2]. I will also talk about the techniques that were used in the proof of this classification, and finish with remarks on a canonization theorem for $\mathrm {FIN}_2^{[\infty ]}$ that I am currently finalizing, that will be used to classify all ultrafilters Tukey reducible to the ultrafilter forced by $\mathrm {FIN}_2^{[\infty ]}$ .

[1] N. Dobrinen, Topological Ramsey spaces dense in forcings, Structure and Randomness in Computability and Set Theory , World Scientific Publishing, Hackensack, 2020, pp. 3–58.

[2] N. Dobrinen and S. Todorcevic, Tukey types of ultrafilters, Illinois Journal of Mathematics , vol. 55 (2011), no. 3, pp. 907–951.

[3] N. Dobrinen and S. Todorcevic, A new class of Ramsey-classification theorems and their application in the Tukey theory of ultrafilters, Part 1, Transactions of the American Mathematical Society , vol. 366 (2014), no. 3, pp. 1659–1684.

[4] T. Ozalp, Initial Tukey structure below a stable ordered-union ultrafilter, preprint, 2024, arXiv:2410.04326.

[5] D. Raghavan and S. Todorcevic, Cofinal types of ultrafilters. Annals of Pure and Applied Logic , vol. 163 (2012), no. 3, pp. 185–199.

▸JACKSON WEST, Farness logics of Euclidean spaces.

Department of Mathematical Sciences, New Mexico State University, Las Cruces, NM, USA.

E-mail: jackwest@nmsu.edu.

In any metric space $(X,d)$ , we can define the far relation R by

This relation gives a uni-modal logic of $(X,d)$ which is known as the farness logic of $(X,d)$ , denoted by $\text {Log}_{>1}(X)$ . In this talk, I will present results on the farness logics of $\mathbb {R}^n$ and $\mathbb {Q}^n$ , recently obtained in a joint work with Gabriel Agnew, Uzias Gutierrez-Hougardy, John Harding, and Ilya Shapirovsky [1].

Namely, we show that the farness logics of $\mathbb {R}^n$ are all distinct and contain an infinite anti-chain. In particular, for $n < m$ , we have $\text {Log}_{>1}(\mathbb {R}^m)\not \subseteq \text {Log}_{>1}(\mathbb {R}^n)$ . Additionally, for m sufficiently larger than $n,$ we have $\text {Log}_{>1}(\mathbb {R}^n)\not \subseteq \text {Log}_{>1}(\mathbb {R}^m)$ . We also show that the logics $\text {Log}_{>1}(\mathbb {R}^n)$ and $\text {Log}_{>1}(\mathbb {Q}^n)$ are not finitely axiomatizable and $\text {Log}_{>1}(\mathbb {Q})$ is strictly contained in $\text {Log}_{>1}(\mathbb {R})$ . Furthermore, $\text {Log}_{>1}(\mathbb {R})$ lacks the finite model property.

This work was supported by NSF Grant DMS - 2231414.

[1] G. Agnew, U. Gutierrez-Hougardy, J. Harding, I. Shapirovsky, and J. West, On distance logics of Euclidean spaces, preprint, 2025, arXiv:2501.04884.

▸HONGYU ZHU, The Borel complexity of the class of models of first-order theories.

Department of Mathematics, University of Wisconsin–Madison, Van Vleck Hall, 480 Lincoln Dr, Madison, WI 53706, USA.

E-mail: hongyu@math.wisc.edu.

Viewed as a subset of Cantor space, the class of countable models $\operatorname {Mod}(T)$ of any first-order theory T is always Borel. A natural question, then, is the relationship between its descriptive complexity and the complexity of the underlying theory. Using theorems of López-Escobar and Solovay, we give a more precise characterization of the complexity of $\operatorname {Mod}(T)$ in terms of that of T. We also discuss some applications to models of PA and infinitary logic. (This is based on joint work with Andrews, Gonzalez, Lempp, Rossegger [1], and related to recent work of Enayat and Visser [2].)

[1] U. Andrews, D. Gonzalez, S. Lempp, D. Rossegger, and H. Zhu, The Borel complexity of the class of models of first-order theories, preprint, 2024, arXiv:2402.10029.

[2] A. Enayat and A. Visser, Incompleteness of boundedly axiomatizable theories. Proceedings of the American Mathematical Society , vol. 152 (2024), no. 11, pp. 4923–4932.

Abstracts of talks presented by title

▸JOACHIM MUELLER-THEYS, The monotonicity paradox and its solution.

Independent Scholar, Heidelberg, Germany.

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

I. It is a truism that laws must not be simply extended. Substitution is a meta-theorem of propositional logic, which becomes false in our metalogical (or auto-modal, respectively) extensions MPL: $ \neg \Box p $ is logically true (since $ p $ can be interpreted false), but $ \neg \Box \top $ is not. The same happens to monotonicity: $ \neg \Box p $ is no consequence of $ p $ .

II. In contrast, we found and proved that monotonicity belongs to the valid principles of universal semantics: $ \forall f \in S \ (F \ \mathrm {Seq} _T \, f \& G \supseteq F \Rightarrow G \ \mathrm {Seq} _T \, f ) $ ( $ F , G \subseteq S $ ), whereby $ \mathrm {Seq} _T \subseteq \wp ( S ) \times S $ (“consequence”) is defined in standard, Tarskian manner: $ F \ \mathit {Seq} _T \, f : \Leftrightarrow \forall w \in W \, ( F \, T \, w \Rightarrow f \, T \, w) $ , but the underlying relation: $ T \subseteq S \times W $ (“true at”), between $ S \neq \emptyset $ (“Sprache”) and $ W \neq \emptyset $ (“worlds”) is free.

It follows that general consequences and logical laws coincide: $ \mathit {Seq} _\forall \, f : \Leftrightarrow \forall F \, F \, \mathrm {Seq} \, f \Leftrightarrow \emptyset \ \mathrm {Seq} \, f \Leftrightarrow : \mathit {Seq} _0 \, f \Leftrightarrow \mathit {V} \! f : \Leftrightarrow \forall w \, f \, T \, w $ .

III. How do I and II go together though? Let $ \Im ^\ast $ be the set of all interpretations $ I ( p ) \in \{ 1 , 0 \} $ . We extend PL satisfaction $ \models \ \subseteq \Im ^* \times L $ conservatively to $ || \! \! \! = _\Phi \ \subseteq \Im ^* \times L ^\Box $ ( $ \Phi \subseteq L $ ), for $ \alpha = \Box \beta $ specifically by $ I \, | | \! \! \! = _\Phi \alpha : \Leftrightarrow \forall J \, ( J \models \Phi \Rightarrow J \, | | \! \! \! = _\Phi \beta ) $ , and PL consequence $ \Phi \models \phi $ to $ \Phi \, | | \! \! = \alpha : \Leftrightarrow \forall I \, ( I \models \Phi \Rightarrow I \, | | \! \! = _\Phi \alpha ) $ .

In analogy to II, $ I \, | | \! \! \! = _\Phi \alpha $ induces the consequence $ \Gamma \, | | \! \! \! = _\Phi \alpha $ . The theorem of II now yields indeed that $ | | \! \! \! = _\Phi $ is monotonic, but it does not yield that $ \Phi \, | | \! \! \! = \alpha $ and $ \Psi \supseteq \Phi $ generally imply $ \Psi \, | | \! \! \! = \alpha $ , since $ \Phi \, | | \! \! \! = \alpha $ corresponds to $ \Phi \, | | \! \! \! = _\Phi \alpha $ , whereas $ \Psi \, | | \! \! \! = \alpha $ corresponds to $ \Psi \, | | \! \! \! = _\Psi \alpha $ . As indicated in I, concrete refutation is, e.g., by $ \Phi : = \emptyset $ , $ \alpha : = \neg \Box p $ , $ \Psi : = \{ p \} $ .

Notes. This abstract is widely self-contained. There have been several précis in “The Bulletin of Symbolic Logic” as well on MPL (with some severe misprints) as on abstract semantics. In a letter to Wilfried Buchholz from March 2024, we, among other things, explained that monotonicity, despite its universal validity, fails for auto-modal extensions, because satisfaction differs. We are grateful to anybody who has helped us.