British Logic Colloquium 2025
&
Peter Aczel Memorial Conference
The University of Manchester (UK)
&
Peter Aczel Memorial Conference
The University of Manchester (UK)
The 2025 meeting of the British Logic Colloquium will take place at the University of Manchester (UK) from 11th to 12th September 2025. It will be preceded by the Peter Aczel Memorial Conference on 10th September 2025.
The programme will include invited and contributed talks on a range of topics including (but not restricted to) categorical logic, computability theory, proof theory, logic in computer science, model theory, philosophical logic, set theory, history of logic.
This meeting aims to bring together researchers working in logic and related areas, both from the UK and overseas, to share and discuss recent developments in those areas. The plenary speakers are all leaders in their respective fields, and their talks would normally cover not only their own work but also important related research in their fields. This would benefit all the participants and, in particular, junior researchers including students and postdocs. The contributed talks would benefit the speakers by giving them an opportunity to present their work to a general logic audience (outside their immediate research area) and by encouraging discussions with both senior and junior logicians.
Dates:
10th September 2025 (Peter Aczel Memorial Conference)
11th-12th September 2025 (British Logic Colloquium)
Venue: Alan Turing Building, University of Manchester
BLC
Mirna Džamonja (Paris)
Fairouz Kamareddine (Heriot-Watt)
Fraser MacBride (Manchester)
Paul-André Melliès (Paris)
Paula Quinon (Warsaw/Gothenburg)
Katrin Tent (Münster)
Frank Wolter (Liverpool)
Peter Aczel Memorial Conference
Steve Awodey (Carnegie Mellon University)
Jouko Väänänen (University of Helsinki)
Rosalie Iemhoff (Utrecht University)
Andrew Swan (University of Ljubljana)
All talks, other than one of the parallel sessions of contributed talks, will be in the room G.207 in the Alan Turing Building. The AGM will also be in G.207.
Registration, lunches, and tea/coffee breaks will take place just outside G.207.
Reception and dinner will take place in the kitchen area/atrium bridge on the first floor.
Each day, Session 1 will be in G.207 on the ground floor of Alan Turing, and Session 2 in Frank Adams 1 on the first floor of Alan Turing.
Peter Aczel Memorial Conference
Steve Awodey (Carnegie Mellon University)
Jouko Väänänen (University of Helsinki)
Title: On internal categoricity
Abstract: I will give an overview of internal categoricity of second order theories. I will discuss its benefits in comparison with ordinary categoricity. I will then move on to internal categoricity of first order theories, mainly arithmetic and set theory. There is no comparison to ordinary categoricity since the relevant first order theories are famously non-categorical. Instead, I will discuss the question, what is the relevance of internal categoricity in first order arithmetic and set theory.
Rosalie Iemhoff (Utrecht University)
Andrew Swan (University of Ljubljana)
Title: (Higher) inductive types in (constructive) set theory
Abstract: In the third of Aczel's papers introducing CZF he extended his set theory with a new axiom he called the *regular extension axiom*, allowing the easy construction of sets by inductive definition inside the theory. Although inductive definitions in set theory are closely related to inductive types in type theory, one of the inductive definitions in Aczel's paper, that of sets of hereditarily bounded cardinality, can also be regarded as a kind of *higher inductive type*, i.e. as one where the construction of new elements and of equalities between elements are simultaneously defined as parts of a single inductive definition. I will talk about a special case of this definition, hereditarily countable sets, alongside two related examples: ordinals of hereditarily countable cofinality and unordered countably branching trees. I'll talk about the behaviour of these higher inductive types in both constructive set theory and classical set theory without choice.
BLC
Joop Leo & Fraser MacBride
Title: Varieties of Symmetry: Full, Partial, Strict and Mere
Abstract: What is a symmetric relation? The notion of symmetry for binary relations is familiar. But when we turn to relations of arity greater than 2, different possibilities open up which are absent from the binary case. We define and motivate a variety of definitions of symmetry, differing with respect to the logical and mathematical machinery they invoke, including definitions for what we call ‘full' and ‘partial’ symmetry. We then define and motivate corresponding definitions for ’strict’ symmetry, which invoke an ontology of states, and ‘mere’ symmetry, which are relations that aren’t strictly symmetric, and explore candidates for relations that satisfy the criteria for being merely symmetric relations. Our outlook is one of tolerance. We don’t look for a privileged definition of symmetry, one which uniquely captures what symmetry really is.
Frank Wolter
Title: The Interpolant Existence Problem
Abstract. A Craig interpolant for formulas phi and psi is a formula using only the shared non-logical symbols of phi and psi which is entailed by phi and entails psi. A logic has the Craig Interpolation Property (CIP) if a Craig interpolant for phi and psi exists whenever phi entails psi.
Hence the CIP reduces a potentially hard existence problem to an entailment problem. First-order logic, intuitionistic logic, and many modal logics enjoy the CIP. In this talk, I will discuss what happens if a logic does not enjoy the CIP. I will focus on decidability of the interpolant existence problem and therefore on logics for which entailment is decidable. I will discuss decidable fragments of FO such as the two-variable and guarded fragments and also a few modal logics. Often, the interpolant existence problem turns out be one exponential harder than entailment, and sometimes even undecidable for decidable logics. For temporal logics, I will relate interpolant existence to separation of regular languages by first-order definable languages. Finally, I will consider interpolants in which also logical symbols are disallowed.
Paula Quinon
Title: Is the concept of computation a conceptual fixed point?
Abstract: \{Conceptual engineering} is a philosophical activity that involves the reframing or refinement of a given concept to better suit specific scientific, philosophical, or social contexts (Cappelen 2018). Has\-lan\-ger's (2000) work on the concepts of ``gender'' and ``race'' is often cited as a flagship example of conceptual engineering, not only for its methodological interest, but also for Halsanger's social justice ``ameliorative'' project. More recently, formal or mathematical concepts have also attracted the attention of conceptual engineers. However, not all concepts can be engineered. Some need to be kept as \emph{fixed points} in order to preserve the intended conceptual structure of their respective frameworks, or because they have properties that make them \emph{natural fixed points} that play the same role consistently across different frameworks. Fixed points have been studied in formal contexts where concepts such as ``truth,'' ``existence,'' and ``quantifier'' are considered to be resistant to engineering (Eklund 2015). In this paper, I explore the theoretical concept of computation as explicated by the Church-Turing Thesis, and argue that it constitutes a natural conceptual fixed point.
Mirna Džamonja
Title: Property B: a generalisation of Baumgartner’s Axiom A
Abstract: In 1978 Baumgartner introduced Axiom A forcing. It preserves $\aleph_1$ in iterations with countable support and includes many familiar notions of forcing. These include perfect set aka Sacks forcing and various other tree forcings, as well as the forcing adding a Prikry-Silver real and products of the same. A more general concept of proper forcing was introduced by Shelah shortly after the Axiom A forcing. Its rapid development pushed Axiom A into the oblivion, but in fact, there are some but not so many examples of proper forcing that do not satisfy Axiom A. More recently it has been of interest to develop iterated forcing theory for iterations with supports of size $\aleph_1$, where both $\aleph_1$ and $\aleph_2$ are preserved. The generalisations naturally sought to generalise proper forcing, but there are various difficulties in doing so. In this work we present the programme of developing such a theory through generalising Axiom A forcing rather than proper forcing. The resulting property is called property B. We prove a conditional iteration theorem on property B forcing and obtain a concrete result regarding the iterabilility of the generalisation of the perfect set forcing to trees on $\aleph_1$.
Paul-André Melliès
Title: Recent advances in tensorial logic and functorial game semantics
Abstrac: Tensorial logic is a primitive logic of sum, tensor and negation which refines linear logic by relaxing the requirement that linear negation is involutive. The logic is designed in such a way that its formulas [modulo canonical isomorphism] are in a one-to-one correspondence with dialogue games, and that its proofs [modulo cut-elimination] are in a one-to-one correspondence with innocent strategies.
In this introductory talk, I will explain how to incorporate the exponential modality of linear logic in order to expand the proof-theoretic and functorial approach to game semantics beyond the multiplicative and additive fragment of tensorial logic. Somewhat surprisingly, the extension is based on a tensorial logic with two negations: the standard tensorial negation together with a new exponential and backtracking negation.
My talk will mainly focus on presenting a recent coherence theorem for tensorial logic, which states that the free dialogue category with two negations (tensorial and exponential) coincides with a specific category of innocent and well-bracketed strategies between dialogue games. I will explain the result and use it to derive a general positionality theorem for innocent and well-bracketed strategies.
This coherence theorem for dialogue categories with two negations represents a significant development in the research programme on functorial game semantics which began around fifteen years ago, inspired by ribbon categories and functorial knot theory.
Katrin Tent
Title: On the model theory of the Farey graph and the free factor complex (joint work with Z. Mohammadi)
Abstract: The free factor complex of a free group of finite rank shares many properties with finite dimensional projective spaces. I will explain the geometry of the the free factor complex and will show how to see that at least for rank 2 the complex is
\omega-stable.
Fairouz Kamareddine
Title: Numbers, Sets, Types, and Paradoxes
Abstract: Aristotle may well have said first that proof checking is decidable whereas proof finding is not. But this is a ground breaking result of Turing and Goedel who showed that Leibniz, Hilbert and others' dream of finding a language and a method that could carry out proof checking and proof finding is impossible. From the old times of Artistotle till today, logic has been plagued by the paradoxes and the infinite. Solutions called for new formalisms but the problems kept returning leading again to newer theories each time. E.g., Principia Mathematica was conceived as a rigorous foundation for logic and mathematics but the complications of its substitution rule led Haskell Curry to conceive of combinatory logic and embark on a lifelong search for powerful systems that combine computations and deductions (functions and logic) and that are able to better formalise mathematics. The number systems, type and set theories as well as other formalisms all evolved as part of the struggle to internalise/define as much as possible while avoiding contradictions. This talk starts as an introductory stroll in the world of numbers, functions, types and logic with a hint of their evolution attempting to explain why and how we got here. We explain how the number systems evolved despite the ancient fear of the infinite, how functions took a central role in modern logic, and how types became basic for mixing functions and logic while avoiding the paradoxes and ensuring termination. Even though we focus on the so-called pure type systems (PTSs) which incorporate polymorphic and dependent types, we give a new formulation based on intersection types which represents intersection types using finite set declarations. Our new PTS characterizes strongly normalising (terminating) terms, something which existing PTSs fail to do since they are not able to type all the terminating terms they represent.
Registration is now closed.
The registration fee will cover lunch and tea/coffee breaks.
The deadline for applying for funding has now passed.
We expect to have a limited number of travel grants available to UK PhD students who wish to attend BLC 2025. We also expect to provide modest grants to support participants with caring responsibilities. If you would like to apply for funding (either as a UK PhD student or as a carer), please complete the below form by 31st July. We will get in touch in August to let you know if and how much funding we can provide.
The deadline for submitting contributed talks has now passed.
The programme committee invites abstracts for contributed talks of up to 1 page (excluding bibliography). These can be on published or unpublished work, as well as work in progress. We especially encourage students and early-career researchers to present their work. If you want to give a contributed talk, please fill in the below form by 31st July. We will get in touch with you shortly after that to confirm whether you have been selected for a contributed talk. These talks will be scheduled on the BLC days (11-12th September).
Pendulum Hotel Sackville Street
Ibis Manchester Centre Princess Street
Premier Inn Manchester City Centre Princess Street
Holiday Inn Express Manchester City Centre Oxford Road
Travelodge Manchester Upper Brook Street
BLC organising committee: Vahagn Aslanyan, Nicola Gambino, Omar Leon Sanchez, Renate Schmidt
BLC scientific committee: Vahagn Aslanyan (Manchester), Nicola Gambino (Manchester), Frederique Janssen-Lauret (Manchester), Omar Leon Sanchez (Manchester), Renate Schmidt (Manchester), Sara Uckelman (Durham)
Peter Aczel Memorial Conference organising committee: Nicola Gambino (Manchester), Michael Rathjen (Leeds)
London Mathematical Society (LMS), Heilbronn Institute for Mathematical Research (HIMR), UKRI/EPSRC Additional Funding Programme for Mathematical Sciences, British Logic Colloquium (BLC), Manchester Institute for Mathematical Sciences (MiMS)