Logic Colloquium 2025, the annual European Summer Meeting of the Association of Symbolic Logic, took place at Technische Universität Wien, July 7 through July 11, 2025. The conference was held in person at the Freihaus Building of TU Wien with 220 registered participants, including 65 students.

Funding for the conference was provided by the Vice-Rectorate for Research, Faculty of Mathematics, and the Marketing Team of Technische Universität Wien as well as by the Association for Symbolic Logic, the Austrian Science Foundation, the European Research Council, the Kurt Gödel Society, the National Science Foundation of the United States, and the Vienna Tourist Board.

The success of the meeting owes a tremendous amount to the excellent work of the Local Organizing Committee chaired by Juan Aguilera, Matthias Baaz, and Anela Lolić. The remainder of this committee was composed of Miguel Aguilar, Fernando Barrera, Kees van Berkel, Anton Fernández, Mariami Gamsakhurdia, Martina Iannella, Thibaut Kouptchinsky, Stella Mahler, Marietta Meszlenyi, Rahman Mohammadpour, Grigorii Stepanov, and Corey Switzer. Special thanks to the student and postdoc volunteers, including Bartosz Bednarczyk, Adrian Chroust, Huimin Dong, Marit Einböck, Martin Gogeißl, Jasmine Haider, Elijah Schulzki, Mirko Tagliaferri, and Rui Zhou.

The Program Committee was chaired by Juliette Kennedy (University of Helsinki) and consisted of Juan Aguilera (TU Wien), Mikołaj Bojańczyk (University of Warsaw), Nicola Gambino (University of Manchester), Nina Gierasimczuk (Danish Technical University), Rosalie Iemhoff (Utrecht University), Sandra Müller (TU Wien), Daniel Palacin (Complutense University of Madrid), Ludovic Patey (CNRS, Paris), and Andrés Villaveces (National University of Colombia).

The program included two tutorial courses, nine plenary lectures, twenty two invited lectures in seven special sessions (Computability Theory, Condensed Math, Logic and Leibniz, Logic in Computer Science, Model Theory, Proof Theory, and Set Theory), the Thirty-Sixth Gödel lecture, and 96 contributed talks. The Gödel lecture New challenges to our conception of the Higher Infinite was given by Joan Bagaria (University of Barcelona). The following tutorial courses were given.

Dima Sinapova (Rutgers University), Compactness principles: the tree property and friends.

Henry Towsner (University of Pennsylvania), Fast-growing functions, ordinals, and proof theoretic strength.

The following invited plenary lectures were presented.

Bahareh Afshari (University of Gothenburg), Demystifying $\mu $ .

Ulrik Buchholtz (University of Nottingham), Logical aspects of simplicial type theory.

Thomas Colcombet (CNRS, Université Paris Cité), Monadic second-order logic and variations.

Sébastien Gandon (Université Clermont Auvergne), Jean Nicod’s Geometry in the sensible world: an early interplay between logic and French philosophy.

Patrick Lutz (University of California Berkeley), A theory which really doesn’t have a computable model.

Maryanthe Malliaris (University of Chicago), Ultrafilters and model theory.

Saharon Shelah (Hebrew University and Rutgers University), Twins: non-isomorphic models forced to be isomorphic, part 1.

Benjamin Siskind (TU Wien), The status of order-preserving Martin’s Conjecture.

Sonja Smets (ILLC, University of Amsterdam), Comparing knowledge.

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

For the Program Committee

Juliette Kennedy

Abstract of the invited 36th Annual Gödel Lecture

▸JOAN BAGARIA, New challenges to our conception of the Higher Infinite.

ICREA (Institució Catalana de Recerca i Estudis Avançats) and Departament de Matemàtiques i Informàtica, Universitat de Barcelona, Gran Via de les Corts Catalanes, 585, 08007 Barcelona, Catalonia.

E-mail: bagaria@ub.edu.

Large-cardinal axioms assert the existence of infinite cardinal numbers, collectively known as large cardinals, whose associated properties make them very large and imply they cannot be proved to exist from the ZFC axioms of set theory. The first large cardinals were identified almost a century ago; since then, a wide array of large cardinals have emerged in different contexts and taking a variety of forms. The world of large cardinals, also known as the Higher Infinite, is now one of the main sources of insight into the nature of infinity and the structure of the universe of sets. Moreover, large cardinals have been essential for the solution of many well-known problems across different areas of mathematics. However, in spite of their success, large cardinals have remained a mystery from a foundational point of view. Indeed, a precise definition of large cardinal, which would encompass all known such cardinals into a single general notion, has been lacking. Further, the fact that all large-cardinal axioms tend to line up into a well-ordered hierarchy of relative consistency strength stayed mostly unexplained. Furthermore, no convincing justification of their naturalness, or their status as true axioms of set theory has been put forward, and their acceptance has so far been supported mainly by their fruitful consequences.

Over the last years, a program of reformulating large-cardinal axioms in terms of a new principle called Structural Reflection has demonstrated that most of them are equivalent to particular instances of this principle, with a similar pattern repeating at different regions of the large-cardinal hierarchy. Moreover, the uniformity of the hierarchy revealed by Structural Reflection has prompted the definition of new natural large-cardinal axioms. The strongest of them, asserting the existence of, so-called, exacting and ultraexacting cardinals, challenge our current intuitions about the universe of all sets, V. Indeed, in contrast with all previously known large cardinals, they imply that V is not equal to HOD (Gödel’s universe of Hereditarily Ordinal Definable sets), and so there exist sets that cannot be defined in any reasonable way. Further, the existence of these cardinals challenge the linear incremental picture of the large-cardinal hierarchy, as they interact in quite extreme ways with other large cardinals. For example, even though the existence of ultraexacting cardinals is equiconsistent, modulo ZFC, with the existence of well-studied large cardinals, when taken together with other standard large cardinals below them they become much stronger. One striking consequence of the consistency with ZFC of the existence of an exacting cardinal above some standard large cardinals is that Woodin’s HOD Conjecture cannot hold.

Abstract of invited tutorials

▸DIMA SINAPOVA, Compactness principles: the tree property and friends.

Department of Mathematics, Rutgers University, Piscataway, NJ 08854, USA.

E-mail: dima.sinapova@rutgers.edu.

Compactness is the phenomenon when if a property holds for all strictly smaller substructures of a given object, then it holds for the entire object as well. Compactness usually follows from large cardinals, and on the other hand tends to fail in canonical L-like models. Moreover, it is deeply connected with cardinal arithmetic.

A key instance of compactness is the tree property: a combinatorial principle that generalizes Konig’s old lemma from graph theory that every infinite finitely branching tree has an infinite branch. At higher cardinals, the tree property can be forced using large cardinals. A long-standing project in set theory is forcing the tree property simultaneously at all regular cardinals greater than $\aleph _1$ . We will describe some of the history and the ZFC constraints of this endeavor. Then we will discuss a result (joint with Cummings, Hayut, Magidor, Neeman, and Unger) that constitutes the current state of the art for the longest interval on which the tree property has been obtained.

Finally, I will go over some ZFC constraints on obtaining the tree property further. One such constraint is on the cardinal arithmetic, due to Specker’s lemma. I will discuss applications of failure of square and cardinal arithmetic, especially around singular cardinals.

▸HENRY TOWSNER, Fast-growing functions, ordinals, and proof theoretic strength.

Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104, USA.

E-mail: htowsner@upenn.edu.

URL Address: http://www.math.upenn.edu/∼htowsner.

One of the cornerstones of proof theory is ordinal analysis—the discovery that we can can measure the strength of a theory—more precisely, the consistency strength—of a theory with a (countable) transfinite ordinal, the proof-theoretic ordinal. This ordering behaves robustly when restricted to “natural” theories, simultaneously measuring the provable $\Pi ^0_2$ sentences, the rates of growth of provably total computable function, and the difficulty of proving the consistency of the theory. All this breaks down quickly on artificial examples, leading to the question of what precisely makes a theory natural.

As the theories get stronger, it becomes more and more difficult to describe the corresponding ordinal—as it must, since the ordinal has to capture every computational process which the theory can prove terminates.

Recent developments have expanded the scope of ordinal analysis in several directions—beginning to develop a formal understanding of what makes a theory natural, understanding how to use proof-theoretic tools to analyze the provable $\Pi ^{1}_2$ sentences, and describing the ordinals of stronger theories, even the long sought after goal of describing the proof theoretic ordinal of full second-order arithmetic.

All these developments are tied together by looking past the ordinals to dilators—linear order-preserving functions which preserve well-foundedness which, despite being too “big” to be true ordinals, can be seen as extension of the ordinals.

This tutorial will not assume prior knowledge of ordinal analysis. We will introduce the core tools of the field with an eye to seeing how new results flow naturally from the right perspective on classical theorems in the area.

Abstracts of invited plenary lectures

▸BAHAREH AFSHARI, Demystifying $\mu $ .

Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, Box 200, 40530 Göteborg, Sweden.

E-mail: bahareh.afshari@gu.se.

We explore the theory of ill-founded and cyclic proofs for the modal $\mu $ -calculus, propositional modal logic extended by quantifiers for inductive and co-inductive constructions. A fine analysis of provability for classical and intuitionistic modal logic endowed with fixed points provides a novel bridge between finitary, cyclic, and ill-founded conceptions of proof and re-enforces the importance of disjunctive normal form in proving completeness.

▸ULRIK BUCHHOLTZ, Logical aspects of simplicial type theory.

School of Computer Science, University of Nottingham, Nottingham NG7 2RD, UK

E-mail: ulrik.buchholtz@nottingham.ac.uk.

URL Address: https://ulrikbuchholtz.dk/.

Riehl and Shulman [3] introduced simplicial type theory to reason about higher categories (meaning $(\infty ,1)$ -categories) almost synthetically in an extension of homotopy type theory. In recent work with Daniel Gratzer and Jonathan Weinberger [1, 2] we further extend simplicial type theory to construct fundamental examples, such as the category of spaces up to homotopy, and show how the theory of higher categories can be developed to a greater extent in this framework.

In the talk, I shall focus on the logical aspects of this work, leaving type theory in the background as much as possible. One aspect is the need for constructive modal logics of a variety of shapes, and another is the central importance of the geometric logic of bounded distributive lattices.

The duality axiom, first proposed by Blechschmidt, holds in the intended models and states that the evaluation map $A \to \bigl (\mathrm {hom}_{\mathbb {I}}(A, \mathbb {I}) \to \mathbb {I}\bigr )$ is an isomorphism, where $\mathbb {I}$ is the universal bounded distributive lattice, A is any finitely presented $\mathbb {I}$ -algebra, i.e., $\mathbb {I}[x_1,\ldots ,x_n]$ modulo finitely many relations, and $\mathrm {hom}_{\mathbb {I}}(A, \mathbb {I})$ is the set of $\mathbb {I}$ -algebra homomorphisms from A to $\mathbb {I}$ .

I shall comment on the origin and uses of the duality axiom and the prospects for further syntheses of modal and geometric logic in type theory.

[1] U. Buchholtz and J. Weinberger, Synthetic fibered $(\infty ,1)$ -category theory. Higher Structures , vol. 7 (2023), no. 1, pp. 74–165.

[2] D. Gratzer, J. Weinberger, and U. Buchholtz, The Yoneda embedding in simplicial type theory, LICS ’25: 40th Annual ACM/IEEE Symposium on Logic in Computer Science (Singapore) , to appear.

[3] E. Riehl and M. Shulman, A type theory for synthetic $\infty $ -categories. Higher Structures , vol. 1 (2017), no. 1, pp. 147–224.

▸THOMAS COLCOMBET, Monadic second-order logic and variations.

Université Paris Cité – CNRS – IRIF, Paris 75013, France.

E-mail: thomas.colcombet@irif.fr

The subject of this talk is monadic second-order logic (MSO for short), i.e., the extension of first-order logic with the ability to quantify over sets of elements.

In a first part, we shall review some classical results of Elgot, Büchi, Trakhtenbrot, Rabin, and Shelah concerning the decidability of the MSO theory of chains and trees.

In the second part, we will see how the seminal works of Schützenberger, McNaughton, and Papert that effectively characterize first-order definability over finite words by algebraic identities can be extended fruitfully to infinite chains (with Carton, Puppis, and Sreejith A.V.). We get from it the collapse of MSO to one alternation of set quantifiers, the effective algebraic characterization of first-order logic and several other logics. An unexpected consequence is a new elementary proof of the failure of Lyndon’s preservation theorem in the finite (Kuperberg).

The third part considers extending the expressiveness of MSO while retaining its strong decidability properties. The logic MSO+U, introduced by Bojańczyk, uses a new quantifier U which means “there exist sets of arbitrarily large size such that $\ldots $ ”. Some non-trivial fragments of MSO+U are known to be decidable over $\omega $ (collaboration with Bojańczyk), yet this logic turns out to be undecidable in general as shown by Bojańczyk, Parys, and Toruńczyk. The undecidability of several other natural extensions of MSO are obtained as consequences (by Bojańczyk, Kelmendi, Stefanski, and Zetzsche, and collaborations with Carton, Blumensath, and Rabinovich). Another extension is cost-MSO which extends MSO with the ability to express positively the existence of a bound on the size of sets. This logic is known to be decidable over finite chains (C.), finite trees (with Löding), and partially over infinite trees (with Blumensath, Kuperberg, Parys, and Vanden Boom). Its status over countable infinite trees remains open.

▸SÉBASTIEN GANDON, Jean Nicod’s Geometry in the sensible world: an early interplay between logic and French philosophy.

Department of philosophy, Université Clermont Auvergne, 29 Bd Gergovia, 63000 Clermont, France.

E-mail: sebastien.gandon@uca.fr.

Jean Nicod was a French philosopher and logician who worked with Russell from 1914 to 1917. Before his premature death in 1924, he published around ten articles and wrote a doctoral thesis. The talk aims to introduce his main work, La géométrie dans le monde sensible, taken from his dissertation and published posthumously. I will argue that Nicod sets out one of the first formal definitions of the notion of interpretation of one theory in another, and that he does so in response to Bergson’s anti-intellectualism. By highlighting how a philosophical context that was rather hostile to science led to advances in logic, this study illustrates the complexity of the relationship between logic and philosophy in the first half of the twentieth century.

▸PATRICK LUTZ, A theory which really doesn’t have a computable model.

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

E-mail: pglutz@berkeley.edu.

The completeness theorem guarantees that any consistent theory has a model, but it is not hard to show that the computable version of this statement does not hold: there is a computable, consistent theory with no computable model. Furthermore, there are many natural theories with this property. In particular, the proof of Tennenbaum’s Theorem can be used to show that essentially any reasonably strong set theory, including ZFC, cannot have a computable model. Recently, however, Pakhomov showed that this phenomenon is somewhat fragile: it depends on the language in which the theory is formulated. For example, Pakhomov showed that there is a theory which is definitionally equivalent to ZFC (a strong form of bi-interpretability) which does have a computable model. In light of this, Pakhomov raised the question of whether every computable, consistent theory is definitionally equivalent to a theory with a computable model. In response to Pakhomov’s question, James Walsh and I have constructed a counterexample: a computable, consistent theory such that no definitionally equivalent theory has a computable model. I will explain the context for our result and the main ingredients of the proof, which consist of a mixture of computability theory and tame model theory.

▸MARYANTHE MALLIARIS, Ultrafilters and model theory.

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

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

The talk will give a model-theoretic perspective on the ways in which (regular) ultrafilter construction has developed in the last 50 years or so, starting with work of Keisler and Kunen, through recent joint work of the speaker and Shelah.

▸SAHARON SHELAH, Twins: non-isomorphic models forced to be isomorphic, part 1.

Einstein Institute of Mathematics, The Hebrew University of Jerusalem, Jerusalem 9190401, Israel, and Department of Mathematics, Rutgers University, Piscataway, NJ 08854, USA.

E-mail: saharon.shelah@mail.huji.ac.il.

For which (first-order complete, usually countable) T do there exist non-isomorphic models of T which become isomorphic after forcing with a forcing notion $\mathbb {P}$ ? Necessarily, $\mathbb {P}$ is non-trivial; i.e., it adds some new set of ordinals. It is best if we also demand that it collapses with no cardinal. It is better if we demand on the one hand that the models are non-isomorphic, and even far from each other (in a suitable sense), but on the other hand, $\mathcal {L}$ -equivalent for some suitable logic $\mathcal {L}$ .

We may require that the forcing notion is just any c.c.c. one as in older works with Baldwin and Laskowski. But we like to fix the forcing as a known one rather than to construct (or force) one.

In this part we give sufficient conditions: for theories with the independence property, we prove this when $\mathbb {P}$ adds no new $\omega $ -sequence. We may prove it “for some $\mathbb {P}$ ,” but better would be for some specific forcing notions, or a natural family. Best would be to characterize the pairs $(T,\mathbb {P})$ for which we have such models.

The results say (e.g.) that there are models $M_1, M_2$ which are not isomorphic (or even far from being isomorphic, in a rigorous sense) which become isomorphic when we extend the universe by adding a new branch to the tree $({}^{\theta>}2,\lhd )$ .

We shall mention some specific choices of $\mathbb {P}$ : mainly ${}^{\theta>}2$ with $\theta = \theta ^{<\theta }$ uncountable and the order being an initial segment.

This is part of the classification and so-called Main Gap programs.

▸BENJAMIN SISKIND, The status of order-preserving Martin’s Conjecture.

Institute of Discrete Mathematics and Geometry, TU Wien, 1040 Vienna, Austria.

E-mail: benjamin.siskind@tuwien.ac.at.

Martins Conjecture is a proposed classification of Turing-invariant functions under the Axiom of Determinacy, consisting of two parts. Part 1 of the conjecture states that every Turing-invariant function is either equivalent to a constant function or above the identity function with respect to a natural order on Turing-invariant functions, the Martin order. Part 2 of the conjecture says that the functions which are Martin-above the identity are pre-well-ordered by the Martin order, with the successor operation given by composition with the Turing jump. Both parts of the conjecture remain open, even for Borel functions. However, restricting the conjecture to the (ostensibly) smaller class of functions that are order-preserving for the Turing-reducibility order turns out to be more tractable. We have shown that part 1 of the conjecture holds restricted to the class of order-preserving functions and, building on work of Slaman and Steel, part 2 of the conjecture holds through the iterates of the hyperjump. Furthermore, there is a natural plan for proving order-preserving Martin’s Conjecture in models of determinacy which have been analyzed by inner model theory. This is joint work with Patrick Lutz.

▸SONJA SMETS, Comparing knowledge.

Institute for Logic, Language and Computation, University of Amsterdam, Science Park 107, 1098 X Amsterdam, The Netherlands.

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

I present a philosophical analysis of comparative epistemic assertions between individuals or groups of agents. Such assertions can express that a group of agents collectively knows at least as much as another individual or group of agents. I will provide examples of epistemic comparison statements and analyze them in the context of different epistemic conditions. Formally, I introduce the logic obtained by adding a ‘group epistemic comparison’ operator to the standard multi-agent epistemic logic with distributed and common knowledge. I will report on the results obtained in [1], in which we axiomatized the resulting logic on the class of $S5$ -models, and on recent work that generalizes the study of these group epistemic comparisons to the context of epistemic models including (besides $S5$ ) also $KT$ and $S4$ . In this context, I will pay special attention to what agents (collectively/individually) can deduce about their own epistemic position relative to that of other agents, who may know more or less than them. We will observe that the type of epistemic attitude that we attribute to individual agents and to groups of agents will play a crucial role. On the dynamic side, I discuss the informational events by which an epistemic advantage can be acquired. Such events subsume different kinds of actions via which agents gain access to other agents’ information or data, and hence they can in principle learn everything known to those others. This presentation is based on joint work with A. Baltag at the University of Amsterdam on a philosophical discussion of the results in [1, 2].

[1] A. Baltag and S. Smets, Learning what others know, EPiC Series in Computing (LPAR23 Proceedings of the International Conference on Logic for Programming AI and Reasoning) , vol. 73 (E. Albert and L. Kovacs, editors), Easy Chair, 2020, pp. 90–119.

[2] A. Baltag and S. Smets, Logics for data exchange and communication, AiML Proceedings, vol. 15 (A. Ciabattoni, D. Gabelaia, and I. Sedlár, editors), Advances in Modal Logic, College Publications, Prague, 2024, pp. 147–170.

Abstracts of invited talks in the Special Session on Computability Theory

▸GEORGE BARAMPALIAS, Computable oneway functions on the reals.

State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100045, China.

E-mail: barmpalias@gmail.com.

Central in computational complexity and cryptography is the notion of oneway functions: finite maps that are easy to compute but hard to invert. Levin recently extended this concept to functions on the reals—infinite bit-sequences—using computability and algorithmic randomness. He asked whether computable oneway functions exist, and whether they can satisfy the properties that are desirable in cryptography, such as collision-resistance. In this talk, I will present answers to some of these questions and additional results on probabilistic hardness of inversion for real functions. I will then proceed to explore variations of this concept and focus on characterizing the unsolvability of inverting effective real functions. I will conclude with several open questions and connections between this and several topics in computability and algorithmic randomness.

This work is joint with Mingyang Wang and Xiaoyan Zhang based on the preprints in the bibliography.

[1] G. Barmpalias, M. Wang, and X. Zhang, Complexity of inversions on the reals, preprint, 2025, arXiv:2412.07592.

[2] G. Barmpalias and X. Zhang, Computable one-way functions on the reals, preprint, 2025, arXiv:2406.15817.

[3] G. Barmpalias and X. Zhang, Collision resistant hash-shuffles on the reals, preprint, 2025, arXiv:2501.02604.

▸ELLEN HAMMATT, Arriving on time: punctual structures and isomorphisms.

Institute of Discrete Mathematics and Geometry, TU Wien, 1040 Vienna Austria.

E-mail: ellen.hammatt@tuwien.ac.at.

Computable structures can delay new elements in an unbounded way. We explore what happens when we require structures to be computable without delay, that is, the structure must provide a bound for each element and then the element must arrive on time. In 2017, Kalimullin, Melnikov, and Ng initiated the study of such punctual structures. This study connects naturally to polynomial-time structures but has several advantages over directly studying polynomial-time presentations. In this talk we will discuss the motivations to study this area and some of the interesting results that have been collected so far. In particular, we will compare the results and techniques in the computable and punctual cases of categoricity and dimension. We will also discuss the properties of the punctual degrees, a degree structure on the presentations of a fixed structure, defined via the reduction induced by primitive recursive isomorphism.

▸GIOVANNI SOLDÀ, A proof of Generalized Higman’s Lemma using iterated ideals.

WE16, Ghent University, Krijgslaan 281, Ghent 9000, Belgium.

E-mail: giovanni.a.solda@gmail.com

Higman’s Lemma says that if an order Q is wqo, then so is $Q^{<\omega }$ , the set of finite strings over Q ordered by embedding. By Generalized Higman’s Lemma we mean the statement obtained from the previous one by substituting every instance of “wqo” with “bqo”. Other than being an interesting combinatorial statement on its own, Marcone in [3] showed the importance of Generalized Higman’s Lemma in the study of the reverse mathematics of Nash–Williams’ Theorem.

In this talk, after giving a brief introduction to the theory of bqo’s in reverse mathematics, we aim at giving a (to the best of our knowledge) new proof of Generalized Higman’s Lemma. The main ingredient to do this are iterated ideals, a controlled form of iterated powerset of an order (similar concept where known from the inception of bqo theory, see, e.g., [2], and were recently proficuously used in reverse mathematics, e.g., in [1]). Although we will sketch the proof in a strong theory, we will indicate how to modify it so as to make it go through in the relatively weak theory $\mathsf {PRS}\omega \mathsf {U}$ .

This is joint work with Fedor Pakhomov.

[1] A. Freund, On the logical strength of the better quasi order with three elements. Transactions of the American Mathematical Society , vol. 376 (2023), pp. 6709–6727.

[2] R. Laver, On Fraïssé’s order type conjecture. Annals of Mathematics , vol. 96 (1971), no. 1, pp. 89–111.

[3] A. Marcone, On the logical strength of Nash–Williams’ theorem on transfinite sequences, Logic: From Foundations to Applications , Oxford University Press, 1996, pp. 327–351.

Abstracts of invited talks in the Special Session on Condensed Math

▸DAGUR ASGEIRSSON, Formalized condensed mathematics.

Department of Mathematical and Statistical Sciences, University of Alberta, University Commons 5-140, Edmonton, AB T6G 2R3, Canada.

E-mail: dagurtomas@gmail.com.

Following a challenge of Peter Scholze, in 2022 members of the Lean community completed a formalization of the “fundamental theorem of liquid vector spaces”. This project, known as the Liquid Tensor Experiment, contained the first formalized definition of a condensed set. After the completion of this project, there was an effort to formalize the foundations of condensed mathematics in Lean’s mathematical library mathlib. In this talk I will explain the difference between these two types of formalization projects, give an overview of what results from condensed mathematics are in mathlib and what is within reach, and discuss some subtleties in the theory which were uncovered and resolved thanks to the formalization effort.

▸NATHANIEL BANNISTER AND DIANTHE BASAK, Orion’s Belt: what set theory can and cannot say about condensed mathematics.

Institut de Mathématiques de Jussieu – Paris Rive Gauche, Université Paris Cité, Place Aurélie Nemours, 75013 Paris, France.

E-mail: basak@imj-prg.fr.

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

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

Clausen and Scholze [3] and independently Barwick and Haine [1] define the condensed (resp., pyknotic) sets to be sheaves on a site consisting of all (resp., of size $< \kappa $ ) Stone spaces of Boolean algebras. There have been many speculations as to how this relates to forcing with “all Boolean algebras at once”, and work of Bergfalk, Lambie-Hanson, and Šaroch [2] shows that indeed certain results of Clausen and Scholze pertaining to Whitehead’s problem for condensed abelian groups can be recast as forcing results.

On the set theoretic side, however, there is a well-known way to force with many Boolean algebras at once: the Solovay model [4] construction. Might the two lead to the same outcome? We will elaborate in this talk the exact connection between these two methods, using the Whitehead problem as an instructive example. The talk is based on joint work with Nathaniel Bannister.

[1] C. Barwick and P. Haine, Pyknotic objects, I. Basic notions, preprint, 2019, arXiv:1904.09966.

[2] J. Bergfalk, C. Lambie-Hanson, and J. Šaroch, Whitehead’s problem and condensed mathematics, preprint, 2023, arXiv:2312.09122.

[3] P. Scholze, Lectures on Condensed Mathematics, preprint, 2019.

[4] R. M. Solovay, A model of set-theory in which every set of reals is Lebesgue measurable. Annals of Mathematics , vol. 92 (1970), no. 1, pp. 1–56.

▸MAI GEHRKE, ELENA POZZAN, AND MATTEO VIALE, The Wallman compactification is universal among $T_1$ -compactifications.

Laboratoire J.A. Dieudonné, Université Cote d’Azur, Nice 06000, France.

E-mail: Mai.Gehrke@unice.fr.

Dipartimoento di Matematica “Giusepe Peano”, University of Torino, Turin 10124, Italy

E-mail: elena.pozzan@unito.it.

E-mail: matteo.viale@unito.it.

Recall that for any topological space $(X,\tau )$ its Wallman compactification $\mathbf {W}(X,\tau )$ is the topological space whose points are the maximal filters of closed sets for $\tau $ and whose topology is generated by the open sets

for $U\in \tau $ .

We show that for any $T_1$ -space $(X,\tau )$ its Wallman compactification is universal wrt a very large class of continuous $f:X \to K$ with $(K,\sigma )$ a compact $T_1$ -space. Specifically we introduce the notion of strongly continuous function and show that if $f:X \to K $ is strongly continuous, then f admits a unique (strongly) continuous extension $\mathbf {W}(f):\mathbf {W}(X,\tau )\to K$ .

This result (almost) generalizes the Stone–Cech compactification theorem in that $\mathbf {W}(X,\tau )$ is the Stone–Cech compactification $\beta (X)$ of $(X,\tau )$ when $(X,\tau )$ is normal; more generally $\beta (X)$ is the largest quotient of $\mathbf {W}(X,\tau )$ which is compact Hausdorff. We also note that the class of strongly continuous functions between $T_1$ -spaces is closed under composition and is quite large; any continuous $f:X\to Y$ with $(X,\tau ),(Y,\sigma ) T_1$ -spaces is strongly continuous if any of the following conditions are met: $(Y,\sigma )$ is normal, f is closed, f is the inclusion of X into $Y=\mathbf {W}(X,\tau )$ . Furthermore this class is provably larger than the family of continuous functions between $T_1$ -spaces for which a theorem of the same flavour had already been proved in [1].

[1] John. D. Harris, The Wallman compactification as a functor. General Topology and Applications , vol. 1 (1971), pp. 273–281.

Abstracts of invited talks in the Special Session on Logic and Leibniz

▸FILIPPO COSTANTINI, Leibniz’s mereology.

Centre National de la Recherche Scientifique, Laboratoire SPHERE, 75205 Paris, France.

E-mail: filippo.costantini@u-paris.fr.

This talk is an introduction to Leibniz’s mereological system. I start by explaining the distinction between the containment and the part-whole relation: first, I introduce the Real Addition calculus (the calculus concerning the containment relation); then, I introduce the mereological calculus by extending the Real Addition calculus via what I call the Homogeneity axiom. I analyze this notion in detail and argue that it implies a gunk conception of (proper) part.

▸MARKO MALINK AND ANUBAV VASUDEVAN, Every truth is analytic: Leibniz on conceptual containment.

Department of Philosophy, New York University, New York, NY 10012, USA.

E-mail: mm7761@nyu.edu.

Department of Philosophy, University of Chicago, Chicago, IL 60637, USA.

E-mail: anubav@uchicago.edu.

Leibniz holds that every truth is analytic. In every truth, he claims, the concept of the predicate is contained in the concept of the subject. In this talk, we will examine the logical foundations of this account of truth. We will discuss how the logical work done by Leibniz in the 1680s in which he introduces the device of propositional terms allows him to render every categorical and hypothetical truth as a case of conceptual containment. Moreover, we will see how his logical work enables him to verify his claim that every substance mirrors the whole universe, and hence that “when I perceive one thing or one mode of a thing, I always perceive the whole universe”.

▸MASSIMO MUGNAI, Leibniz, the Boolean Algebra and the nature of the conditional corresponding to the relation of containment.

Scuola Normale Superiore, Pisa 56126, Italy.

E-mail: massimo.mugnai@sns.it.

In the General Inquiries on the Analysis of Notions and Truths [Generales Inquisitiones de Analysi Notionum et Veritatum] Leibniz works out a logical calculus that has all the necessary ingredients to develop a Boolean algebra. Relying on the work of Marko Malink and Abumav Vasudevan, I attempt to reconstruct some fundamental aspects of the logical calculus contained in the GI and briefly address the problem of Leibniz’s apparent disregard for the development of a calculus based on join. Contrary to what is commonly held, I intend to show that Leibniz came very close to intuiting the dual behavior of join and meet. I will also try to temper Malink and Vasudevan’s thesis that the conditional corresponding to the Leibnizian containment relation between antecedent and consequent of a proposition is a material conditional. Indeed, I think that Leibniz is unaware of the distinction between the so-called material conditional and a conditional analogous to the one proposed by C.I. Lewis in the early twentieth century; and that he therefore employs in the logical calculus a conditional however ‘modalized’. This conclusion of course is independent of whether the ‘material’ interpretation of the conditional used by Leibniz is preferable for the consistency of the calculus itself.

▸ALESSIA SALIERNO, Some notes on Leibniz’s geometrical calculus.

Dipartimento di Filosofia Piero Martinetti, Università degli Studi di Milano, via Festa del Perdono, 8, Milan 20122, Italy and SPHERE laboratoire, Université Paris Cité, 8 rue Albert Einstein, Paris 75006, France.

E-mail: alessia.salierno@unimi.it.

My talk will deal with Leibniz’s geometrical calculus and its development throghout the years, from 1679 to 1716, drawing upon a significant number of unpublished texts. Despite the connection of this calculus with many different topics (among which the analysis of geometrical concepts called by Leibniz analysis situs and the make up of a suitable set of characters apt to express it, the characteristica geometrica), I will focus mainly on the calculus itself, illustrating the rules for the derivation of new propositions and providing some examples of the most elaborated demonstrations and the results generally achieved by Leibniz through such a calculus.

Abstracts of invited talks in the Special Session on Logic in Computer Science

▸JAKUB OPRŠAL, Homotopy and the complexity of homomorphism problems.

School of Computer Science, University of Birmingham, Birmingham B15 2TT, UK.

E-mail: j.oprsal@bham.ac.uk.

I will talk about an emerging new application of homotopy theory in the computational complexity of discrete problems.

Many natural and well-known computational problems (e.g., graph 3-colouring or solving systems of linear equations over a finite field) can be naturally expressed as the question of deciding the existence of a homomorphism from a given structure A to a fixed structure B (called template). The two structures are required to have a common signature which contains only relational symbols. For a fixed B, this problem is known as the constraint satisfaction problem (CSP) of B. For example, graph k-colouring is the CSP of the k-clique. The talk will explore the question: how does the topology of the solution space of a CSP influence its complexity?

I will focus on a particular example of graph homomorphism problems that are the subject of a seminal paper by Hell and Nešetřil [1990], who proved that homomorphism to a graph H can be decided in polynomial time if H is bipartite (or contains a self-loop), and is NP-complete otherwise. This dichotomy served as an important test case for the Feder–Vardi dichotomy conjecture, and Bulatov–Zhuk dichotomy of complexity of finite-template CSPs. I will present a new proof of the Hell–Nešetřil theorem using tools from topological combinatorics based on ideas of Lovász (1978) and Brower’s fixed-point theorem. This is joint work with Sebastian Meyer (TU Dresden).

▸SZYMON TORUŃCZYK, Monadically dependent classes and the model checking problem.

Institute of Informatics, University of Warsaw, Warsaw 00-927, Poland.

E-mail: szymtor@mimuw.edu.pl.

A central problem in theoretical computer science concerns the complexity of the model-checking problem: to decide if a given formula holds in a given structure. Here, I will focus on formulas of first-order logic, and assume that the structure comes from a fixed hereditary class of graphs, allowing to leverage tools from structural graph theory. For some ‘tame’ graph classes—such as the class of planar graphs, or every class of graphs with bounded maximum degree—the model-checking problem is tractable in the sense of parameterized complexity, while for some others, it is hard. It is conjectured that the dividing line between the tractable and the hard hereditary classes corresponds precisely to the notion of monadic dependence, originating in model theory. I will survey the recent progress in this fascinating area, which connects various notions originating in structural graph theory—such as nowhere denseness, treewidth, and twin-width—with notions originating in model theory—such as stability and dependence—as well as notions originating in statistical learning theory and computational geometry—such as VC-dimension and $\varepsilon $ -nets.

Abstracts of invited talks in the Special Session on Model Theory

Jana Maříková, Matchings, measures and Grothendieck groups.

Kurt Gödel Research Center, University of Vienna, Kolingasse 14-16, 1090 Vienna, Austria.

E-mail: jana.marikova@univie.ac.at.

We discuss a generalization of results from [1] on the existence of definable matchings in biparatite graphs in o-minimal structures, and its implications for a related Grothendieck group.

[1] J. Marříková, On definable matchings in o-minimal bipartite graphs. Fundamenta Mathematicae , vol. 264 (2024), pp. 85–102.

▸PIERRE TOUCHARD, On reduced products of first order structures: which groups recognize coordinates?

Institute of Algebra, TU Dresden, Zellescher Weg 12-14, 01069 Dresden, Germany.

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

This talk is based on a joint project with Ilijas Farah and Kyle Gannon on reduced products of first-order structures. Let $\mathcal {L}$ be a first-order language and let $(M_i)_{i\in I}$ be a family of first-order structures indexed by a set I. Given an ideal $\mathcal {I}$ on I, one can consider the reduced product $M:= \prod _{\mathcal {I}} M_i$ , which naturally inherits an $\mathcal {L}$ -structure. A classical result in model theory, the Feferman–Vaught theorem, describes a language where such a reduced product eliminates quantifiers relative to the Boolean algebra $\mathcal {P}(I)/ \mathcal {I}$ . It is however not always clear if this language is interpretable in the original language $\mathcal {L}$ . An interesting subquestion is to determined whether $\prod _{\mathcal {I}} M_i$ recognize coordinates—namely, whether the structure M “knows” that it is a product over $\mathcal {P}(I)/ \mathcal {I}$ . After providing all the necessary definitions, we will discuss this question in the context of various first-order structures and for particular classes of groups.

▸TINGXIANG ZOU, Around the Elekes-Szabó Theorem.

Department of Mathematics, University of Bonn, Bonn 53113, Germany.

E-mail: tingxiangzou@gmail.com.

The Elekes–Szabó Theorem roughly says the following: Let R be an algebraic ternary relation in $W_1\times W_2\times W_3$ defined in a field K of characteristic 0, such that any two coordinate is interalgebraic with the third one, for example, the collinear relation for three distinct points in a curve. Suppose there are arbitrarily large finite subsets $X_i$ of $W_i$ each of size n and has bounded intersection with any proper subvariety of $W_i$ , such that the intersection of R with $X_1\times X_2\times X_3$ has size approximately $n^2$ , then R must be essentially the graph of group operation of some commutative algebraic group G. In this talk, I will give an overview of several results (joint work with Martin Bays and Jan Dobrowolski) in the effort of removing the assumption of $X_i$ having bounded intersection with proper subvarieties of $W_i$ . This assumption is closely related to $W_i$ being one-dimensional. Our motivation is to find a genuine higher-dimensional generalisation of the Elekes–Szabó Theorem.

Abstracts of invited talks in the Special Session on Proof Theory

▸LUISA DESPRÉS, Applications of Herbrand’s theorem to Euclidean geometry.

Department of Mathematics, Technische Universität Darmstadt, Schlossgartenstraße 7, 64289 Darmstadt, Germany.

E-mail: luisa.despres@stud.tu-darmstadt.de.

Herbrand’s theorem is a well-known logical theorem about the realizability of first-order formulae in a suitable universe. In the context of (Tarski’s axiomatization of) Euclidean geometry, it has been used ‘negatively’ by Beeson, Boutry, and Narboux [1] to show the underivability of the parallel axiom from a first-order version of the other axioms. As suggested by the ‘proof mining’ paradigm, this talk discusses a ‘positive’ application of Herbrand’s theorem: the extraction of computational content from proofs in geometry. As a case study, it presents the extraction of a Herbrand disjunction for the Outer Pasch theorem from its proof by Schwabhäuser, Szmielew, and Tarski in [4]. It turns out that this extraction can be done in a modular way. The talk explores why this is likely to be possible for most proofs in geometry, in contrast to the generally bad behaviour of Herbrand’s theorem in connection with the modus ponens rule, as discussed in [3, pp. 22–40]. The talk is based on joint work with U. Kohlenbach in [2].

[1] M. Beeson, P. Boutry, and J. Narboux, Herbrand’s theorem and non-Euclidean geometry. Bulletin of Symbolic Logic , vol. 21 (2015), no. 2, pp. 111–122.

[2] L. M. Després and U. Kohlenbach, Herbrand analyses in geometry: A case study. Journal of Logic and Computation , vol. 35 (2025), no. 5, p. exaf017.

[3] U. Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics , Springer Monographs in Mathematics, Springer, 2008.

[4] W. Schwabhäuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie: Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie. Teil II: Metamathematische Betrachtungen , Springer, 1983.

▸ANELA LOLIĆ, A proof theory for Henkin quantifiers.

Institute of Logic and Computation, TU Wien, Favoritenstrasse 9, 1040 Vienna, Austria.

E-mail: anela@logic.at.

Henkin quantifiers extend classical first-order logic by allowing more flexible relationships between quantifiers. In standard first-order logic, the scope of an existential quantifier typically depends on all the preceding universal quantifiers. Henkin quantifiers, by contrast, allow for partial dependencies: an existential quantifier may depend on only some of the universal quantifiers. The simplest Henkin quantifier not expressible in first-order logic can be described as a quantifier macro binding four variables in a formula:

This is to be read “For every x there is a u (depending only on x) and for every y there is a v (depending only on y)” such that $A(x, y, u, v)$ . If the semantical meaning of this formula is given in second-order notation, the above formula is semantically equivalent to the second-order formula $\exists f \exists g \forall x \forall y A(x, y, f(x), g(y)),$ where f and g are function variables.

We will present a general methodology to construct globally sound, but possibly locally unsound sequent calculi in first-order format tailored to quantifier macros [1] and partial theories of Henkin quantifiers [2]. Globally sound here means every derivable sequent is valid under the chosen semantics, although individual inference steps might be unsound in isolation. A central negative result is that no locally sound analytic sequent calculus exists for any reasonable fragment of the full theory of Henkin quantifiers. The root cause is the interplay of strong and weak quantifier inferences within a single rule, which violates eigenvariable conditions typical in first-order systems. This problem not only occurs for Henkin quantifiers, but already for much simpler quantifier macros involving universal and existential quantifiers.

[1] M. Baaz and A. Lolić, Towards a proof theory for quantifier macros. Information and Computation , vol. 287 (2022), pp. 104753.

[2] M. Baaz and A. Lolić, Towards a proof theory for Henkin quantifiers. Journal of Logic and Computation , vol. 31 (2021), no. 1, pp. 40–66.

▸DALE MILLER, Peano arithmetic and $\mu $ MALL.

Inria-Saclay and LIX, Institut Polytechnique de Paris, Palaiseau 91120, France.

E-mail: dale.miller@inria.fr.

Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $\mu $ MALL [2, 1] as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative–additive linear logic (MALL) [3] with the addition of the universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $\mu $ MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $\mu $ MALL, we obtain $\mu $ LK $_p$ , a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $\mu $ LK $_p$ (including cut-elimination and the completeness of focusing), we prove that $\mu $ LK $_p$ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $\mu $ LK $_p$ over $\mu $ MALL. This talk is based on the forthcoming paper [4].

[1] D. Baelde, Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic , vol. 13 (2012), no. 1, pp. 2:1–2:44.

[2] D. Baelde and D. Miller, Least and greatest fixed points in linear logic, International Conference on Logic for Programming and Automated Reasoning (LPAR) (N. Dershowitz and A. Voronkov, editors), Springer, Yerevan, 2007, pp. 92–106.

[3] J.-Y. Girard, Linear logic. Theoretical Computer Science , vol. 50 (1987), no. 1, pp. 1–102.

[4] M. Manighetti and D. Miller, Peano arithmetic and $\mu $ MALL, Fundamenta Informaticae , to appear, arXiv:2312.13634.

Abstracts of invited talks in the Special Session on Set Theory

▸JAN GREBÍK, Poisson-Voronoi percolation in higher rank.

Institute of Mathematics, Universität Leipzig, Augustusplatz 10, Leipzig 04109, Germany.

E-mail: grebikj@gmail.com.

The Poisson–Voronoi percolation model on a locally compact metric space with measure $(M,d,\mu )$ is defined as follows. For $\lambda>0$ , consider a Poisson point process of intensity $\lambda \mu $ and associate to each point its Voronoi cell, that is the set of all points in M closer to this point than to any other point of the Poisson process. For $p\in (0,1)$ , erase each cell with probability p independently of all other cells. This defines a random closed subset $\omega $ of M that is the Poisson–Voronoi percolation model with parameters $(\lambda ,p)$ .

We show that the uniqueness thresholds for Poisson–Voronoi percolation in higher rank symmetric spaces of non-compact connected semisimple Lie groups with property (T) converge to zero in the low-intensity limit. This phenomenon is fundamentally different from situations in which Poisson–Voronoi percolation has previously been studied. Our approach builds on a recent breakthrough of Fraczyk, Mellick, and Wilkens and provides an alternative proof strategy for Gaboriau’s fixed price problem. As a further application of our result, we describe a class of examples of non-amenable Cayley graphs that admits factor of iid bond percolations with a unique infinite cluster and arbitrarily small expected degree, giving an answer to a question of Pete and Rokob.

All of this is joint work with Konstantin Recke.

▸RAHMAN MOHAMMADPOUR, A very strong higher guessing model principle.

Institute of Mathematics of the Polish Academy of Sciences (Gdansk branch), Antoniego Abrahama 18, 81-825 Sopot, Poland.

E-mail: rahmanmohammadpour@gmail.com.

I will talk about joint work with Boban Veličković [1, 2], where we used the novel forcing technique of side conditions with virtual models to show the consistency of a guessing model principle with very strong consequences. These results partially fulfil our expectations for a hypothetical higher analogue of strong forcing axioms like $\mathrm {PFA}$ and $\mathrm {MM}$ .

[1] R. Mohammadpour and B. Veli ković, Guessing models and the approachability ideal. Journal of Mathematical Logic , vol. 21 (2021), no. 2, pp. 2150003.

[2] R. Mohammadpour and B. Veli ković, On indestructible strongly guessing models. Journal of Symbolic Logic , to appear.

▸JONATHAN SCHILHAN, Properness and universal domination.

Institute of Mathematics, University of Vienna, Kolingasse 14–16, 1090 Vienna, Austria.

E-mail: jonathan.schilhan@univie.ac.at

Given a relation R on the reals, we say that a set A is $\omega $ -dominating (with respect to that relation) if for any reals $\langle x_n : n \in \omega \rangle $ there is $y \in A$ with $x_n R y$ , for all n. A natural and canonical forcing for adding a real dominating the ground model with respect to R is the forcing consisting of Borel $\omega $ -dominating sets. For example, this gives rise to Sacks forcing when R is $\neq $ or Miller forcing when R is $\not>^*$ . We study the properness of such forcings more generally using a notion that we call “universal domination”. For instance dominating forcing (naturally adding a $<^*$ -dominating real) is proper, while the forcing for eventually different reals is improper below some condition.

Abstracts of contributed talks

▸JUAN P. AGUILERA, FERNANDO BARRERA, AND GRIGORII STEPANOV, The modal logic of forcing and inner models.

Institut für Diskrete Mathematik und Geometrie, Technische Universität Wien, Wiedner Hauptstraße 8-10/104, 1040 Vienna, Austria.

E-mail: aguilera@logic.at.

E-mail: f.barrera.esteban@gmail.com.

E-mail: grigorii.stepanov@tuwien.ac.at

In this talk, I will present recent work on the interplay between modal logic and set theory. Building on earlier work by Hamkins, Inamdar, Leibman, and Löwe, we study the combined modal logic of forcing and grounds, as well as forcing and inner models. In these systems, one modal operator is interpreted as “true in every forcing extension,” while the other is interpreted either as “true in every ground” or “true in every inner model,” depending on the context. We formulate bi-modal systems that intend to axiomatize the interaction between the relevant modal operators. For the first system, we establish completeness with respect to appropriate classes of Kripke frames, and subsequently derive completeness results for the corresponding set-theoretic interpretations. For the second system, we also establish Kripke completeness, and discuss the obstacles faced so far towards a full completeness result. This is joint work with Juan P. Aguilera and Grigorii Stepanov.

▸SARA AYHAN, Contradictions without negation and a proof-theoretic understanding of connexive logics.

Institute of Philosophy I, Ruhr University Bochum, Bochum 44801, Germany.

E-mail: ilsara.ayhan@rub.de.

URL Address: https://sites.google.com/view/sara-ayhan.

The study of connexive logics has undergone a recent increase in attention. A usual conception of these contra-classical systems is that (among further conditions) they validate theorems called Aristotle’s Theses and Boethius’ Theses, which are non-theorems of classical logic. A standard example for a formulation of Aristotle’s Thesis is the following: ${\sim }({\sim }A \rightarrow A)$ , expressing that no formula is implied by its own negation. A prominent system among these is Wansing’s (2005) logic C, which is also a non-trivial negation-inconsistent logic (also called contradictory logics) in the sense that it contains formulas of the form A and ${\sim } A$ among its theorems. Thus, both the conception of connexive and of contradictory logics seem to rely heavily on the presence of a negation.

I will show, though, that this is not necessarily the case. Therefore, I will present and discuss the negation-free fragment of a bilateralist version of C. With this approach, firstly, a different notion of contradictory logics that does not rely on negation inconsistency but rather on a primitive notion of refutation will be motivated. Secondly, I will propose a change of the usual definition commonly given for connexive logics. Though there are different proposals for definitions of (different forms of) connexive logics, what they all have in common is that they focus on whether or not certain formulas are validated. My definition will radically break with these definitions by purely relying on a rule-based account of connexivity. Thus, I will propose a conception of connexive logics based on (bilateralist) proof-theoretic semantics.

[1] H. Wansing, Connexive modal logic, Advances in Modal Logic, vol. 5 (R. Schmidt, I. Pratt-Hartmann, M. Reynolds, and H. Wansing, editors), College Publications, London, 2005, pp. 367–383.

▸LUIS F. BARTOLO ALEGRE, A formal characterisation of logical theories.

Munich Center for Mathematical Philosophy, Ludwig-Maximilians-Universität München, Ludwigstraße 31, 80539 Munich, Germany.

E-mail: l.bartolo@campus.lmu.de.

In this talk, I propose a formal characterisation of logical theories. A logical theory is an account of inference which is often formalised by means of a logical system—i.e., a logical consequence relation on a formal language. However, as Hjortland notes [4, 252–3], a logical theory is more than a formal system. The significance of this distinction, however, becomes apparent only when we question the thesis that logic is topic-neutral. This thesis states that any logical consequence relation which is considered correct must be correct for any topic or context. Although topic-neutrality is often regarded as a defining attribute of logic (cf. [3, 6]), some authors have questioned this idea stating that some logical systems might be appropriate to some contexts or topics but inappropriate to others. This has resulted in views such as logical contextualism [1] and logical modalism [2], the latter explicitly defending that logic is topic-specific.

In formal terms, a logical theory is a set of statements structured by a three-tuple $\mathfrak {L}=\langle \mathcal {T}, \mathcal {L}, \mathbf {C}\rangle $ such that: $\mathcal {T}$ is a set of topics; $\mathcal {L}$ is the set of formal systems which satisfy the minimal criteria for logicality according to our theory; and $\mathbf {C} \subset \mathcal {T} \times \mathcal {S}$ is a relation establishing which logical systems in $\mathcal {L}$ are correctly applied to which topics in $\mathcal {T}$ .

[1] D. Batens, Meaning, acceptance and dialectics, Change and Progress in Modern Science (J. C. Pitt, editor), Reidel, Dordrecht, 1985, pp. 333–60.

[2] O. Bueno, Modality and the plurality of logics, The Routledge Handbook of Modality (O. Bueno and S. A. Shalkowski, editors), Routledge, London, 2021, pp. 319–27.

[3] C. D. Novaes, The different ways in which logic is (said to be) formal. History and Philosophy of Logic , vol. 32 (2011), no. 4, pp. 303–32.

[4] O. Th. Hjortland, What counts as evidence for a logical theory? The Australasian Journal of Logic , vol. 7 (2019), no. 7, pp. 250–82.

[5] S. Shapiro, Varieties of Logic , Oxford University Press, Oxford, 2014.

[6] J. Woleński, Universality of logic. Bulletin of the Section of Logic , vol. 46 (2017), nos. 1–2, pp. 21–32.

▸DANA BARTOŠOVÁ AND LYNN SCOW, Semi-retractions and pre-adjunction as a measure of complexity of Ramsey theorems.

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

E-mail: dbartosova@ufl.edu.

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

E-mail: lscow@csusb.edu.

We will describe a model-theoretic notion of semi-retraction introduced by the second author in [3] for her interest in generalized indiscernible sequences. We found optimal conditions under which semi-retractions transfer the Ramsey phenomena from one class of finitely generated structures to another in [1]. We compare the notion of semi-retraction to that of pre-adjunction studied by Mašulović (first in [2]) for its transfer of the Ramsey property.

[1] D. Bartošová and L. Scow, A new perspective on semi-retractions and the Ramsey property. Journal of Symbolic Logic , vol. 89 (2024), no. 3, pp. 1–33.

[2] D. Mašulović, Pre-adjunctions and the Ramsey property. European Journal of Combinatorics , vol. 70 (2018), pp. 268–283.

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

▸JEREMY BEARD AND MARCOS MAZARI-ARMIDA, On the spectrum of limit models.

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

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

URL Address: https://jeremypbeard.github.io/.

Department of Mathematics, Baylor University, Waco, TX 76706 USA.

E-mail: marcos_mazari@baylor.edu.

URL Address: https://sites.baylor.edu/marcos_mazari/.

Limit models, originally introduced by Kolmann and Shelah as a surrogate for saturated models, have proved to be a key notion for extending the classification theory of first-order model theory to abstract elementary classes (AECs). In particular, the question of which limit models are isomorphic has proved important when approaching the main test question of AECs, Shelah’s categoricity conjecture [2, 3].

In this talk, we present a full characterisation of the spectrum of limit models under reasonable assumptions: all ‘long’ limit models are isomorphic, and all ‘short’ limit models are non-isomorphic.

Both implications in the conclusion have improvements. High cofinality limits are isomorphic without the $\aleph _0$ -tameness assumption and assuming is defined only on high cofinality limit models. Low cofinality limits are non-isomorphic without assuming non-forking amalgamation.

Our results can be used to study limit models in both abstract settings and in natural examples of abstract elementary classes.

This abstract and talk are based on [1].

[1] J. Beard and M. Mazari-Armida, On the spectrum of limit models, preprint. https://arxiv.org/abs/2503.11605

[2] S. Shelah and S. Vasey, Categoricity and multidimensional diagrams. Journal of the European Mathematical Society , vol. 26 (2024), no. 7, pp. 2301–2372.

[3] S. Vasey, The categoricity spectrum of large abstract elementary classes, Selecta Mathematica , vol. 23 (2019), no. 5, p. 65, 51 pp.

▸CÉLIA BORLIDO, GANNA KUDRYAVTSEVA, AND BRETT MCLEAN, Difference–restriction algebras with operators.

Department of Mathematics, Faculty of Science and Technology, University of Coimbra, Largo D. Dinis, 3000-143 Coimbra, Portugal.

E-mail: cborlido@mat.uc.pt.

Faculty of Mathematics and Physics/Institute of Mathematics, Physics and Mechanics, University of Ljubljana, Ljubljana 1000, Slovenia.

E-mail: ganna.kudryavtseva@fmf.uni-lj.si.

Department of Mathematics WE16, Ghent University, Krijgslaan 281-S8, 9000 Ghent, Belgium.

E-mail: brett.mclean@ugent.be.

We exhibit an adjunction between a category of abstract algebras of partial functions that we call difference–restriction algebras and a category of Hausdorff étale spaces. Difference–restriction algebras are those algebras isomorphic to a collection of partial functions closed under relative complement and domain restriction [1]; the morphisms are the homomorphisms. Our adjunction generalises the adjunction between the generalised Boolean algebras and the category of Hausdorff spaces. We define the finitary compatible completion of a difference–restriction algebra, and show that the monad induced by our adjunction yields the finitary compatible completion of any difference–restriction algebra. The adjunction restricts to a duality between the finitarily complete difference–restriction algebras and the locally compact zero-dimensional Hausdorff étale spaces, generalising the duality between generalised Boolean algebras and locally compact zero-dimensional Hausdorff spaces. We then extend these adjunction, duality, and completion results to difference–restriction algebras equipped with arbitrary additional compatibility preserving operators. A ‘discrete’ version of these results appeared in [2]; this is their topologised counterpart.

[1] C. Borlido and B. McLean, Difference–restriction algebras of partial functions: axiomatisations and representations. Algebra Universalis , vol. 83 (2022), no. 3.

[2] C. Borlido and B. McLean, Difference–restriction algebras of partial functions: discrete duality and completion. Journal of Algebra , vol. 604 (2022), no. 3, pp. 760–789.

▸SAMUEL BRAUNFELD, COLIN JAHEL, AND PAOLO MARIMON, When invariance implies exchangeability.

E-mail: sbraunfeld@iuuk.mff.cuni.cz.

E-mail: cj21@aub.edu.lb.

Institut für Diskrete Mathematik & Geometrie, TU Wien, Wiedner Hauptstraße 8–10/104, 1040 Wien, Austria.

E-mail: paolo.marimon@tuwien.ac.at.

We study the problem of when, given a countable homogeneous structure M and a space S of expansions of M, every $\mathrm {Aut}(M)$ -invariant probability measure on S is exchangeable (i.e., invariant under all permutations of the domain). We show, for example, that if M is a finitely bounded homogeneous $3$ -hypergraph with free amalgamation (including the generic tetrahedron-free $3$ -hypergraph), all $\mathrm {Aut}(M)$ -invariant random expansions by graphs are exchangeable. We extend and recover both the work of Angel, Kechris, and Lyons [1] on invariant random orderings and some of the work of Crane and Towsner [3] on relative exchangeability. Invariant Keisler measures, a natural notion of size on the definable subsets of a structure, are a special case of the context we study. Hence, our work allows us to describe the spaces of invariant Keisler measures of various homogeneous structures beyond the reach of previous techniques. In particular, we show there are $2^{\aleph _0}$ supersimple homogeneous ternary structures for which there are non-forking formulas which are assigned measure zero by every invariant Keisler measures, giving tame examples of the phenomenon first observed in [2].

[1] O. Angel, A. S. Kechris, and R. Lyons, Random orderings and unique ergodicity of automorphism groups. Journal of the European Mathematical Society , vol. 16 (2014), no. 10, pp. 2059–2095.

[2] A. Chernikov, E. Hrushovski, A. Kruckman, K. Krupiński, S. Moconja, A. Pillay, and N. Ramsey, Invariant measures in simple and in small theories. Journal of Mathematical Logic , vol. 23 (2023), no. 2, p. 2250025.

[3] H. Crane and H. Towsner, Relatively exchangeable structures. The Journal of Symbolic Logic , vol. 83 (2018), no. 2, pp. 416–442.

▸JÖRG BRENDLE, The splitting number for mad families.

Graduate School of System Informatics, Kobe University, Rokkodai-cho 1-1, Nada-ku, Kobe 657-8501, Japan.

E-mail: brendle@kobe-u.ac.jp

Given an ideal ${\mathcal I}$ on the natural numbers $\omega $ , we may consider cardinal invariants of the quotient structure ${\mathcal P} (\omega ) / {\mathcal I}$ and compare them to the corresponding classical cardinal invariants of ${\mathcal P} (\omega ) / {\mathrm {fin}}$ . While a lot is known about such cardinals in case ${\mathcal I} $ is a Borel ideal, this is not so if $ {\mathcal I}$ non-definable, e.g., if ${\mathcal I} = {\mathcal I} ( {\mathcal A})$ is the ideal generated by a maximal almost disjoint (mad) family ${\mathcal A}$ of subsets of $\omega $ . For the splitting number ${\mathfrak s} ({\mathcal A}) $ of the quotient ${\mathcal P} (\omega ) / {\mathcal I} ({\mathcal A})$ , it is known that $\min \{ {\mathfrak b} , {\mathfrak s} \} \leq {\mathfrak s} ({\mathcal A}) \leq {\mathfrak s}$ (results of Yhon Castro and others). Using a matrix iteration, we prove that it is consistent that there exists a mad family ${\mathcal A}$ such that ${\mathfrak s} ({\mathcal A}) < {\mathfrak s}$ . The talk will present both an introduction to the area of research and a sketch of the proof of this result. This is joint work with Hiroaki Minami.

▸GABRIELE BURIOLA AND ANDREAS WEIERMANN, Ordinal analysis of well-ordering principles and well quasi-orders properties.

Department of Computer Science, University of Verona, Verona 37129, Italy.

E-mail: Gabriele.Buriola@UniVr.it.

Department of Mathematics, University of Ghent, Ghent 9000, Belgium.

E-mail: Andreas.Weiermann@UGent.be

This contribution deals with two well-established topics in proof theory: well-ordering principles [3, 5] and well quasi-order closure properties [2, 4]. The former refers to the property of ordinal functions to preserve well-orderedness; more precisely, given an ordinal function g $\colon \Omega \rightarrow \Omega $ , the Well-Ordering Principle of ${\texttt {g}}$ , WOP( ${\texttt {g}}$ ), amounts to the following sentence:

where $WO(X)$ denotes the fact that X is a well-order.

For what concerns well quasi-orders, the situation is as follows: let $\mathcal {G}$ be a set operation, we consider its Well-Quasi order closure Property, WQP $(\mathcal {G})$ , asserting that any finite iteration of $\mathcal {G}$ preserves the property of being a well quasi-order:

Extending some previous results [1], our aim is to measure the $\Pi ^1_1$ proof-theoretic ordinals of some WOP’s and WQP’s over RCA $_0$ , the base theory of reverse mathematics [6]. In particular, we compute the ordinals for the WOP’s corresponding to the following ordinal functions:

Regarding well quasi-orders instead, we give preliminary estimates for the proof-theoretic ordinals of the following WQP’s that involve, respectively, the product, the sum, and the disjoint union of well quasi-orders:

1. 1. WQP $(\times ):\ \forall n\, \forall Q\, [Q\, \mbox {{wqo}} \, \rightarrow \, \underbrace {Q \times \dots \times Q}_{n \, \mbox {times}}\, \mbox {{wqo}}]$ ;

2. 2. WQP $(+):\ \forall n\, \forall Q\, [Q\, \mbox {{wqo}} \, \rightarrow \, \underbrace {Q + \dots + Q}_{n \, \mbox {times}}\, \mbox {{wqo}}]$ ;

3. 3. WQP $(\dot {\cup }):\ \forall n\, \forall Q\, [Q\, \mbox {{wqo}} \, \rightarrow \, \underbrace {Q \, \dot {\cup } \dots \dot {\cup } \, Q}_{n \, \mbox {times}}\, \mbox {{wqo}}]$ .

[1] G. Buriola, Proof-Theoretical Aspects of Well Quasi-Orders and Phase Transitions in Arithmetical Provability , Ph.D. thesis, University of Trento, 2024.

[2] P. Cholak, A. Marcone, and R. Solomon, Reverse mathematics and the equivalence of definitions for well and better quasi-orders. The Journal of Symbolic Logic , vol. 69 (2004), no. 3, pp. 683–712.

[3] A. Freund and M. Rathjen, Well ordering principles for iterated $\Pi ^1_1$ -comprehension. Selecta mathematica , vol. 29 (2023), no. 5.

[4] A. Marcone, The Reverse mathematics of wqos and bqos, Well-Quasi Orders in Computation, Logic, Language and Reasoning (P. M. Schuster, M. Seisenberger, and A. Weiermann, editors), Springer, 2020, pp. 189–219.

[5] M. Rathjen, Well-ordering principles in proof theory and reverse mathematics, Axiomatic Thinking II (F. Ferreira, R. Kahle, and G. Sommaruga, editors), Springer, 2022, pp. 89–127.

[6] S. G. Simpson, Subsystems of Second Order Arithmetic , Perspectives in Logic, Cambridge University Press, 2009.

▸GUSTAVO CIPAGAUTA AND ANDRÉS VILLAVECES, Elementary equivalence in stochastics structures.

Department of Mathematics, National University of Colombia, Bogotá 111321, Colombia.

E-mail: gdcipagautac@unal.edu.co.

E-mail: avillavecesn@unal.edu.co.

The concept of elementary equivalence (and elementary substructure, elementary extension, Ehrenfeucht–Fraïssé game) are at the heart of model theory. In the case of stochastic structures—whose bases are the adapted probability spaces—Keisler, Hoover, and Fajardo defined elementary equivalence and the Ehrenfeucht–Fraïssé game in the framework of the adapted probability logic. In our ongoing doctoral research work, we have set out to extend these results in two directions: (i) mixing the logic of Keisler with the continuous logic—developed for metric structures—, enhancing the correspondence between syntax and semantics (overcoming some expressivity limitations pointed out by Hrushovski) and (ii) exploring the possibility of defining the concept of abstract elementary class for stochastic structures, opening the door to implement notions of classification that complement those developed by Keisler and company. We seek, in the end, to apply these model-theoretical tools to compare stochastic processes that shed light on the dividing lines within quantum phenomenology and between it and classical phenomenology.

[1] I. B. Yaacov, A. Berenstein, C. W. Henson and A. Usvyatsov, Model theory for metric structures, Model Theory with Applications to Algebra and Analysis (Z. Chatzidakis, D. Macpherson, A. Pillay, and A. Wilkie, editors), London Mathematical Society, Cambridge University Press, 2008, pp. 315–427.

[2] S. Fajardo, Elementary embeddings and games in adapted probability logic. Archive for Mathematical Logic , vol. 30 (1990), pp. 49–58.

[3] S. Fajardo and J. Keisler, Model Theory of Stochastic Processes , Lecture Notes in Logic, Cambridge University Press, 2002.

[4] D. Hoover and J. Keisler, Adapted probability distributions. Transactions of the American Mathematical Society , vol. 286 (1984), no. 1, pp. 159–201.

▸HUIMIN DONG, Permissible shared knowledge.

Institute of Logic and Computation, Faculty of Informatics, TU Wien, 1040 Vienna, Austria.

E-mail: huimin@logic.at.

Information is exchanged and shared, but it is possible for an agent to gain knowledge that they are not authorised to know. How can we represent and reason about permissible shared knowledge? Information exchange has been extensively formalised across various logical frameworks in distributed systems [2, 1], each characterized by distinct information-sharing patterns. These approaches generally adopt an intersection perspective, aggregating all possible information regardless of whether it is known or unknown to the agents. In contrast, this work takes a distinct approach, emphasising that sharing knowledge means distributing what is known, rather than what remains uncertain.

This article introduces a new modality $[\equiv _a]$ called information sufficiency, which captures the distinction between implicit to explicit knowledge in the information distribution process. Here, $[\equiv _a]\varphi $ is read as “ $\varphi $ provides sufficient information to understand what a knows.” The non-normal modality of sufficiency has been applied to capture the concept of strong permission, a notion originating in von Wright’s 1951 work [6]. While the modal logic of sufficiency can be traced to van Benthem’s minimal deontic logic [4], subsequent development has expanded beyond deontic logic into a more general logical framework by Humberstone [3].

My paper presents an epistemic variant of sufficiency through the modality $[\equiv _a]$ . Its interpretation via the relation $\equiv _a$ , constructed as a ceteris paribus relation [5] from the equivalence relation $R_a$ for the S5 modality $K_a$ of knowledge, serves as a crucial technical component in constructing canonical models.

This epistemic modality of sufficiency provides a new logical framework for shared knowledge, applicable not only to individual knowledge sharing but also to group sharing, with a strongly complete axiomatization for common knowledge. Furthermore, based on this epistemic account, I explore a new modal logic concerning the interaction between permission and information exchange, where permission to know is restricted to group membership.

[1] A. Baltag and S. Smets, Learning What Others Know, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Alicante, Spain, May 2020), vol. 73 (E. Albert and L. Kovács, editors), EPiC Series in Computing, EasyChair, 2020, pp. 90–119.

[2] R. Galimullin and L. B. Kuijer, Varieties of Distributed Knowledge, Advances in Modal Logic, vol. 15 (A. Ciabattoni, D. Gabelaia, and I. Sedlár, editors), College Publications, 2024, pp. 379–400.

[3] I. L. Humberstone, Inaccessible worlds. Notre Dame Journal of Formal Logic , vol. 24 (1983), no. 3, pp. 346–352.

[4] J. van Benthem, Minimal deontic logics. Bulletin of the Section of Logic , vol. 8 (1979), no. 1, pp. 36–42.

[5] J. van Benthem, P. Girard, and O. Roy, Everything else being equal: A modal logic for ceteris paribus preferences. Journal of Philosophical Logic , vol. 38 (2009), no. 1, pp. 83–125.

[6] G. H. von Wright, Deontic logic. Mind , vol. 60 (1951), no. 237, pp. 1–15.

▸PABLO DOPICO, Supervaluations, truth, and intuitionistic logic.

Department of Philosophy, King’s College London, Strand, London WC2R 2LS, UK, and Department of Philosophy, Humboldt Universität zu Berlin, Unter den Linden 6, 10117 Berlin, Germany.

E-mail: pablo.dopico@kcl.ac.uk.

In [2], Kripke proposed his well-known theory of truth based on a fixed-point construction. While the construction has most often been carried out on the basis of the Strong Kleene scheme, Kripke also suggested to employ some form of supervaluationist scheme in the style of [3]. Naturally, van Fraassen’s scheme is based on classical logic. But there are both technical and philosophical motivations for developing a supervaluationist theory of truth over intuitionistic logic instead. That is the goal of this article. In particular, we show how to do supervaluations over Kripke structures for intuitionistic logic, and we obtain the corresponding semantic fixed-point construction that yields a theory of truth in the style of Kripke. Moreover, we also propose an axiomatization of this construction, in the style of the celebrated theory VF of Cantini [1]. Finally, we show how the theory of truth changes when the Kripke structures over which the supervaluations are defined change. Specifically, we look at the theory of truth when supervaluations are defined over: (i) Kripke structures with varying domains and (ii) non-hereditary Kripke structures.

[1] A. Cantini, A theory of formal truth arithmetically equivalent to ID $_1$ . Journal of Symbolic Logic , vol. 55 (1990), no. 1, pp. 244–259.

[2] S. Kripke, Outline of a theory of truth. The Journal of Philosophy , vol. 72 (1975), no. 19, pp. 690–716.

[3] B. C. van Fraassen, Singular terms, truth-value gaps, and free logic. The Journal of Philosophy , vol. 63 (1966), no. 17, pp. 481–495.

▸DARIEN FARNHAM, Quasi-finite axiomatizability of automorphism groups of symplectic manifolds.

Department of Mathematics, University of Virginia, Kerchof Hall, 141 Cabell Dr, Charlottesville, VA 22903, USA.

E-mail: qzr2cy@virginia.edu

It has recently been shown by Kim, Koberda, and de la Nuez González that compact topological manifolds are determined by (a finite fragment of) the first-order theory of their automorphism groups.

The key idea is to use Rubin’s theory of “locally moving” groups [2] to interpret second-order arithmetic in $ \text {Homeo}(M)$ , thereby enabling one to express topological properties of M within the first-order theory of $\text {Homeo}(M)$ , using only the language of groups.

In this talk, we explore the expressive power of the first-order theory of automorphism groups of symplectic manifolds.

I will present partial progress toward a proof of this conjecture, including a method for interpretation of second-order arithmetic in $\text {Aut}(M)$ , and will illustrate the striking blend of topological flexibility with geometric rigidity in the symplectic context. This work is part of my doctoral research.

[1] S.-h. Kim, T. Koberda and J. de la Nuez González, First order rigidity of homeomorphism groups of manifolds, Communications of the American Mathematical Society , to appear.

[2] M. Rubin, Locally moving groups and reconstruction problems, Ordered Groups and Infinite Permutation Groups , Kluwer Academic Publishers, 1996, pp. 121–157.

▸PAULO FIRMINO AND LAURENŢIU LEUŞTEAN, Proof mining in nonlinear analysis.

Departamento de Matemática, Faculdade de Ciências, Universidade de Lisboa, Lisbon 1649-004, Portugal.

E-mail: fc49883@alunos.ciencias.ulisboa.pt.

LOS, Faculty of Mathematics and Computer Science, University of Bucharest, Bucharest 030018, Romania,

Simion Stoilow Institute of Mathematics of the Romanian Academy (IMAR), Bucharest 010702, Romania, and

Institute for Logic and Data Science, Bucharest 010805, Romania.

E-mail: laurentiu.leustean@unibuc.ro

This talk presents a recent application in nonlinear analysis of proof mining, an area of applied proof theory developed by Ulrich Kohlenbach beginning with the 1990s.

Let X be a normed space and $T:X\to X$ be a nonexpansive mapping with fixed points. The generalized Krasnoselskii–Mann-type iteration, studied recently in [3, 7], is defined as follows:

where $(r_n)_{n \in \mathbb {N}} \subseteq X$ and $(\alpha _n)_{n \in \mathbb {N}}, \,(\beta _n)_{n \in \mathbb {N}} \subseteq [0,1]$ satisfy $\alpha _n+\beta _n \le 1$ for all $n\in \mathbb {N}$ .

We compute in [1] uniform rates of asymptotic regularity for this iteration in uniformly convex Banach spaces. For special choices of the parameter sequences, we obtain quadratic rates.

The proof mining methods that we use to obtain these quantitative results, developed in [5, 6], are based on a combination of two logical metatheorems: one for classical systems [4] and another for semi-constructive systems [2].

[1] P. Firmino and L. Leuştean, Rates of (T-)asymptotic regularity of the generalized Krasnoselskii–Mann-type iteration, Portugaliae Mathematica , (2025).

[2] P. Gerhardy and U. Kohlenbach, Strongly uniform bounds from semi-constructive proofs. Annals of Pure and Applied Logic , vol. 141 (2006), pp. 89–107.

[3] C. Kanzow and Y. Shehu, Generalized Krasnoselskii–Mann-type iterations for nonexpansive mappings in Hilbert spaces. Computational Optimization and Applications , vol. 67 (2017), pp. 595–620.

[4] U. Kohlenbach, Some logical metatheorems with applications in functional analysis. Transactions of the American Mathematical Society , vol. 357 (2005), pp. 89–128.

[5] L. Leuştean, Nonexpansive iterations in uniformly convex W-hyperbolic spaces, Nonlinear Analysis and Optimization I: Nonlinear Analysis (B. S. Mordukhovich, I. Shafrir, and A. Zaslavski, editors), Contemporary Mathematics, 513, American Mathematical Society, 2010, pp. 193–209.

[6] L. Leuştean, An application of proof mining to nonlinear iterations. Annals of Pure and Applied Logic , vol. 165 (2014), pp. 1484–1500.

[7] Y.-C. Zhang, K. Guo, and T. Wang, Generalized Krasnoselskii–Mann-Type iteration for nonexpansive mappings in Banach spaces. Journal of the Operations Research Society of China , vol. 9 (2021), pp. 195–206.

▸GUNTER FUCHS, A new context for the strong reflection principle.

Department of Mathematics, College of Staten Island, City University of New York, New York, NY 10017, USA.

E-mail: gunter.fuchs@csi.cuny.edu.

There is a natural way to formulate fragments of Todorcevic’s strong reflection principle (SRP) which are associated with forcing classes more restrictive than all stationary set preserving forcing. The fragment associated with the subcomplete forcings, while retaining many crucial consequences of SRP, is compatible with CH, and even diamond. An surprising phenomenon arising here is that the weaker principle, when paired with CH, has more far reaching consequences in terms of diagonal reflection than the original, stronger principle. I will describe several instances of this phenomenon.

This is joint work with Hiroshi Sakai.

▸JAMES E. HANSON, Special coheirs and model-theoretic trees.

Department of Mathematics, Iowa State University, 411 Morrill Road, Ames, IA 50011, USA.

E-mail: jameseh@iastate.edu.

In neostability theory, the two broadest classes of first-order theories with good structure theory are NTP $_2$ and NSOP $_1$ . As these two classes are incomparable, there has been some interest in finding a mutual generalization. The class of theories without the comb tree property is one of three such generalizations that have appeared in the literature. We will discuss a characterization of this property in terms of a variant of Kim’s lemma involving special coheirs.

▸VICENT NAVARRO ARROYO AND JOOST J. JOOSTEN, Principles of interpretability logic in the intersection of $\mathbf {IL}\mathsf {P}$ and $\mathbf {IL}\mathsf {M}$ .

Department of Philosophy, University of Barcelona, Carrer Montealegre 6, Barcelona 08007, Spain.

E-mail: vicent.navarro@ub.edu.

E-mail: jjoosten@ub.edu.

URL Address: http://www.joostjjoosten.nl/.

Interpretability logics are genuine extensions of the provability logic $\mathbf {GL}$ . The logic $\mathbf {GL}$ is the provability logic of any theory that contains enough arithmetic, like $\mathsf {ZFC}$ , $\mathsf {PA}$ , $\mathsf {I}\Sigma ^0_1$ , etc. The situation is very different for interpretability logics where different theories have different logics. In [1] a conjecture is proposed for the core logic $\mathbf {IL}(\mathsf {All})$ : the logic that generates principles that are provably valid in any theory that contains enough arithmetic. The conjecture can be phrased as

where $\mathbf {IL}(\mathfrak {All})$ is defined to be the set of modal interpretability principles that hold on a certain class $\mathfrak {All}$ of Veltman frames.

In this talk we comment on recent progress on the conjecture. Firstly, we see how the class of Veltman frames $\mathfrak {All}$ can be substantially restricted while still generating all known valid principles. Secondly, we see how various natural frame restrictions give rise to modally undefinable properties. Lastly, we report how purely modal semantic considerations give rise to new valid arithmetical principles.

[1] E. Goris and J. J. Joosten, Two new series of principles in the interpretability logic of all reasonable arithmetical theories. The Journal of Symbolic Logic , vol. 85 (2020), no. 1, pp. 1–25.

▸DARIUSZ KALOCIŃSKI, More acceptable notation.

Institute of Computer Science, Polish Academy of Sciences, Warsaw 00-901, Poland.

E-mail: dariusz.kalocinski@ipipan.waw.pl

A notation for natural numbers is a bijection from a decidable set of strings (numerals) to $\mathbb N$ . We say that a function on $\mathbb N$ is computable in a notation d if its preimage under d is a computable function on strings. A notation d is acceptable if the functions computable in d are the same as standard computable functions. Shapiro examined which notations are acceptable and provided several natural criteria.

We introduce a stronger notion of acceptability: a notation is acceptable for primitive recursion if the class of functions that are primitive recursive in it coincides with the class of standard primitive recursive functions. Through a series of examples, we demonstrate that Shapiro’s acceptability criteria no longer apply in this context. Additionally, we develop new criteria that are suitable for this stricter version of acceptability. Along the way, we explore connections to the philosophy of mathematics and computation, as well as to punctual structure theory.

This is a joint work with Paula Quinon, Luca San Mauro, and Michał Wrocławski.

[1] S. Shapiro, Acceptable notation. Notre Dame Journal of Formal Logic , vol. 23 (1982), no. 1, pp. 14–20.

▸HARUKA KOGURE AND TAISHI KURAHASHI, Some results on partially conservative sentences.

Graduate School of System Informatics, Kobe University, Kobe 657-8501, Japan.

E-mail: kogure@stu.kobe-u.ac.jp.

E-mail: kurahashi@people.kobe-u.ac.jp.

Partially conservative sentences have been studied in the context of the incompleteness theorems. Let T and U denote consistent RE extensions of Peano Arithmetic. For a class $\Gamma $ of sentences, a sentence $\varphi $ is said to be $\Gamma $ -conservative over T if every $\Gamma $ sentence provable in $T+\varphi $ is already provable in T.

In this talk, we present the following three results proved in our papers [2, 3].

1. 1. We proved the existence of a $\Theta $ sentence which is simultaneously $\Gamma $ -conservative over T and U for various reasonable pairs $(\Gamma , \Theta )$ . This is a continuation of the work of Kurahashi, Okawa, Shavrukov, and Visser [4].

2. 2. As a result of the first study, we proved the existence of a sentence which is essentially $\Theta $ and exactly hereditarily $\Gamma $ -conservative over T for various reasonable pairs $(\Gamma , \Theta )$ . This is an affirmative answer to Guaspari’s question [p. 62, Question (2)] in a more refined form.

3. 3. We studied several variants of Solovay’s theorem on the existence of doubly partially conservative sentences. Here, a sentence $\varphi $ is doubly $(\Gamma , \Lambda )$ -conservative over T if $\varphi $ and $\neg \varphi $ are $\Gamma $ -conservative and $\Lambda $ -conservative over T, respectively.

[1] D. Guaspari, Partially conservative extensions of arithmetic. Transactions of the American Mathematical Society , vol. 254 (1979), pp. 47–68.

[2] H. Kogure and T. Kurahashi, A variety of partially conservative sentences, preprint, arXiv:2412.08208.

[3] H. Kogure and T. Kurahashi, Doubly partially conservative sentences, preprint, arXiv:2503.12373.

[4] T. Kurahashi, Y. Okawa, V. Yu. Shavrukov, and A. Visser, On Guaspari’s problem about partially conservative sentences. Annals of Pure and Applied Logic , vol. 173 (2022), no. 5, p. 103087.

▸TAISHI KURAHASHI, Lyndon interpolation property for extensions of $\mathbf {S4}$ and intermediate logics.

Graduate School of System Informatics, Kobe University, Kobe 657-8501, Japan.

E-mail: kurahashi@people.kobe-u.ac.jp.

Let $v^+(\varphi )$ (resp., $v^-(\varphi )$ ) be the set of all propositional variables occurring in a propositional formula $\varphi $ positively (resp., negatively). We say that a propositional logic L has the Lyndon interpolation property (LIP) iff for any formulas $\varphi $ and $\psi $ , if $L \vdash \varphi \to \psi $ , then there exists a formula $\rho $ such that $v^\circ (\rho ) \subseteq v^\circ (\varphi ) \cap v^\circ (\psi )$ for $\circ \in \{+, -\}$ , $L \vdash \varphi \to \rho $ , and $L \vdash \rho \to \psi $ . LIP for extensions of $\mathbf {S4}$ has been studied by Maksimova [8, 9], Fitting [1], and Kuznets [4, 5]. It is also verifiable that Shimura’s proofs of the Craig interpolation property (CIP) for some extensions of $\mathbf {S4}$ also work with respect to LIP [10]. In this talk, we show that among the 18 consistent normal modal logics of finite height extending $\mathbf {S4}$ known to have CIP, 11 logics have LIP and 7 logics do not.

LIP for intermediate propositional logics has been studied by Maksimova [8, 9] and Kuznets and Lellmann [6, 7]. Among these 7 logics known to have CIP, LIP for the 6 logics other than $\mathbf {LV}$ has already been proved. In this talk, we also show that for intermediate propositional logics, CIP, LIP, and ULIP [2] are equivalent.

Our presentation is based on [3].

[1] M. Fitting, Proof Methods for Modal and Intuitionistic Logics , Synthese Library, D. Reidel Publishing Co., Dordrecht-Boston, 1983.

[2] T. Kurahashi, Uniform Lyndon interpolation property in propositional modal logics. Archive for Mathematical Logic , vol. 59 (2020), nos. 5–6, pp. 659–678.

[3] T. Kurahashi, Lyndon interpolation property for extensions of $\mathbf {S4}$ and intermediate propositional logics. The Journal of Symbolic Logic , to appear.

[4] R. Kuznets, Proving Craig and Lyndon interpolation using labelled sequent calculi, Logics in Artificial Intelligence Lecture Notes in Computer Science, 10021, Springer, Cham, 2016, pp. 320–335.

[5] R. Kuznets, Multicomponent proof-theoretic method for proving interpolation properties. Annals of Pure and Applied Logic , vol. 169 (2018), no. 12, pp. 1369–1418.

[6] R. Kuznets and B. Lellmann, Interpolation for intermediate logics via hyper- and linear nested sequents, Advances in Modal Logic, vol. 12 , College Publications, London, 2018, pp. 473–492.

[7] R. Kuznets and B. Lellmann, Interpolation for intermediate logics via injective nested sequents. Journal of Logic and Computation , vol. 31 (2021), no. 3, pp. 797–831.

[8] L. L. Maksimova, The Lyndon interpolation theorem in modal logics (in Russian). Mathematical Logic and the Theory of Algorithms , vol. 2 (1982), pp. 45–55.

[9] L. L. Maksimova, The Lyndon property and uniform interpolation over the Grzegorczyk logic (in Russian), Rossiı̆skaya Akademiya Nauk. Sibirskoe Otdelenie. Institut Matematiki im. S. L. Soboleva. Sibirskiı̆ Matematicheskiı̆ Zhurnal , vol. 55 (2014), no. 1, pp. 147–155.

[10] T. Shimura, Cut-free systems for some modal logics containing $\mathrm {S4}$ . Reports on Mathematical Logic , vol. 26 (1992), pp. 39–65.

▸SATORU KURODA, Bounded reverse mathematics of linear algebra.

Faculty of Culture and Informatics, Gunma Prefectural Women’s University, 1395-1, Kaminote, Tamamura, Gunma 370-1127, Japan.

E-mail: satoru@mail.gpwu.ac.jp.

Proving theorems of linear algebra, especially properties of the determinant, is one of the central topics in bounded reverse mathematics. Although the determinant has $\#L$ algorithms, known upper bounds on proving many of its properties are in a theory slightly stronger than $\#L$ . The seminal work of Soltys and Cook [2] revealed that the multiplicativity of the determinant implies the cofactor expansion, the axiomatic definition of the determinant and Cayley–Hamilton Theorem over the theory $\mathbf {V\#L}$ introduced by Cook and Fontes [1]. Another breakthrough was given by Tzameret and Cook [3] who proved that the multiplicativity of the determinant is provable in $\mathbf {VNC}^2$ .

In this talk we discuss the provability of linear algebra properties in these theories. Firstly, we show that matrix rank is formalizable in $\mathbf {V\#L}$ and its fundamental properties are provable in $\mathbf {VNC}^2$ .

Secondly, we show that Pfaffian of skew symmetric matrices of even degree can be formalized in $\mathbf {V\#L}$ and show that a version of the multiplicativity of Pfaffian

is provable in $\mathbf {V\#L}$ .

Finally, we discuss the problem of proving properties of the determinant from equation (0.1).

[1] S. Cook and L. Fontes, Formal theories for linear algebra. Logical Methods in Computer Science , vol. 8 (2012) no. 1:25, pp. 1–31.

[2] M. Soltys and S. A. Cook, The proof complexity of linear algebra. Annals of Pure and Applied Logic , vol. 130 (2004), no. 1–3, pp. 277–323.

[3] I. Tzameret and S. A. Cook, Uniform, integral, and feasible proofs for the determinant identities. Journal of the Association for Computing Machinery , vol. 68 (2021), no. 2, pp. 1–80.

▸ORVAR LORIMER OLSSON, Proof systems for logics in power-algebras from varieties.

Department of Philosophy, Linguistics and Theory of Science; University of Gothenburg, Renströmsgatan 6, Gothenburg 40530, Sweden.

E-mail: orvar.lorimer.olsson@gu.se.

Power-algebras, the algebras of subsets over an underlying algebra inheriting its signature by way of pointwise operations, have been sporadically investigated throughout the past century. An extensive survey is given by Brink [1] who further investigates the power-lifting of relational structures, such as orderings, with an interest in applications in logic. More lately, this type of construction has found new appreciation for logical semantics, both for multivalued logics and notions of plurivalence [3], and in efforts to give algebraic presentations of logics with team semantics [2].

We present a general way of defining a proof system for deriving entailments of membership statements for elements of an algebra as members in elements of its power-algebra. The deductive power of these proof systems fully depends on the deducabillity within the equational theory of the underlying algebra. In doing so we give proof systems for the logic induced by the $\subseteq $ -ordering for classes of power-algebras formed from varieties with well presented equational theories. Furthermore, by extending with some additional rules, we can present proof systems for plurivalent logics for which the semantics is expressed in terms of subsets of a finite algebra of truth values.

[1] C. Brink, Power structures. Algebra Universalis , vol. 30 (1993), pp. 177–216.

[2] F. Engström and O. L. Olsson, The propositional logic of teams, preprint, 2023, arXiv.2303.14022.

[3] G. Priest, Plurivalent logics. The Australasian Journal of Logic , vol. 11 (2014), no. 1.

▸DIEGO A. MEJÍA, Directed schemes of ideals and cardinal characteristics.

Graduate School of System Informatics, Kobe University, 1-1 Rokkodai-cho, Nada-ku, Kobe, Hyogo 657-8501, Japan.

E-mail: damejiag@people.kobe-u.ac.jp.

URL Address: https://researchmap.jp/mejia?lang=en

In 2002, Yorioka [4] introduced the so-called Yorioka ideals to deepen the understanding of the combinatorics of strong measure zero subsets of the reals and show that ZFC does not prove an inequality between the cofinality of the strong measure zero ideal and the size of the continuum. These ideals form an example of what we formalize as directed schemes of ideals.

In this talk, we present the general framework of directed schemes of ideals, generalize results from [4, 1] and show its effect on cardinal characteristics of the continuum. We further show that the ideals of meager-additive sets and null-additive sets can be adapted to this framework, which helps proving consistency results about their cardinal characteristics.

This is a joint work with Miguel Cardona and Ismael Rivera-Madrid [2, 3].

[1] M. A. Cardona and D. A. Mejía, More about the cofinality and the covering of the ideal of strong measure zero sets. Annals of Pure and Applied Logic , vol. 176 (2025), no. 4, Article no. 103537.

[2] M. A. Cardona, D. A. Mejía, and I. E. Rivera-Madrid, Uniformity numbers of the null-additive and meager-additive ideals. The Journal of Symbolic Logic , to appear.

[3] M. A. Cardona, Directed schemes of ideals and cardinal characteristics, I: The meager additive ideal, preprint, 2025.

[4] T. Yorioka, The cofinality of the strong measure zero ideal. The Journal of Symbolic Logic , vol. 67 (2002), no. 4, pp. 1373–1384.

▸RUSSELL MILLER, Computability for the additive group of p-adic integers.

Mathematics Department, Queens College—CUNY, 65-30 Kissena Blvd., Queens, NY 11367, USA.

E-mail: russell.miller@qc.cuny.edu.

We present joint work by Jason Block and the speaker. The additive group $\mathbb {Z}_p$ of all p-adic integers has size continuum, making it unsuitable for traditional computable structure theory. However, it has an extremely natural tree presentation, describing the group as the set of all paths through a computable finite-branching tree T, and is thus subject to the same kind of analysis carried out on profinite groups in Block’s dissertation, or on absolute Galois groups by the speaker. Of course, in a structure of this size, the equality relation (on the paths through T) must be undecidable. Here we will show that this undecidability is the only stumbling block: the atomic diagram and indeed the elementary diagram may both be considered decidable up to the problem of deciding equality, in a way that will be made rigorous in the talk. The group $\mathbb {Z}_p$ , when presented this way, has computable Skolem functions, and the subgroup consisting of all computable p-adic integers is elementary within the entire group.

▸MOJTABA MOJTAHEDI AND BORJA SIERRA MIRANDA, Provability models for modal logics.

Department of Mathematics: Analysis, Logic and Discrete, Ghent University, 9000 Ghent, Belgium.

E-mail: mojtahedy@gmail.com.

URL Address: http://mmojtahedi.ir.

Institut für Informatik, University of Bern, Bern 3012, Switzerland.

E-mail: borja.sierra@unibe.ch.

We introduce a novel Kripke-style semantics for modal logics, referred to as provability models. In this framework, a Kripke model is enriched by assigning a distinct logic to each possible world, and the formula $\Box A$ is interpreted as the derivability of A in the logics associated with all accessible worlds.

We establish soundness and completeness results for various modal logics with respect to this semantics. A significant advantage of provability models lies in their capacity to replace traditional frame conditions with inference rules internal to the logics assigned to individual worlds. However, this expressiveness introduces complexity: the decidability of formula satisfaction at a given world in a given provability model becomes a non-trivial issue, and may not always be guaranteed.

Despite this challenge, we demonstrate that for Gödel–Löb logic ( $\mathsf {GL}$ ), it is possible to construct a provability model for any finite irreflexive frame (not necessarily transitive) and any finite collection of formulas, where each formula serves as an axiom for the logic assigned to a corresponding world. Furthermore, we extend this approach to interpretability logic ( $\mathsf {ILM}$ ), and find—remarkably—that the same class of provability models used for $\mathsf {GL}$ also yields soundness and completeness for $\mathsf {ILM}$ .

The notion of provability models for intuitionistic provability logic was first introduced in [1], where it played a crucial technical role. Notably, it facilitated the construction of a finite and decidable provability model for the provability logic of Heyting Arithmetic ( $\mathsf {HA}$ ).

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

▸JOACHIM MUELLER-THEYS, The Unequality Theorem.

Independent Scholar, Heidelberg, Germany.

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

I. We shall prove that in no universe $ M $ , there exists a normal property with respect to which all $ M $ are equal, whereby a property on $ M $ is called normal if it is neither empty nor total.

We determine that two elements of $ M $ are equal with respect to some property $ P $ on $ M $ —shortly: $ P $ -equal—if both have $ P $ or both do not have $ P $ . For example, Carl XVI Gustaf and Charles III are equal with respect to the property king, but they are also equal with respect to the property plebeian.

We naturally say that all $ M $ are $ P $ -equal if all elements of $ M $ are pairwise $ P $ -equal. However, if $ P $ is any normal property on $ M $ , then it is not the case that all $ M $ are $ P $ -equal. Sketch of proof: Since $ P $ is normal, some $ a _0 \in M $ has $ P $ and some $ b _0 \in M $ does not have $ P $ , whence $ a _0 $ , $ b _0 $ are not $ P $ -equal.

II. Let, more formally, $ a , b , \ldots \in M $ , $ P \subseteq M $ , $ P ( a ) : \Leftrightarrow a \in P $ , and $ \sim $ , &, v, …symbolize negation, conjunction, alternation (“or”), etc.

Definition. $ a \equiv _P b : \Leftrightarrow \big ( P ( a ) $ & $ P ( b ) \big ) $ v $ \big ( \! \sim \! P ( a ) $ & $ \sim \! P ( b ) \big ) $ .

The definiens is logically equivalent to Buchholz’s more abstract one: $ a \equiv _P b \Leftrightarrow \big ( P ( a ) \Leftrightarrow P ( b ) \big ) $ . Thereby equality with respect to all properties coincides with Leibniz’s identitas indiscernibilium: $ a \equiv ^\ast b : \Leftrightarrow \forall P \! \subseteq \! M \ a \equiv _P b \Leftrightarrow \forall P \! \subseteq \! M \, \big ( P ( a ) \Leftrightarrow P ( b ) \big ) \Leftrightarrow : a =_{\mathrm { L.}} b $ . Since $ P ( a ) $ & $ P ( b ) $ and $ \sim \! P ( a ) $ & $ \sim \! P ( b ) $ cannot be true together, $ a \equiv _P b \Leftrightarrow \big ( P ( a ) $ & $ P ( b ) \big ) $ v $ \big ( \! \sim \! P ( a ) $ & $ \sim \! P ( b ) \big ) $ .

By further specifying $ {Empty} _M ( P ): \Leftrightarrow \sim \! \! \exists a \! \in \! M \, P ( a ) $ , $ {Total} _M ( P ) : \Leftrightarrow \forall a \! \in \! M \, P ( a ) $ , $ {Normal} _M ( P ) : \Leftrightarrow \sim \! \mathrm {Empty} _M ( P ) $ & $ \sim \! \mathrm {Total} _M ( P ) $ , and $ {AllEq} _M ( P ) : \Leftrightarrow \forall a , b \in M a \equiv _P b $ , we reach the mathematical form:

Theorem(Mueller–Theys–Buchholz). $ \forall P \subseteq M \ \big ( \mathrm {Normal} _M ( P ) \ \Rightarrow \ \sim \! \mathrm {AllEq} _M ( P ) \big ) $ .

Proof. Since $ \sim \! \mathrm {Empty} _M ( P ) $ , $ P ( a _0 ) $ ; since $ \sim \! \mathrm {Total} _M ( P ) $ , $ \sim \! P ( b _0 ) $ . Thus $ P ( a _0 ) $ & $ \sim \! P ( b _0 ) $ , whence $ P ( a _0 ) \not \!\Leftrightarrow P ( b _0 ) $ . So $ a _0 \not \equiv _P b _0 $ , whereby $ \sim \! \mathrm {AllEq} _M ( P ) $ .

For $ R : = \equiv _P \ \subseteq M \! \times \! M $ , $ \mathrm {AllEq} _M ( P ) $ and $ \mathrm {Total} _M ( R ) $ have the same definiens:

Béziau’s Corollary. $ \sim \exists P \subseteq M \ \big ( \mathrm {Normal} _M ( P ) \ \& \ \mathrm {Total} _M ( \equiv _P ) \big ) $ .

Notes. We had already shown that $ \mathrm {Real} _M ( P ) $ & $ \mathrm {AllEq} _M ( P ) \Rightarrow P = M $ , where $ {Real} _M ( P ) : \Leftrightarrow \sim \! \mathrm {Empty} _M ( P ) $ (cf. “Similarity and Equality”, The Bulletin of Symbolic Logic 27, 3 (2021), p. 329; “Mathematical theorems on equality and unequality”, ibidem, 28, 2 (2022), pp. 317–318). The Unequality Theorem is part of our Theory of Property Similarity and Property Equality—Related to the Square of Opposition, where $ a \sim _P b : \Leftrightarrow P ( a ) \ \& \ P ( b ) $ . Meanwhile, we have provided a rigorous treatment in terms of formal predicate logic.

▸SOPHIE NAGLER, Inference behaviour semantics for all $^{*}$ connectives in two-dimensional sequent calculi.

Institute for Logic, Language and Computation, University of Amsterdam, Science Park 107, 1098 XG Amsterdam, The Netherlands, and Arché Research Centre, University of St Andrews, 17–19 College St, St Andrews, KY16 9AL, UK.

E-mail: s.e.nagler@uva.nl.

Inference behaviour semantics (IBS), first introduced in [3], is a novel method in proof-theoretic semantics that operationalises and refines recent (sub)structural approaches [4, 2]. IBS identifies the meaning of a connective with its use in sequent calculus proofs, as measured via its minimal inferential behaviour. The inferential behaviour of a connective captures how it is used in each step of a proof, recording whether it occurs in a premiss or conclusion formula, and keeping book of the rule that justifies its use. Inferential behaviour is minimal iff it is measured in Belnap-style proofs of the connective’s definability, viz., conservativity and uniqueness [1], relative to a derivability relation that only includes rules for Identity and Cut.

In this study, we measure the minimal inferential behaviour of all 11,025 operational rule pairs that can be formulated in standard two-dimensional sequent calculi, using at most two premiss sequents and active formulae. This results in 21 fixed points, which correspond to unique connective meanings for bottom, top, the trivial connective, two negations, additive and multiplicative conjunction and disjunction (and their converses), as well as additive and multiplicative implication and reverse-implication (and their inverses).

These findings represent nearly all connectives in commonly used logics, including classical, intuitionistic, dual-intuitionistic, minimal, lattice, relevant and linear logics. This strongly supports IBS’s ability to capture a connective’s meaning independently of the calculus in which it is employed. Moreover, these results shed new light on the semantic interrelations among different logics, as well as between each logic’s meaning-determining (substructural) core and its full calculus.

[1] N. D. Belnap, Tonk, Plonk and Plink. Analysis , vol. 22 (1962), no. 6, pp. 130–134.

[2] B. Dicher, A proof-theoretic defence of meaning-invariant logical pluralism. Mind , vol. 125 (2016), no. 499, pp. 727–757.

[3] S. Nagler, Measuring meaning, submitted, 2025.

[4] G. Restall, Pluralism and proofs. Erkenntnis , vol. 79 (2014), no. 2, pp. 279–291.

▸NICOLÁS NÁJAR-SALINAS, Exploring NIP in Abstract Elementary Classes.

Departamento de Matemáticas, Universidad Nacional de Colombia, Bogotá 111321, Colombia.

E-mail: nicolas.na7ar@gmail.com.

This talk investigates generalizations of dependent theories (also called NIP) to the setting of Abstract Elementary Classes (AECs), based on work by Grossberg, Van Dieren, and Villaveces [1]; Shelah, Villaveces, and Nájar-Salinas [2], and Yang [5]. Drawing on key equivalences from first-order model theory—such as shattering, type counting, and the generic pair conjecture [3, 4]—we adapt these notions to AECs and examine their interplay. A central test question guides this exploration: Are all stable AECs necessarily dependent (NIP)? The results discussed are part of the speaker’s Ph.D. thesis.

[1] R. Grossberg, M. VanDieren, and A. Villaveces, Existence of a model of cardinality $\lambda ^{++}$ , in progress.

[2] N. Nájar-Salinas, S. Shelah, and A. Villaveces, Around non-elementary dependence, in progress.

[3] S. Shelah, Classification Theory: And the Number of Non-Isomorphic Models , Studies in logic, Elsevier, 1990.

[4] S. Shelah, Dependent theories and the generic pair conjecture, Communications in Contemporary Mathematics , vol. 17 (2015), no. 1, p. 1550004.

[5] W. Yang, An NIP-like notion in abstract elementary classes, preprint, 2023, arXiv:2303.04125.

▸MORENIKEJI NERI, Quantitative aspects of stochastic convergence.

Department of Mathematics, Technische Universität Darmstadt, Schlossgartenstraße 7, Darmstadt 64289, Germany.

E-mail: neri@mathematik.tu-darmstadt.de.

In this talk, we discuss logically motivated computational interpretations of almost sure convergence. In the deterministic setting, the direct interpretation one gives to the convergence of a sequence of real numbers $\{x_n\}$ is a rate of convergence, which is a function, $f: \mathbb {Q}^+ \to \mathbb {N}$ , satisfying

An application of Kreisel’s no counter example interpretation [2] to Cauachy convergence gives rise to a different computation interpretation for convergence known as a rate of metastability, a concept studied extensively in both the Analysis and Proof theory literature.

The idea of metastability was first lifted to the probabilistic setting by Avigad, Dean, and Rute [1], where they formulate two notions of metastable stochastic convergence and demonstrate their (bar recursive) computational equivalence. In this talk, we discuss how the metastable notions from [1] connect with existing notions of quantitative stochastic convergence from the Probability theory literature. Furthermore, we present the new notion of stochastic learnability, which form special instances of the metastable notions introduced in [1] and arise naturally in the literature. This talk is based on the joint work with Thomas Powell [3] and formed part of the author’s Ph.D. thesis.

[1] J. Avigad, E. Dean, and J. Rute, A metastable dominated convergence theorem. Journal of Logic and Analysis , vol. 4 (2012), pp. 1–19.

[2] G. Kreisel, On the interpretation of non-finitist proofs, Part I. Journal of Symbolic Logic , vol. 17 (1952), no. 1, pp. 43–58.

[3] M. Neri and T. Powell, On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales, Transactions of the American Mathematical Society , to appear.

▸BRENT ODLAND AND RICHARD ZACH, Fitting-style tableaux for some multi-modal logics with inclusion axioms.

Department of Philosophy, McMaster University, 1280 Main Street W, Hamilton, ON L8S 4L8, Canada.

E-mail: odlandb@mcmaster.ca.

Department of Philosophy, University of Calgary, 2500 University Dr NW, Calgary, AB T2N 1N4, Canada.

E-mail: rzach@ucalgary.ca.

We describe a general method for obtaining Fitting-style signed tableau systems for some propositional multi-modal logics with modalities and interaction axioms of the form . Such axioms correspond to an inclusion of the respective accessibility relations, i.e., $R_j \subseteq R_i$ . Some restrictions on the pairs of included modalities must be placed to obtain completeness, and only modalities for which Fitting-style tableaux have rules (e.g., those given by combinations of the standard axioms T, D, B, $4$ , and $5$ ) can be accommodated. The approach may nevertheless be useful for some applications, as Fitting-style tableaux are generally easier to handle than Nerode-style tableaux in which the syntax includes formulas for the accessibility relation and rules governing these.

▸LEONARDO PACHECO, $\mathsf {IGL}$ via $\omega $ -rules.

Department of Mathematical and Computing Sciences, Institute of Science Tokyo, Tokyo 113-8510, Japan.

E-mail: leonardovpacheco@gmail.com.

URL Address: leonardopacheco.xyz.

$\mathsf {IGL}$ is an intuitionistic version of the provability logic $\mathsf {GL}$ using both box and diamond modalities. It was first studied by Das, van der Giessen, and Marin [2], who provided two ill-founded proof systems and two semantics for this logic. Later, Aguilera and Pacheco [1] defined a cyclic proof system $\mathsf {cm\ell IGL}$ for $\mathsf {IGL}$ ; they also proved that the set of theorems of $\mathsf {IGL}$ is recursively enumerable.

We define a well-founded labeled proof system $\mathsf {\omega m\ell IGL}$ for $\mathsf {IGL}$ characterized by the following $\omega $ -rule:

where x is a label variable. To prove that all valid formulas of $\mathsf {IGL}$ can be proved using the $\omega $ -rule, we use a proof search game argument. To show the soundness of the $\omega $ -rule are valid, we closely analyze the completeness of $\mathsf {cm\ell IGL}$ . Note that an $\omega $ -rule for classical $\mathsf {GL}$ was studied by Tanaka [3].

[1] J. P. Aguilera and L. Pacheco, Intuitionistic Gödel–Löb without sharps, ACM Transactions on Computational Logic , to appear.

[2] A. Das, I. van der Giessen, and S. Marin, Intuitionistic Gödel-Löb logic, à la Simpson: Labelled systems and birelational semantics, EACSL Annual Conference on Computer Science Logic, vol. 288 , Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2024, Article no. 22, 18 pp.

[2] Y. Tanaka, A cut-free proof system for a predicate extension of the logic of provability. Reports on Mathematical Logic , (2018), no. 53, pp. 97–109.

▸FRANCESCO PARENTE, On the Rudin–Frolík ordering of ultrafilters on complete Boolean algebras.

Graduate School of System Informatics, Kobe University, 1-1 Rokkodai-cho, Nada-ku, Kobe 657-8501, Japan.

E-mail: francesco.parente@people.kobe-u.ac.jp.

URL Address: https://www2.kobe-u.ac.jp/˜parente/.

The Rudin–Frolík ordering of ultrafilters over $\omega $ was introduced by Frolík [2], who used it to show that the topological space $\beta \omega \setminus \omega $ is not homogeneous. Two generalizations of the Rudin–Frolík ordering to ultrafilters on complete Boolean algebras have been proposed independently by Balcar and Dow [1] and Murakami [3]. In this talk, we compare the two notions and investigate to what extent they coincide on the class of c.c.c. Boolean algebras.

This talk is based on joint work in progress with Jörg Brendle.

[1] B. Balcar and A. Dow, Dynamical systems on compact extremally disconnected spaces. Topology and its Applications , vol. 41 (1991), no. 1, pp. 41–56.

[2] Z. Frolík, Sums of ultrafilters. Bulletin of the American Mathematical Society , vol. 73 (1967), no. 1, pp. 87–91.

[3] M. Murakami, Standardization principle of nonstandard universes. The Journal of Symbolic Logic , vol. 64 (1999), no. 4, pp. 1645–1655.

▸PHILIPP PROVENZANO, A non-wellfounded system for projective determinacy.

UGent, Krijgslaan 281, 9000 Gent, Belgium.

E-mail: Philipp.Provenzano@UGent.be.

We introduce a non-wellfounded system $\mathrm {G^{<\omega -trees}}$ , based on a non-wellfounded language $\mathcal {L}(\mathrm {G^{<\omega -trees}})$ , and analyze its strength from a reverse mathematical point of view. Concretely, we show that all of consistency, semantic cut-admissibility and soundness, for an appropriate semantic, are equivalent to projective determinacy $\mathrm {PD}$ over the base theory $\mathrm {RCA}_0$ . A related project on the study of non-wellfounded systems based on non-wellfounded languages and their connection to questions of determinacy will be presented at CiE 2025 [2]. Syntactic cut-elimination and a formal translation of $\mathrm {RCA}_0+\mathrm {PD}$ into $\mathrm {G^{<\omega -trees}}$ will be addressed in future research. Together, this will then give some characterization of well-ordering principles provable in $\mathrm {PD}$ .

For the definition of $\mathcal {L}(\mathrm {G^{<\omega -trees}})$ , we introduce a $\mathrm {\Pi }^1_{n+1}$ -complete concept of n-wellfounded n-trees. An $(n+1)$ -tree is a tree T, together with a continuous embedding of an n-tree along each branch of T, with the unique $(-1)$ -tree given by the empty tree. It is $(n+1)$ -wellfounded if every infinite branch B of T can be justified, in the sense that the n-tree embedded along B is not n-wellfounded. This notion is inspired by Girard’s n-ptykes [1].

By labelling the nodes of an $(n+1)$ -tree T with propositional connectives $\vee $ and $\wedge $ , we obtain the notion of a non-wellfounded $(n+1)$ -formula $\varphi $ . A natural semantic is given in the form of an infinite game between two players P and O which cooperatively play a path through $\varphi $ . On $\vee $ -nodes, it is P’s turn to choose a child, and on $\wedge $ -nodes it is O’s turn. An infinite play is won by P if the n-tree embedded along the played path of $\varphi $ is not n-wellfounded. In the special case where all nodes of $\varphi $ are conjunctive, P has a winning strategy for this evaluation game iff the tree underlying $\varphi $ is $(n+1)$ -wellfounded.

We define the theory $\mathrm {G^{<(n+1)-trees}}$ over the language $\mathcal {L}(\mathrm {G^{<(n+1)-trees}})$ consisting of all m-formulas for $m<n+1$ . Pre-proofs are built by obvious inference rules for our non-wellfounded language. The correct proofs P are then selected by a trace condition asserting that for every branch B of P, there is a path through some $(m+1)$ -formula $\varphi $ on B along which the embedded m-tree is not m-wellfounded. Finally, the system $\mathrm {G^{<\omega -trees}}:\equiv \bigcup _{n\in \omega }\mathrm {G^{<n-trees}}$ is defined over the language $\mathcal {L}(\mathrm {G^{<\omega -trees}}):\equiv \bigcup _{n\in \omega }\mathcal {L}(\mathrm {G^{<n-trees}})$ .

This project has been funded by the FWO (Research Foundation—Flanders) under file number 11K7425N.

[1] J.-Y. Girard, Proof-Theory and Logical Complexity, vol. II , 1982, unpublished. https://girard.perso.math.cnrs.fr/Archives4.html.

[2] P. Provenzano, On the reverse mathematics of cut-elimination and determinacy, Crossroads of Computability and Logic: Insights, Inspirations, and Innovations (A. Beckmann, F. Manea, and I. Oitavem, editors), Springer Nature, 2025, pp. 410–424.

▸DIEGO A. ROJAS, Effective vague convergence of locally finite measures on the real line and vague Skorokhod representation.

Department of Mathematics and Statistics, Sam Houston State University, 1900 Avenue I, Huntsville, TX 77340, USA.

E-mail: dar117@shsu.edu.

We expand the effective framework of vague convergence of measures on the real line in [1] to locally finite measures. Furthermore, we discuss an effective version of a Skorokhod representation theorem for vague convergence of subprobability measures on the real line due to Startek [2].

[1] D. A. Rojas, Effective weak and vague convergence of measures on the real line. Archive for Mathematical Logic , vol. 63 (2024), pp. 225–238

[2] M. Startek, Representation theorem for vague convergence in $\mathbb {R}$ . International Journal of Pure and Applied Mathematics , vol. 37 (2007), pp. 239–245

▸CALLIOPE RYAN-SMITH, Local reflections of choice.

School of Mathematics, University of Leeds, Leeds LS2 9JT, UK.

E-mail: cr638@cantab.ac.uk.

URL Address: https://academic.calliope.mx.

Symmetric extensions are a generalisation of forcing that are most commonly used for independence proofs regarding the axiom of choice, originally used by Cohen to show that the axiom of choice is not a theorem of ZF set theory. Given a notion of forcing, one can restrict to a class of sufficiently symmetric names (formalised through the language of permutation groups) to obtain a model of ZF lying between the ground model and the forcing extension.

A result of Blass [1] demonstrates an underlying structure of symmetric extensions called small violations of choice that implies that they are, in a sense, ‘almost’ models of the well-ordering principle. SVC states that there is a set S such that for all X there is an ordinal $\eta $ such that $S\times \eta $ surjects onto X. Hence, every set is well-orderable up to a ‘factor’ of S. Under this assumption the truth of ‘global’ consequences of the axiom of choice (such as countable choice: every countable family has a choice function) are equivalent to ‘local’ statements about S (e.g., countable choice is equivalent to countable choice for families of subsets of S). We call this phenomenon local reflections of choice [2], and this allows for an easier analysis of the consequences of choice that have been preserved, or violated, in a symmetric extension. We shall introduce symmetric extensions and investigate local reflections of various consequences of the axiom of choice, leading to some surprising consequences for S itself.

[1] A. Blass, Injectivity, projectivity, and the axiom of choice. Transactions of the American Mathematical Society , vol. 255 (1979), pp. 31–59.

[2] C. Ryan-Smith, Local reflections of choice. Acta Mathematica Hungarica , to appear.

▸TAPIO SAARINEN, On second-order spectra.

Department of Mathematics and Statistics, University of Helsinki, Helsinki 00100, Finland.

E-mail: tapio.saarinen@helsinki.fi.

The spectrum of a sentence of some logic is the set or class of cardinalities of the models of the sentence (in symbols, $\mathop {Spec}(\phi ) = \lbrace \left |\mathcal M \right | : \mathcal M \models \phi \rbrace $ ). Due to the upward and downward Löwenheim–Skolem theorems, the spectrum of a first-order sentence is nontrivial only in the finite part. More complicated logics, such as the infinitary logics $L_{\kappa \kappa }$ or logics with generalized quantifiers, have more complicated spectra, but usually the collection of spectra still has some regularity properties. However, the spectra of second-order logic seem to eschew structure: for example, for any subset $x \subseteq \omega $ , $\lbrace \aleph _n : n \in x \rbrace $ can be forced to become a second-order spectrum. Also, unusually, the collection of second-order spectra is closed under complementation.

Related are also the characteristic numbers of a logic, such as the Hanf and Löwenheim numbers (these are the supremum of all bounded spectra, and the supremum of the minima of each spectrum, respectively). Then the Löwenheim number of second-order logic lies between the first measurable and first supercompact cardinal, and the Hanf number of second-order logic lies between the first supercompact and first extendible cardinal (assuming said cardinals exist).

In this talk we present some closure properties of second-order spectra, and of the spectra of related logics such as the $\Delta $ -extension of second-order logic, and infinitary second-order logics. We also discuss how the Löwenheim numbers of various infinitary second-order logics $L^2_{\kappa \omega }$ relate to each other. For example, for every $L^2_{\omega _1 \omega }$ -sentence there is a second-order theory in a slightly expanded vocabulary such that an uncountable structure models the sentence if and only if it can be expanded into a model of the theory.

▸YUTA SATO AND TAISHI KURAHASHI, Analysis of the pure logic of necessitation and its extensions.

Graduate School of System Informatics, Kobe University, 1-1 Rokkodai, Nada, Kobe 657-8501, Japan.

E-mail: 231x032x@gsuite.kobe-u.ac.jp, kurahashi@people.kobe-u.ac.jp.

In this talk, we first introduce the pure logic of necessitation $\mathbf {N}$ . Originally introduced by Fitting, Marek, and Truszczyński [1], $\mathbf {N}$ is a nonnormal modal logic obtained by removing the $\mathrm {K}$ axiom from the modal logic $\mathbf {K}$ . Despite its trivial construction from normal modal logics and yet having interesting property and potential application, $\mathbf {N}$ and its extensions are left uninvestigated until very recently [2, 4].

For any natural numbers $m, n$ , we then introduce a logic $\mathbf {N}^+\mathbf {A}_{m,n}$ obtained by adding a modal reduction principle $\Box ^n \varphi \to \Box ^m \varphi $ and a rule : $\frac {\neg \Box \varphi }{\neg \Box \Box \varphi }$ to $\mathbf {N}$ . Here, the rule is admissible in every normal modal logic, thus $\mathbf {N}^+\mathbf {A}_{m,n} \subseteq \mathbf {K} + \Box ^n \varphi \to \Box ^m \varphi $ . We will talk about intriguing differences of $\mathbf {N}^+\mathbf {A}_{m,n}$ from $\mathbf {K} + \Box ^n \varphi \to \Box ^m \varphi $ by analyzing the finite frame property and Uniform Lyndon interpolation property of it.

This talk is based on [3, 5].

[1] M. C. Fitting, V. Wiktor Marek, and M. Truszczyński, The pure logic of necessitation. Journal of Logic and Computation , vol. 2 (1992), no. 3, pp. 349–373.

[2] T. Kurahashi, The provability logic of all provability predicates. Journal of Logic and Computation , vol. 34 (2024), no. 6, pp. 1108–1135.

[3] T. Kurahashi and Y. Sato, The finite frame property of some extensions of the pure logic of necessitation, Studia Logica , to appear.

[4] H. Omori and D. Skurt, On Ivlev’s semantics for modality, Many-valued Semantics and Modal Logics: Essays in Honour of Yuriy Vasilievich Ivlev, vol. 485 , Springer International Publishing, Cham, 2024, pp. 243-275.

[5] Y. Sato, Uniform Lyndon interpolation for the pure logic of necessitation with a modal reduction principle, Journal of Logic and Computation , to appear.

▸SEBASTIAN G. W. SPEITEL AND S. KAAN TABAKÇI, Some considerations on the notion of Belnapian uniqueness.

Institute of Philosophy, University of Bonn, Bonn 53113, Germany.

E-mail: sgwspeitel@uni-bonn.de.

Department of Philosophy, Koç University, Istanbul 34450, Türkiye.

E-mail: stabakci@ku.edu.tr.

In his influential response to Prior’s trivializing connective tonk [3], Belnap [1] outlined and developed two conditions that inferential specifications of the meaning of logical notions had to meet: conservativity and uniqueness. These conditions were to ensure existence and unambiguous specification, establishing benchmarks for successful definition.

According to Belnap, a sufficient condition for a notion to be uniquely specified in this sense was its interderivability with any other notion characterized in the precise same manner. Concretely, where $\alpha $ is an n-ary connective and $\beta $ is a connective obeying the same rules as $\alpha $ , $\alpha $ is unique iff, for all $\psi _{1}, \ldots , \psi _{n}$ :

Underlying Belnap’s condition (U) is an inferentialist conception of meaning: identifying meanings with inferential roles ensures that condition (U) constitutes a sufficient criterion for uniqueness of meaning, for (U) guarantees that $\alpha $ ’s inferential behaviour is so tightly circumscribed that there is but a single inferential role consistent with it.

Of course, changing the underlying conception of meaning might thereby also call into question the adequacy of (U) in ensuring unique determination of meaning. In particular, when meanings become model-theoretic (U) (or its model-theoretic analogue (U $^{*}$ ) $\alpha (\psi _{1}, \ldots , \psi _{n}) {=}\,\mathrel {|} \models \beta (\psi _{1}, \ldots , \psi _{n})$ ) might no longer prove sufficient for guaranteeing that there is but a unique model-theoretic value validating the characterizing inferential patterns of $\alpha $ , over and above ensuring synonymy of inferentially characterized meanings in any given situation.

The goal of this talk is twofold. On the one hand, we argue that the ‘right’ model-theoretic analogue of Belnap’s notion of uniqueness is a notion of implicit definability by inferences. Second, we consider several situations in which (U $^{*}$ ) might be successful in ensuring uniqueness of model-theoretic meaning. To do so we take up two suggestions of [2] and show that the contexts in which mutual entailment (U $^{*}$ ) suffices to yield uniqueness of meaning are much more restricted than they were when meanings were identified with inferential roles. The overall aim is to further clarify the nature and motivation of Belnap’s influential uniqueness requirement on successful inferential definition, and its model-theoretic import.

[1] N. Belnap, Tonk, Plonk and Plink. Analysis , vol. 22 (1962), no. 6, pp. 130–134.

[2] K. Došen and P. Schroeder-Heister, Conservativeness and uniqueness. Theoria , vol. 51 (1985), no. 3, pp. 159–173.

[3] A.N. Prior, The Runabout Inference-Ticket. Analysis , vol. 21 (1960), no. 2, pp. 38–39.

▸CESARE STRAFFELINI, Higher Solovay models.

Dipartimento di Matematica, Università di Trento, Via Sommarive 14, 38123 Trento, Italy.

E-mail: straffelini@ub.edu.

In 1970, Solovay wrote a fundamental article, [3], where from a model of ZFC with an inaccessible cardinal he built, by Lévy collapsing the inaccessible to $\omega _1$ and considering the inner model $L(\mathbb R)$ of this extension, a model where all sets of reals are Lebesgue measurable and have the Baire and perfect set properties. In [1], an abstract axiomatisation of this model was introduced, and it was proved that every model satisfying this axiomatisation is the same as a model built with the original Solovay construction.

In recent years, a prolific subject is generalised descriptive set theory, that tries to generalise results about $L(\mathbb R)$ to any model of the form $L(V_{\kappa +1})$ . This is the case also of the article [2], where the authors mimic the Solovay construction. Instead of Lévy collapse, they use some kind of $\Sigma $ -Příkrý forcing, and consider the inner model $L(V_{\kappa +1})$ of this forcing extension, for $\kappa $ a singular cardinal. Here, all sets of “ $\kappa $ -reals” satisfy adapted versions of the Baire and perfect set properties.

The goal of my talk is to introduce an axiomatisation of these higher Solovay models $L(V_{\kappa +1})^M$ , and then show the corresponding version of Bagaria–Woodin’s theorem and prove some generic absoluteness results about these kinds of models.

Joint work with Sebastiano Thei (Udine).

[1] J. Bagaria and H. Woodin, $\Delta ^1_{n}$ sets of reals. Journal of Symbolic Logic , vol. 62 (1997), no. 4, pp. 1379–1428

[2] V. Dimonte, A. Poveda, and S. Thei, The Baire and perfect set properties at singulars cardinals, preprint, 2024, arXiv:2408.05973.

[3] R. Solovay, A model of set-theory in which every set of reals is Lebesgue measurable. Annals of Mathematics. Second Series , vol. 92 (1970), pp. 1–56.

▸ANDREAS WEIERMANN, How to treat Goodstein sequences via well partial orders.

Department of Mathematics WE16, Ghent University, Krijgslaan 281, Building S8, 9000 Ghent, Belgium.

E-mail: Andreas.Weiermann@UGent.be.

We introduce an abstract framework for treating Goodstein principles [1] via well partially ordered direct limits [2]. Besides termination this approach also yields upper bounds on the proof-theoretic complexity of the underlying processes. This explains, for example, why Goodstein sequences based on the Ackermann function [4] are not more powerful than Goodstein sequences based on hereditary exponential normal forms [3].

[1] R. L. Goodstein. On the restricted ordinal theorem. The Journal of Symbolic Logic vol. 9 (1944), pp. 33–41.

[2] D. H. J. Jongh and R. Parikh, Well-partial orderings and hierarchies. Indagationes Mathematicae Nederlandse Akademie van de Wetenschappen, Proc. Ser. A 80 , vol. 39 (1977), no. 3, pp. 195–207.

[3] L. Kirby and J. Paris, Accessible independence results for Peano arithmetic. Bulletin of the London Mathematical Society . vol. 14 (1982), no. 4, pp. 285–293.

[4] A. Weiermann, Ackermannian Goodstein principles for first order Peano arithmetic. Sets and Computations (S. D. Friedman, D. Raghavan, and Y. Yang, editors), Lecture Notes Series. Institute of Mathematical Sciences. National University of Singapore, 33, World Scientific Publishing Co. Pte. Ltd., 2018, pp. 157–181.

▸AIBAT YESHKEYEV AND INDIRA TUNGUSHBAYEVA, The properties of the Kaiser class for a normal Jonsson theory.

Department of Algebra, Mathematical Logic and Geometry named after Prof. T.G. Mustafin, Karaganda Buketov University, 28 Universitetskaya st., Karaganda 100028, Kazakhstan.

E-mail: aibat.kz@gmail.com.

E-mail: intng@mail.ru.

We study Jonsson theories in the framework of a countable first-order language L. In this work, we use a new tool for analyzing Jonsson theories [1]: a specific semantic invariant of a Jonsson theory T—the Kaiser class of T. We give some results concerning the axiomatizability of the Kaiser class and apply this notion to investigate normal Jonsson theories.

Let T be a Jonsson theory. A class $K_T$ of L-structures is called a Kaiser class of T if

Let $T_1$ and $T_2$ be Jonsson L-theories. $T_1$ and $T_2$ are called $K_T$ -equivalent ( $T_1 \overset {\sim }{\bowtie } T_2$ ), if $K_{T_1} = K_{T_2}$ . It is easy to see that $K_T$ equivalence is an equivalence relation.

Let K be a class of L-structures, then by $JSp(K)_{\overset {\sim }{\bowtie }}$ , we denote the factor set of the Jonsson spectrum of K by $K_T$ -equivalence.

Let K be a class of L-structures. A Robinson spectrum $RSp(K)$ of K [2] is the following set of theories:

A Jonsson theory T is called normal, if, for any model $M \in K_T$ , $C_{M^0}$ is an existentially closed submodel of $C_T$ , where $M^0 = Th_{\forall \exists }(M)$ .

[1] J. Barwise, Handbook of Mathematical Logic, Part 1: Model Theory , Izdatel’stvo Nauka, Moscow, 1982.

[2] A. R. Yeshkeyev and O. I. Ulbrikht, JSp-cosemanticness of R-modules. Siberian Electronic Mathematical Reports , vol. 19 (2019), pp. 1233–1244.

Abstracts of talks presented by title

▸AIZHAN ALTAYEVA, BEIBUT KULPESHOV, AND SERGEY SUDOPLATOV, On non-essential expansions of weakly o-minimal theories of finite convexity rank.

International Information Technology University, Almaty 050000, Kazakhstan.

E-mail: vip.altayeva@mail.ru

Institute of Mathematics and Mathematical Modeling, Kazakh-British Technical University, Almaty 050000, Kazakhstan.

E-mail: b.kulpeshov@kbtu.kz.

Sobolev Institute of Mathematics, Novosibirsk State Technical University, Novosibirsk 630087, Russia.

E-mail: sudoplat@math.nsc.ru.

The present lecture concerns the notion of weak o-minimality originally studied by H. D. Macpherson, D. Marker, and C. Steinhorn in [4]. The notion of almost quite orthogonality of 1-types was introduced in [1, 2].

This research has been funded by the Science Committee of Ministry of Science and Higher Education of the Republic of Kazakhstan (AP22685890 and AP19674850), and in the framework of the State Contract of the Sobolev Institute of Mathematics, Project No. FWNF-2022-0012.

[1] B. Sh. Kulpeshov and S. V. Sudoplatov, Almost quite orthogonality of 1-types in weakly o-minimal theories, Logic Colloquium 2023, European Summer Meeting of ASL , University of Milan, Italy, 2023, book of abstracts, p. 128.

[2] B. Sh. Kulpeshov and S. V. Sudoplatov, On new variant of orthogonality of 1-types in weakly o-minimal theories. Algebra and Logic , vol. 63, no. 4 (2024), pp. 270–283.

[3] H. D. Macpherson, D. Marker, and C. Steinhorn,Weakly o-minimal structures and real closed fields. Transactions of the American Mathematical Society , vol. 352 (2000), no. 12, pp. 5435–5483.

▸SANKHA S. BASU, MIHIR K. CHAKRABORTY, AND SAYANTAN ROY, Abstract model structures and the compactness theorem.

Department of Mathematics, Indraprastha Institute of Information Technology, New Delhi 110020, India.

E-mail: sankha@iiitd.ac.in.

School of Cognitive Science, Jadavpur University, Kolkata 700032, India.

E-mail: mihirc4@gmail.com.

Department of Mathematics, Indraprastha Institute of Information Technology, New Delhi 110020, India.

E-mail: sayantanr@iiitd.ac.in.

The compactness theorem for a logic states, roughly, that the satisfiability of a set of wffs can be determined from the satisfiability of its finite subsets, and vice versa. Usually, proofs of this theorem depend on the syntactic/semantic particularities of the corresponding logic (see, e.g., [2]). In this article, using the notion of abstract model structures, we investigate a generalized notion of compactness that is independent of these. Thus, in terms of spirit, this work belongs to the subject known as asbtract model theory (see, e.g., [1] for details) although methodologically, it goes beyond it (e.g., we do not maintain the same commitment to the conventional concrete systems of logic that are characteristic features of works in this area). We also differ from a more categorical take to the subject (see, e.g., [3]) since our approach is purely set-theoretic. We, however, do not compromise with the level of generality, and obtain several characterization theorems for a particular class of compact abstract model structures, generalizing the traditional Henkin-style, topological and ultrproduct proofs respectively. Finally, some directions for future research are discussed as well.

[1] J. Barwise Axioms for abstract model theory. Annals of Mathematical Logic , vol. 7 (1974), pp. 221–265.

[2] C. C. Chang and H. J. Keisler, Model Theory , Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1990.

[3] Ră. Diaconescu, Institution-Independent Model Theory , Studies in Universal Logic, Birkhäuser, 2008.

▸MAHSUT BEKENOV, NURLAN MARKHABATOV, AND ANVAR NURAKUNOV, Note on idempotent complete theories.

L. N. Gumilyov Eurasian National University, 13 Kazhymukan St., 010008 Astana, Kazakhstan.

E-mail: makhsut.bekenov@gmail.com.

E-mail: markhabatov@gmail.com

Institute of Mathematics, NAS KR, pr. Chu 265a, 720071 Bishkek, Kyrgyzstan.

E-mail: a.nurakunov@gmail.com.

On the set of all first-order complete theories $\text {Th}(L)$ of a language L we define a binary operation $\{\cdot \}$ by the rule: $T\cdot S= \text {Th}(A\times B)$ , for any complete theories $T=\text {Th}(A)$ and $S=\text {Th}(B)$ . This operation is well defined by the Feferman–Vaught theorem [3], meaning that the operation does not depend on the choice of the structures A and B. A complete theory T is idempotent if $T=T\cdot T$ . We say that a complete theory T absorbs a theory S if $T=T\cdot S$ . Some properties of idempotent and absorbing theories can be found in [2, 1].

In this talk, we present and discuss new results related to idempotent and absorbing theories.

A theory T is pseudo-finite if for any sentence $\varphi \in T$ , there is a finite structure A such that $A\models \varphi $ .

A first-order formula $\varphi (x,y)$ is preserved under the direct power of structure A if: $A\models \varphi (a,b) \iff A\times A\models \varphi ((a,x),(b,x))\wedge \varphi ((x,a),(x,b))$ , for all $a,b\in A$ and $x\in \{a,b\}$ .

Some examples of groupoids and graphs are provided. The research was supported by the Science Committee of the MSHE RK (AP23485395).

[1] M. Bekenov, A. Kassatova, and A. Nurakunov, On absorption’s formula definable semigroups of complete theories. Archive for Mathematical Logic , vol. 64 (2025), pp. 107–116.

[2] Bekenov, M. I., Nurakunov, A. M. A semigroup of theories and its lattice of idempotent elements. Algebra and Logic , vol. 60 (2021), pp. 1–14.

[3] S. Feferman and R. Vaught, The first order properties of algebraic systems. Fundamenta Mathematicae , vol. 47 (1959), pp. 57–103.

▸LONGYUN DING, On equivalence relations induced by Polish groups.

School of Mathematical Sciences, Nankai University, Tianjin 300071, China.

E-mail: dinglongyun@gmail.com.

In this talk, we recall Borel reducibility among equivalence relations first. Then we introduce equivalence relations $E(G)$ induced by Polish groups G. Main part of this talk is to present many rigid results concerning various kinds of Polish groups: non-archimedean, TSI, CLI, $\alpha $ -l.m.-unbalanced, abelian, locally compact, Lie groups, and Banach spaces (as additive groups) and so on.

This is joint work with Yang Zheng.

▸BEIBUT KULPESHOV, On algebras of binary formulas and the number of countable models.

Institute of Mathematics and Mathematical Modeling, Kazakh-British Technical University, Almaty 050000, Kazakhstan.

E-mail: b.kulpeshov@kbtu.kz.

The present lecture concerns the notion of weak o-minimality originally studied by H. D. Macpherson, D. Marker, and C. Steinhorn in [4]. A weakly o-minimal structure is a linearly ordered structure $M=\langle M,=,<,\dots \rangle $ such that any definable (with parameters) subset of M is a finite union of convex sets in M.

Algebras of binary formulas are a tool for describing relationships between elements of the sets of realizations of an one-type at the binary level with respect to the superposition of binary definable sets. A binary isolating formula is a formula of the form $\varphi (x,y)$ such that for some parameter a the formula $\varphi (a,y)$ isolates a complete type in $S(\{a\})$ . In recent years, algebras of binary formulas for weakly o-minimal theories have been studied in [2, 3, 1].

This research has been funded by the Science Committee of Ministry of Science and Higher Education of the Republic of Kazakhstan (AP19674850 and BR20281002).

[1] A. B. Altayeva, B. Sh. Kulpeshov, and S. V. Sudoplatov, Algebras of distributions of binary isolating formulas for almost $\omega $ -categorical weakly o-minimal theories. Algebra and Logic , vol. 60 (2021), no. 4, pp. 241–262.

[2] D. Yu. Emelyanov, B. Sh. Kulpeshov, and S. V. Sudoplatov, Algebras of distributions for binary formulas in countably categorical weakly o-minimal structures. Algebra and Logic , vol. 56 (2017), no. 1, pp. 13–36.

[3] D. Yu. Emelyanov, B. Sh. Kulpeshov, and S. V. Sudoplatov, On algebras of distributions for binary formulas for quite o-minimal theories. Algebra and Logic , vol. 57 (2019), no. 6, pp. 429–444.

[4] H. D. Macpherson, D. Marker, and C. Steinhorn,Weakly o-minimal structures and real closed fields. Transactions of the American Mathematical Society , vol. 352 (2000), no. 12, pp. 5435–5483.