British Logic Colloquium 2025

Peter Aczel Memorial Conference

•  Steve Awodey (Carnegie Mellon University)

Title: The Effective Infinity-Topos

Abstract: Hyland’s effective topos Eff contains an object of natural numbers N  for which all functions from N to N are computable [1].  As an elementary topos, Eff models extensional Martin-Loef type theory with a universe of propositions Omega that is ``impredicative'', in the sense that it is closed under universal quantification over arbitrary domains.  This is not hard to understand, because Omega is a poset in Eff, and the impredicative quantification simply asserts the completeness of Omega, in the same way that a powerset P(X) is complete in virtue of having arbitrary intersections for families of subsets indexed by arbitrary sets.

But Eff also contains another impredicative universe U that is not a poset [2] --- a fascinating combination not consistent with classical foundations. And indeed, the ``internal logic'' of Eff is intuitionistic higher-order logic.   

In recent joint work with M. Anel and R. Barton, we construct a higher-dimensional realizability topos Eff_oo with a hierarchy of such impredicative universes Omega, U, U1, ..., each of which is also univalent in the sense of homotopy type theory and univalent foundations.  Such universes can be used to give impredicative encodings of (higher) inductive types [3].  The infinity-topos Eff_oo includes the 1-topos Eff as its subcategory of 0-types, so its object of natural numbers N has the same first-order properties as in Eff.   

This builds on prior joint work [4].

[1] J.M.E. Hyland, The effective topos. In: The L.E.J. Brouwer Centenary Symposium, A.S. Troelstra and D. van Dalen (ed.s), Elsevier, 1982.

[2] J.M.E. Hyland, A small complete category.  Annals of Pure and Applied Logic, (40)2, pp. 135--165, 1988.

[3] S. Awodey, J. Frey, S. Speight,  Impredicative encodings of (higher) inductive types. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18), pp. 76--85, 2018.

[4] S. Awodey, J. Emmenegger, G. Rosolini, Toward the effective 2-topos, (forthcoming), 2025.

•  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)

Abstract 

•  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 

Abstract: 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. 

BLC contributed talks

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

Venue: Alan Turing Building, University of Manchester

Travel

For information on travelling to Manchester and to the campus, please visit this website.

You can find the Alan Turing Building on campus map here.

The main train station in Manchester is the Piccadilly Station, about 20-minute walk away from the Alan Turing Building (map). There are regular trains from Manchester Airport to Piccadilly Station (approximately once per 15 minutes); a ticket costs around £6 and the ride is about 15-minute long (check here). The Oxford Road station is within 15 minutes, while the Victoria station is a bit farther (about 40 minutes), although it is possible to take a bus to the campus.

Suggested accommodation

• 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)