Following Lawvere, a classical first-order theory can be represented as a functor from finite sets to Boolean algebras. Dually, the type space functor goes from finite sets to Stone spaces. If the theory is moreover a theory of graphs, ordered sets, monoids, or other kinds of structures, then the category of finite sets can be replaced by the category of finitely presented such structures. Type space functors can often be translated from one context to another via a left Kan extension, for instance along the forgetful functor from finite posets to finite sets. I will present an attempt at a theory of such "translations".

We introduce the notion of the relative Stone-Čech compactification, which is a generalisation of the Stone-Čech compactification.
We show that the relative Stone-Čech compactification is left adjoint to the inclusion functor of the category of proper Hausdorff G0-spaces into the category of G0-spaces, for a locally compact étale groupoid G.
We establish that a groupoid correspondence which acts on a space also acts on the relative Stone-Čech compactification of the space.
The main result shows the existence of a groupoid model for a diagram of proper locally compact groupoid correspondences and shows that it is again a locally compact étale groupoid, i.e., the universal action occurs on a space that is locally compact Hausdorff and proper over G0.

We give a detailed account of one of the most active areas in current Set Theory, namely Set-Theoretic Geology, which consists on the study of the ground models of a given set-theoretic universe.
We begin with a brief introduction to the forcing technique, based on the existing literature.
We continue by introducing the Ground Axiom (GA) and the Ground Model Definability Theorem of Laver and Woodin. By minimality it is easy to show that GA holds in L.
More interestingly, there is a class forcing notion P such that P forces GA.
Thus, we provide a framework for performing class forcing in the context of Morse-Kelly (MK).
Once the tools of class forcing are in place it is now the turn to prove the consistency of the negation of the Bedrock Axiom (BA). Another key result in class forcing and set-theoretic geology is that any model can be the mantle (i.e., the intersection of all grounds) of another model.
Then, we discuss about pseudo-grounds, namely models that have certain cover and approximation properties. In particular, we consider some generalizations of previous results to the context of class forcing and pseudo-grounds, e.g., the class ground model definability theorem.
Adopting the same strategy, we end with a proof of the consistency of the Ground Axiom together with the negation of the pseudo-GA.

Joint work with with Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson, FRS, Cambridge.
This talk is about an application in set theory of what is sometimes called 'automated theorem proving' by mathematicians. This actually refers to several different things, including what computer scientists call formalisation.
After briefly discussing general aspects of formalisation, we shall give an overview of a formalisation project in the proof assistant Isabelle/HOL of a number of results in ordinal partition relations : theorems by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Jean Larson’s proof of the unpublished result by E.C. Milner asserting that for all $m\in \mathbb N $, $\omega^{\omega }\rightarrow (\omega^{\omega },m)$.
Ordinal partition relations are notoriously hard to study by classical methods and have the uncanny feature to be mostly interesting for countable ordinals, where modern set theory seems to be quite silent.
Our approach has been to see if formalising might bring us closer to resolving some of the many unsolved problems in the area. The talk will focus on the process of formalisation, the difficulties and the hopes of the process. In particular, no new proof has yet been obtained by proof assistants. We are hoping that some of the counter-example finding methods in ordinal partitions we developed in this formalisation might allow us to make some modest progress in that direction.
The actual formalisation behind our paper was done by Paulson and is available on the Archive of Formal Proofs.
This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic, as developed in this context by Paulson.

The theory of Borel classification is a central research area in modern descriptive set theory. It provides a logical treatment to the process of classification and has been used effectively in different areas of mathematics as a tool to detect structural obstructions against classification theorems.
The idea of making Borel reducibility functorial goes back to the start of the area, being raised already in one of the initial papers by Friedman and Stanley.
In this talk we will discuss yet another attempt to formalize Borel reducibility in a categorical framework.
This is joint work in progress with Andrew Brooke-Taylor.

In this talk I consider modal propositional logic and look for the constraints that are imposed to the propositions of the form $\square a$ by the shape of a Kripke frame.
Using previous work in algebraic statistics, it is shown that the constraints on $\square a$ can be derived through a binomial ideal containing a toric ideal.
I discuss conditions under which the toric ideal, together with the fact that the truth values are in $\{ 0,1 \}$, fully describes the constraints.
This is joint work with G. Pistone and F. Rapallo.

(Based on a joint work with Sara Negri)
In this talk we discuss the semantics and the proof theory of intuitionistic infinitary logic, i.e. intuitionistic logic with countable disjunctions and conjunctions.
We introduce a neighborhood semantics for such logic and then we extract a labelled sequent calculus with full height-preserving invertibility of every rule.
As an application, a Tait-Schutte-Takeuti style form of completeness via the construction of a reduction tree is obtained.
Finally we introduce a labelled sequent calculus for an infinitary version of S4 modal logic and we extend the Gödel-McKinsey-Tarski to the infinitary setting by a proof-theoretic argument based on transfinite induction on the height of derivations.

After a brief recap of what we saw in previous meetings, I will discuss some results in proof theory for provability logic.
In particular, I will focus on labelled sequent calculi and tree hypersequent calculi for GL, and show that it is possible to translate each formalism into the other one.
In conclusion, I will address some open questions concerning a uniform treatment of analytic calculi for provability and interpretability logics, and propose a different reaserch strategy concerning arithmetical completeness for these systems.

When $G$ is a Polish group, one way of knowing that it has ``nice'’ dynamics is to show that $M(G)$, the universal minimal flow of $G$, is metrizable. For non-Polish groups, this is not the relevant dividing line: the universal minimal flow of $\mathrm{Sym}(\kappa)$ is the space of linear orders on $\kappa$---not a metrizable space, but still ``nice''---, for example. In this talk, we present a set of equivalent properties of topological groups which characterize having ``nice'' dynamics. We show that the class of groups satisfying such properties is closed under some topological operations and use this to compute the universal minimal flows of some concrete groups, like $\mathrm{Homeo}(\omega_{1})$. This is joint work with Andy Zucker.

Lawvere's hyperdoctrines mark the beginning of applications of category theory to logic. In particular, existential elementary doctrines proved essential to provide models of non-classical logic. The clear connection between (typed) logical theories and certain functors valued in posets is exemplified by the embedding of the category of elementary doctrines into that of primary doctrines, which has a right adjoint given by a completion which freely adds quotients for equivalence relations. In a joint work with F. Pasquali and G. Rosolini, we extend that result to show that, in fact, the embedding is 2-functorial and 2-comonadic. As a byproduct we apply the result to produce a simpler way to extend a first order theory to one which eliminates imaginaries than Shelah's original, and show how it works in a wide variety of situations.
This talk is part of a series of seminars "Theory and applications of categories".

Several classes of monomorphisms have been introduced in general algebraic contexts. For some of them, there is a purely categorical description that makes it possible a formal study of their structure. In my talk, after a quick recap of such notions, I will focus on the normal subobjects in the sense of Dominique Bourn, and I will describe some (bi)fibrational properties they have. Finally, I will explore the possibility of extending the fibrational point of view to the other classes of monos mentioned above.
This talk is part of a series of seminars "Theory and applications of categories".

Lawvere's Functorial Semantics (FS - http://www.math.union.edu/~niefiels/13conference/Web/) 57 years later is revisited as a common foundation and source of conceptual (but not only) interactions between Logic, Computer Science, Physics and Biology.
Selected topics include:
- functorial semantics of Proof Nets in Logic and Benini-Schenkel-Woike Operadic AQFT in Physics
- AQFT on QuantumSpacetime from a FS perspective.
- "Adaptive Functorial Semantics" (AFS proposal for Evolution in Biology).
- AFS as a Foundation of Data Science.