The MGS Christmas Seminars 2023 will take place on **Thursday 14 ^{th} December** in

The Midlands Graduate School (MGS) is an annual spring graduate school on the mathematical foundations of computing science. It has run annually since 1999 and has been held at either the University of Birmingham, the University of Leicester, the University of Nottingham, or at the University of Sheffield. The lectures are aimed at graduate students, typically in their first or second year of study for a PhD, but the school is open to anyone who is interested in learning more about mathematical computing foundations, and all such applicants are warmly welcomed. We very much encourage learners from abroad and from industry to attend, and many have done so in the past. The next MGS Graduate School will take place at the University of Leicester, 8-12 April.

Participation is free to all, and no registration is required.

This event is co-located with the 4^{th} Southern and Midlands Logic Seminar, also taking place in Birmingham the previous day,
Wednesday 13^{th} December.
Participants of each event are encouraged to attend both! We will organise a social dinner on the evening of Wednesday 13th, between the two events.

- 14:00–14:45. Elaine Pimentel, University College London.
*Ecumenical and substructural views of proof-theoretic semantics.* - 14:45–15:15. Break.
- 15:15–16:00. Dan Marsden, University of Nottingham.
*Games, Logic and Compositionality.* - 16:00–16:30. Break.
- 16:30–17:15. Jakub Opršal, University of Birmingham.
*NP-hardness of colouring certain graphs with 3 colours via homotopy.* - 18:30– onwards. Pub social at Cherry Reds with buffet festive dinner.

There will be a social dinner from **18:30, Wednesday 13 ^{th} December** at Hen & Chickens (15 minutes walk from New Street station)
between the SMLS meeting and the MGS Christmas Seminars.
There will also be a pub social from

~~Before the Christmas Seminars on Thursday 14~~
(The Noble Room will be closed for Christmas already!)
^{th} many of us will go to the
Noble Room for lunch at 12:30.

The main campus of the University of Birmingham is located in Edgbaston, just outside the city centre. There are frequent trains serving the campus train station (University), about a 10 minute journey from Birmingham New Street. There are also regular buses, but trains will be more convenient for most. Google Maps is reliable for checking train and bus times. It is also possible to travel to/from the campus on foot along the canals, about a 50-60 minute walk from the centre.

All talks, lunch and coffee breaks will take place in **UG09 in the Murray Learning Centre** on the main Edgbaston campus.

*Ecumenical and substructural views of proof-theoretic semantics*. Elaine Pimentel, University College London.

Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of logical proofs as one of the main points of controversy. The intuitionist advocates for a strict notion of constructive proof, while the classical logician advocates for a notion which allows non-constructive proofs through reductio ad absurdum. A great deal of controversy still subsists to this day on the matter, as there is no agreement between disputants on the precise standing of non-constructive methods.
Two very distinct approaches to logic are currently providing interesting contributions to this debate. The first, oftentimes called logical ecumenism, aims to provide a unified framework in which two "rival" logics may peacefully coexist, thus providing some sort of neutral ground for the contestants. The second, proof-theoretic semantics, aims not only to elucidate the meaning of a logical proof, but also to provide means for its use as a basic concept of semantic analysis. Logical ecumenism thus provides a medium in which meaningful interactions may occur between classical and intuitionistic logic, whilst proof-theoretic semantics provides a way of clarifying what is at stake when one accepts or denies reductio ad absurdum as a meaningful proof method.
In the first part of our talk we show how to coherently combine both approaches by providing not only a medium in which classical and intuitionistic logics may coexist, but also one in which classical and intuitionistic notions of proof may coexist.

In the second part, we will discuss substructural behaviors using a Proof Theoretic Semantics view. In particular, we will propose a "INFERENCES-AS-RESOURCES" approach, contrasting to the recent Gheorghiu, Gu and Pym's "ATOMS-AS-RESOURCES" approach to intuitionistic multiplicative linear logic (IMLL), and show how this can be smoothly extended to the full intuitionistic linear logic.

This is an ongoing and joint work with Victor Nascimento, Luiz Carlos Pereira and Yll Buzoku.

*Games, Logic and Compositionality*. Dan Marsden, University of Nottingham.

This talk will discuss a categorical approach to compositionality
theorems for logical equivalence in finite model theory. Our approach involves model
comparison games, and their abstraction via the recently introduced notion of game comonads.
The presentation will assume only basic category theory and elementary knowledge of first-order logic.

Joint work with Tomas Jakl and Nihil Shah.

*NP-hardness of colouring certain graphs with 3 colours via homotopy*. Jakub Opršal, University of Birmingham.

A colouring of a graph with k colours is an assignment of colours to vertices so that no edge is monochromatic. It is well-known that if there is a polynomial time algorithm for finding a colouring with 3 colours even when we are promised that such a colouring exists, then the computational classes P and NP collapse. This raises a question of whether we can efficiently colour graphs that are promised satisfy a stronger condition, e.g., those that allow a homomorphism (an edge-preserving map) to an odd cycle?

In a proof based on topological ideas (first used to show lower bounds of chromatic number of Kneser graphs by Lovász), we will show that this strengthening the promise does not make the problem easier, and we will discuss where these topological ideas might lead in classification of computational complexity of similar problems in the near future.

Anupam Das

Jamie Hough

Any queries should be addressed to Anupam Das.