The theory of definable equivalence relations in Polish spaces has been a very active area of research in descriptive set theory for several decades now. It serves as a foundation of a theory of complexity of classification problems in mathematics. Another source of motivation comes from the study of group actions in a descriptive, topological or measure theoretic context, where one analyzes the structure of the equivalence relation induced by the orbits of the action and the corresponding orbit space. In these talks I will concentrate on the subject of countable Borel equivalence relations, which are those induced by Borel actions of countable (discrete) groups and has important connections with other areas of mathematics such as group theory, dynamical systems, combinatorics, probability theory, and operator algebras.

Stability in model theory, as developed in Shelah’s classification theory in the seventies, is a certain measure of complexity of theories: roughly speaking, models have few limit points (types). This tutorial will discuss a few of the many recent interactions of stability with ideas across mathematics.

We examine metrizability criteria for ideals of subsets of some countable index-set. This will be done both from the combinatorial and descriptive angle.

The classical notion of algebras in the context of k-vector spaces or R-modules generalize in a natural way to a suitable notion of ‘monad’ in a higher-dimensional categorical structure, that of a double category D. Starting from the base case of a category equipped with a monoidal structure, we will discuss monoids and their dual notion of comonoids therein, and we will extend a folklore result that enriches the space of algebra maps with a comultiplication (using the so-called Sweedler’s ‘universal measuring coalgebras’) to the double categorical context. Such a process opens paths for further applications involving operads and other related structures, within a general framework that may be called ’enriched duality’.

A class K of finite structures is said to have the Ramsey Property (RP) if it satisfies a natural generalization of the classical finite Ramsey theorem. RP can be easily phrased as a property of the category of structures in K and embeddings between them, so it makes sense for any category C. Under mild hypotheses on C, I will show that C has RP if and only if every presheaf P on C admits a “global ultrafilter”: an ultrafilter U(A) on the set P(A) for each object A in C, such that the action of each morphism from A to B pushes forward U(B) to U(A). An equivalent formulation is that every contravariant functor from C to the category of compact Hausdorff spaces has a global element (a kind of fixed-point). As an application, we obtain a new proof of the celebrated Kechris-Pestov-Todorčević theorem characterizing extreme amenability of automorphism groups of countable structures in terms of RP. All notions from Ramsey theory and category theory will be explained in the talk.

Extreme amenability is a remarkable property for a topological group to have. Ever since the first example of such groups was constructed in 1975, many groups have been shown to be extremely amenable. In this talk I will address the question: How many pairwise non-isomorphic extremely amenable groups are there? We consider the isomorphism relation of extremely amenable Polish groups from the point of view of descriptive set theory and show that countable graph isomorphism is Borel reducible to the isomorphism relation of extremely amenable closed subgroups of $S_\infty$. We also discuss the related property of concentration of measures for some related groups.

In economics, there is some interest in different notions of equitable social welfare orders. Their existence sometimes is linked to the Axiom of Choice, but how much choice do we need to construct these objects? We show that for any Borel funicular preorder, it is consistent that there is a prelinearization of it while there are no free ultrafilters on the natural numbers. This is joint work with Luke Serafin.

Given a collection of mathematical objects and a natural notion of equivalence (such as isomorphism), we want to find a complete classification, that is, an assignment of a ‘classifying invariant’ to each object, so that two objects are equivalent if and only if they are assigned the same classifying invariant. In this talk we discuss methods of proving anti-classification results, that is, when a complete classification is not possible using certain classifying invariants.

The problem of using real numbers as classifying invariants is well understood. In this case, the obstruction to classifiability is ergodicity. We consider classifiability by higher rank objects, such as countable sets of real numbers, and present a simple ergodicity-like obstruction for classifiability. This method is particularly useful when applied in various models of ZF where even weak fragments of the axiom of choice fails.

The CSP Dichotomy Theorem states that for every finite relational structure D, the problem of deciding whether there is a homomorphism from a structure E to D is solvable in polynomial time or NP-complete, with no intermediate cases. This result is fundamental because it gives a complete complexity classification of a vast class of problems and reveals that tractability is governed by algebraic structure, namely so called polymorphisms. I will talk about how these algebraic properties relate to compactness principles over ZF. In particular, the existence of cyclic polymorphisms characterize the easy case, and we show that this boundary exactly matches the strength of the corresponding compactness statements over ZF. Surprisingly, this theorem does not use the CSP Dichotomy. I will also discuss recent results of Bodor and Tardiff, connecting compactness principles to promise CSPs, for which the finitary dichotomy is wide open.

This talk gives a concise introduction to the area of team semantics. I begin with the basic ideas of team semantics in the first-order setting, where formulas are evaluated over sets of assignments rather than single assignments. This shift in perspective makes it possible to naturally express notions of dependence, independence, and other relational properties between variables. Building on this foundation, I then introduce temporal extensions of team semantics, focusing in particular on the temporal team logic TeamLTL and some of its variants. These logics allow reasoning about sets of traces and provide a natural framework for expressing hyperproperties that arise in the verification of systems. Finally, I discuss connections between team-based logics and separation logic. The aim of the talk is to illustrate how team semantics provides a flexible and general logical perspective that is relevant to the study of logics used in formal verification.

HyperLTL, a temporal logic expressing properties of sets of execution traces of a computational system (so-called hyperproperties) with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical model-checking algorithm for full HyperLTL is automata-theoretic, more recently, a game-based alternative for the $\forall ^* \exists ^*$-fragment has been presented.

Here, we employ imperfect information-games to extend the game-based approach to full HyperLTL, i.e., to arbitrary quantifier prefixes. As a byproduct of our game-based algorithm, we obtain finite-state implementations of Skolem functions via transducers with lookahead that explain satisfaction or violation of HyperLTL properties.

Based on joint work with Sarah Winter (IRIF).

Equational logic is the logical framework studying which equations are sound and provable, and which axiom sets are complete over a given model and for a given definition of equality. Within the field of mathematics there are plenty of definitions of such theories, from the ones developed via the point of view of universal algebra, to the category theory interpretation. When one defines the models as programs and the equality predicate as a type of program equivalence, the techniques of equational logic can be applied to provide algorithms, proof techniques, and results identifying which programs behave in the same way, a question which is at the core of one of the most common formal verification techniques in existence. In this talk we will first look into the basic definition of equational logic and briefly study its connection to universal algebra. We will then move to describing one of the types of programs that equational logic is used often with, the type(s) of equality used in this setting and finish with a overview of axioms, results, and techniques that have emerged within this setting.

There is an emerging consensus about the correct modal logic of plurals. The key idea is that every plurality is modally rigid: in essence, that some things comprise the very same things at every world at which they exist. I explain and defend this consensus. Furthermore, as has been known since Gödel, there is a close connection between intuitionistic and modal logic. By combining these two insights, I present and defend an intuitionistic plural logic. I end by explaining the broader philosophical significance of this logic.

Epistemic logic is an umbrella term for a variety of logics whose main objects of study are knowledge, belief, and related notions such as evidence and justification. As a field of study, epistemic logic uses logical and mathematical tools to formalize, clarify, and address the questions that drive (formal) epistemology, and its applications extend not only to philosophy but also to theoretical computer science, artificial intelligence, and economics. While any logic with an epistemic interpretation can be called an epistemic logic, research in epistemic logic has advanced significantly on the basis of (normal) modal logics and standard possible-worlds semantics on relational structures, as these provide a relatively straightforward way of modeling knowledge and belief. However, this mainstream approach is subject to well-known conceptual objections and invites extensions to better capture the dynamics and structure of epistemic states. These challenges and avenues for refinement have given rise to a rich and rapidly evolving literature, fostering a wide range of alternative frameworks and significant developments in the field (see, e.g., [3]).

In this talk, I will focus on features of standard relational possible-worlds semantics for modal epistemic logics that call for refinement or enrichment, and I will provide an overview of topological approaches to epistemic logic. In particular, I will argue that topological spaces emerge naturally as information structures if one not only seeks an easy way of modeling knowledge and belief, but also aims at representing evidence and its relationship to these notions. Based on some of the topological semantics proposed in [1, 2], I will show that the topological approach enables fine-grained and more refined representations of the aforementioned epistemic notions, highlighting several variations and extensions in the literature, as well as—time permitting—applications in mathematical logic, formal epistemology, and formal learning theory.

References

[1] Baltag, A., Bezhanishvili, N., Özgün, A., and Smets, S. (2022) Justified belief, knowledge, and the topology of evidence. Synthese, 200, 1–51.

[2] Özgün, A. (2017) Evidence in Epistemic Logic: A Topological Perspective. Ph.D. thesis, ILLC, University of Amsterdam.

[3] van Ditmarsch, H., Halpern, J., van der Hoek, W., and Kooi, B. (2015) Handbook of Epistemic Logic. College Publications.

In a seminal result Solovay showed that the normal modal operator logic GL is the logic of the provability predicate of PA in PA, that is, the modal operator of GL has precisely the modal properties of the provability predicate of PA in PA. This is known as Solovay’s arithmetical completeness result for GL. By inspecting the result, one realizes that it is possible to investigate the modal logics of other sentential predicates along the lines of Solovay’s result. For example, one can investigate the modal logics of different non-naive, theories of self-applicable truth and thereby determine the precise modal properties of the truth predicate of these theories. A truth predicate is self-applicable if it can apply to sentences in which the truth predicate occurs itself. In this talk we present Solovay-style results for two different families of theories of self-applicable truth and discuss how these results bear on the philosophical discussion about truth.

Theophrastus, Aristotle’s pupil and eventual successor as head of the Peripatos, developed a theory of hypothetical syllogisms in which he sought to reduce various modes of propositional reasoning to categorical syllogisms. Jonathan Barnes has argued that Theophrastus’ attempted reduction of propositional to categorical logic is incoherent and “doomed to failure”. Others have gone still further, denying that Theophrastus’ hypothetical syllogistic constitutes any sort of contribution to the study of propositional logic at all. The present paper offers, in place of such negative assessments, an alternative view of what we shall argue are, in fact, significant and noteworthy achievements on Theophrastus’ part in the field of propositional logic. We reconstruct Theophrastus’ calculus and show that it gives rise to a coherent and natural system of propositional logic (namely, first-degree intensional linear logic). This system captures exactly the early Peripatetic theories of wholly and mixed hypothetical syllogisms. Theophrastus’ calculus also underwrites Aristotle’s rule of reductio ad impossibile and his commitment to the connexive law that no proposition entails its own negation. This is joint work with Anubav Vasudevan (University of Chicago).

The mechanism known as Pons Asinorum, in the context of the Aristotelian syllogistic, is an algorithmic machine that operates upon premisses codified in inventories, in search of a deduction that establishes a given target conclusion. More specifically, each categorical term that appears in a premiss is assigned three inventories. One containing terms universally predicated of it, one containing terms of which it is universally predicated, one containing terms universally negated of it. Given a target conclusion C, if the procedure terminates then it outputs a sound (assuming the premisses codified in the inventories are true) argument for C. The fact that only inventories pertaining to universal forms of affirmative or negative predication are to be employed has traditionally be thought of as puzzling. Here, we will formally prove that the three lists employed per term by the machine are indeed sufficient, in the sense that, if certain well posed conditions are fulfilled by the corresponding set of premisses, then there is no need to also employ additional lists for particular propositions. Furthermore, based on the observation that the inventories of a Pons machine can be understood as the adjacency list of a directed labeled graph, we implement in ASP (Answer Set Programming) a Pons Asinorum machine, formalized as a transition system in the style of the action language AL, that treats the search for deductions as a graph pathfinding problem, and use it to mechanically demonstrate the formal result. We conclude with some remarks regarding how this computational conclusion supports the ontological and epistemological thesis that, if something can be proved by the syllogistic, its proof emanates from the truth of some unprovable propositions, which, crucially, are all general.

In a passage of the Prior analytics called the pons asinorum (APr I 27-31), Aristotle proposes a spatial method for building syllogisms out of databases for a given problem. This produces a spatialized semantics. Aristotle manipulates the lists of data embedded in this semantic spatial structure in order to produce syllogistic diagrams. This passage of the Prior analytics sheds a new light on the way Aristotle conceived of formal logic, putting an emphasis on visual thinking, diagrams, and the organization and manipulation of databases.