**Cross-Alps Logic Seminar**
An online seminar series gathering the logic groups at the universities of Genoa, Lausanne, Turin and Udine.

**Past seminars at DIMA:**

**Friday, March 17th 2023**
· 14h00-18h00 CEST, Room 706

**Genoese recollections on Lawvere's work and ideas**
An informal meeting in Genoa to celebrate and recollect some of the work of

Bill Lawvere.

Tentative list of speakers:

· Marco Grandis

· Eugenio Moggi

· Ruggero Pagnan

· Fabio Pasquali

· Pino Rosolini

The meeting is in person and everyone is welcome to join. Registration is not required, but please write to one of the organisers in case you wish to join for dinner afterwards.

For any question feel free to write to one of the other organisers:

Greta Coraglia,

Francesco Dagnino,

Jacopo Emmenegger,

Enrico Ghiorzi.

**Thursday, Sept. 30th 2021**
· 16h00 CEST, Room 706

Jérémie Marquès (Université de Nice Sophia-Antipolis)

**Title:** Translations of type space functors

[

Abstract | Slides]

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".

**Tuesday, June 8th 2021**
· 15h00 CEST (13h00 UTC), online seminar

Joanna Ko (University of Göttingen)

**Title:** Groupoid Models for Diagrams of Groupoid Correspondences

[

Abstract | Slides]

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.

**Thursday, May 27th 2021**
· 15h00 CEST (13h00 UTC), online seminar

Sebastiano Thei (University of Trento)

**Title:** Class forcing and set-theoretic geologies

[

Abstract |

Slides]

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.

**Monday, February 1st 2021**
· 14h00 CET (13h00 UTC), online seminar

Mirna Džamonja (Institut d'Histoire et de Philosophie des Sciences et des Techniques, Paris, and Institute of Mathematics Czech Academy, Prague)

**Title:** Formalising Ordinal Partition Relations Using Isabelle/HOL

[

Abstract | Slides]

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.

**Monday, January 11th 2021**
· 15h00 CET, online seminar

Filippo Calderoni (University of Illinois at Chicago)

**Title:** Categorifying Borel reducibility

[

Abstract | Slides]

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.

**Monday, November 23rd 2020**
· 14h00 CET, online seminar

Riccardo Camerlo (University of Genoa)

**Title:** Modal Operators and Toric Ideals

[

Abstract |

Slides]

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.

**Monday, November 2nd 2020**
· 15h00 CET, online seminar

Matteo Tesi (SNS)

**Title:** Proof-theory and neighborhood semantics for infinitary intuitionistic logic with an application to Gödel- McKinsey-Tarski embedding

[

Abstract |

Slides]

(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.

**Tuesday, September 29th 2020**
· 16h00 CEST, online seminar

Fifth meeting of the working seminar on

**Modal logic**. Speaker: Cosimo Perini Brogi (University of Genoa)

[

Abstract |

Slides]

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.

**Tuesday, September 8th 2020**
· 17h00 CEST, online seminar

Gianluca Basso (University of Lausanne)

**Title:** Topological dynamics beyond Polish groups

[

Abstract | Slides]

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.

**Tuesday, February 25th 2020**
· 14h00, room 714

Jacopo Emmenegger (University of Genoa)

**Title:** Elementary doctrines as coalgebras

[

Abstract | Slides]

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".

**Thursday, February 20th 2020**
· 15h30, room 714

Giuseppe Metere (CNR)

**Title:**
[

Abstract | Slides]

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".

**Thursday, February 13th 2020**
· 14h00, room 713

Jean-François Mascari (CNR)

**Title:** Functorial semantics in logic, computer science, physics and biology

[

Abstract | Slides]

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.

**Previous years:** 2018,

2019.