British Logic Colloquium Bristol 2023









BLC 2023 

The BLC2023 will be held on Thursday afternoon to Saturday lunchtime, September 7-9th, 2023 in Room 2.04 of the Fry Building at the School of Mathematics, University of Bristol.

Following on the BLC, co-located in the Fry Building will be Johannes Stern’s “Working with Truth” workshop; this will be the Saturday 9th in the afternoon and on Sunday 10th. (A separate registration is required for this.)



Speakers for the BLC will include: 

  • Sandra Müller (TU Vienna)  
  • Paul Shafer (Leeds)  
  • Juan Aguilera (Ghent and TU Vienna)
  • Vicenzo Mantova (Leeds)    
  • Carlo Nicolai (KCL)
  • Elaine Pimentel (UCL)
  • Juliette Kennedy (Helsinki) 
  • Anupam Das (Birmingham)
  • Ali Enayat (U. of Gothenburg)
  • Abstracts - where received - are below. 

We anticipate that there will a timetabled slot for a small number of probably shorter contributed talks. If you wish to be considered for giving such a talk please forward a title and abstract to Philip Welch ( 

Participants are also encouraged to bring posters of their work for display.

On the Thursday evening there will be a General Meeting of the BLC.

On the Thursday evening there will also be a conference dinner on the harbourfront, 7.30pm, at the 





14.00 - 15.00 Lecture V. Mantova 

        Quasi-minimality of complex exponentiation: are we there yet?

15.00 - 15.30 Tea

15.30 -16.30 Lecture  S. Müller 

        Generic absoluteness for the definable powerset of the universally Baire sets

16.30 - 17.30 Lecture  J. Kennedy Extracting syntax from semantics

17.45 - 18.30 BLC Annual Meeting

19.30 Dinner


9.00 -10.00 Lecture C. Nicolai Non-Wellfounded Properties

10.00 -10.30 Tea/Coffee

10.30 - 11.30 Lecture  P. Shafer Usual theorems of unusual strength

11.30 - 11.55 Contributed Talk: P.Dopico 

       A rose by any other name: more supervaluation-style truth without supervaluations

12.00 - 12.25 Contributed Talk: P. Brocci 

       Minimal variants of axiomatic theories of truth


14.00 - 15.00 Lecture Lecture  J. Aguilera. Some results on Gödel logics 

15.00 - 15.30 Tea

15.30 - 16.30 Lecture  A. Das On the proof theoretic strength of circular reasoning


9.30 -10.30   Lecture A. Enayat Satisfaction classes, truth theories, and nonstandard models of arithmetic

10.30 -11.00 Tea/Coffee

11.00 - 12.00 Lecture  E. Pimentel Axioms as rules: How to reason with mathematical theories

See Fry Building on the map:


Other maps and travel information:

Travel: From Heathrow the express coach is direct and is almost the easiest way to get to Bristol. The Bristol Bus/Coach station is within a fairly stiff 10/15 min. walk of Fry and Berkeley Square Hotel. In Bristol, bus number 8 from the train station (or from near the Bus Station) will take you very near the Berkeley Square Hotel; (“Park street Top”) they also stop at  “The Triangle West” (5 mins walk to Fry). Bus Number 8 continues on to the Rodney Hotel (“by the Quadrant pub'', in Clifton).

Rodney Hotel to Fry Building walking route

For Accommodation: The Rodney Hotel (in Clifton) and The Berkeley Square Hotel will house most speakers.  Postgrads may wish to consider Toad Lodge or as usual AirBNB 





Juan Aguilera:

“Some results on Gödel logics”

I will survey some results concerning model-theoretic and computability-theoretic aspects of Gödel logics and in particular of scattered Gödel logics. These were introduced by Gödel in his proof that  intuitionistic logic is not finite-valued. They are extensions of intuitionistic logic which take truth values in some closed subset of the unit interval. Even though they appear tame and are weaker than classical first-order logic, their proper study requires the use of highly non-computable Turing degrees and relatively large uncountable cardinals.

Anupam Das: 

“On the proof theoretic strength of circular reasoning"

Classical approaches to logic and computation model inductive reasoning by recursion. However such a ‘black box’ approach admits no finer decomposition of inductive reasoning. Contrast this with, say, the use of an ω-rule in proof theory, recovering a metalogical analysis at the cost of finite presentability. However there is another, perhaps more drastic, approach: circular reasoning. Here the dependency graph of a proof need not be well-founded but is typically regular, akin to low-level computational models with loops while nonetheless enjoying excellent metalogical properties. Naturally, such ‘proofs’ may admit fallacious reasoning, and so one typically employs some global correctness condition inspired by ω-automaton theory to ensure logical soundness. Nowadays cyclic and non-wellfounded proof systems are a common technique for demonstrating metalogical properties of systems incorporating (co)induction, including modal logics, predicate logics, type systems and algebras. The tools employed in cyclic proof theory are diverse, exhibiting beautiful interplays between proof theory, automata theory, reverse mathematics and other areas. In this talk I will address a question at the heart of this subject: how strong is circular reasoning? In particular I will survey a recent line of work addressing this question in the setting of arithmetic, comparing cyclic systems to their usual inductive counterparts.”

Ali Enayat

“Satisfaction classes, truth theories, and nonstandard models of arithmetic”

At first approximation, a satisfaction class on a nonstandard model M of arithmetic or set theory is a binary relation S on M that shares many of the salient features of the usual Tarskian satisfaction relation on M, but in sharp contrast to the Tarskian satisfaction relation, a satisfaction class is required to decide the `truth' of some (or even all) nonstandard formulas of M. This notion was brought to prominence in the 1970's, thanks to the fine efforts of a number of logicians---especially in Poland---including Krajewski, Kotlarski, Lachlan, Murawski, Ratajczyk, Kossak,and Schmerl. A notable precursor is a 1963 paper of Abraham Robinson, which probed the subtle obstacles in the development of a coherent Tarski-style semantic framework for first order formulas of nonstandard length. 

The flurry of activity in the 1970's and 1980's primarily focused on models PA and revealed two distinct `flavors' of satisfaction classes: full satisfaction classes and inductive satisfaction classes. The past decade has witnessed a renewed interest in the subject, especially due to the intimate relation between full satisfaction classes and the lively subject of axiomatic theories of truth in philosophical logic. In this talk I will present a survey of a number of model-theoretic and proof-theoretic results regarding satisfaction classes and the closely associated topic of truth theories, with special emphasis on the latest developments.

Juliette Kennedy 

“Extracting syntax from semantics”

If a model class is a class of structures of the same similarity type closed under isomorphism, under what conditions can the class be said to have a natural syntax, or a natural logic? How to think about model classes that have no syntax, no notion of formula? More generally, does syntax always supervene on semantics? In this talk we present some old and new results dealing with these questions.

Vicenzo Mantova

“Quasi-minimality of complex exponentiation: are we there yet?”

No! But we sure are trying. More than 20 years ago, Zilber asked if complex exponentiation is quasi-minimal, meaning that in the language of fields with an exponential function, every definable subset of
is either countable or the complement of a countable set. He then proposed that is "exponentially-algebraically closed" (EAC), which is an even stronger statement. I will motivate the conjecture using a slightly alternative history, starting from work of Keisler about the quantifier 𝐐 "there exist uncountably many". I will then survey the progress on the EAC conjecture and its variations, including, very notably, the unconditional quasi-minimality theorem of complex raising to powers by Gallinaro and Kirby.

Sandra Müller

“Generic absoluteness for the definable powerset of the universally Baire sets”

Universally Baire sets play an important role in studying canonical models with large cardinals. But to reach higher large cardinals more complicated objects, for example, canonical subsets of universally Baire sets come into play. Inspired by inner model theory, we introduce the definable powerset of the universally Baire sets and show that, after collapsing a large cardinal, the constructible universe of the definable powerset of the universally Baire sets is a model of determinacy and its theory cannot be changed by forcing. Even though the work is inspired by inner model theory, the techniques do not use any fine structure. This is joint work with Grigor Sargsyan. The talk will be introductory and all relevant concepts and ideas will be introduced.

Carlo Nicolai

"Non-Wellfounded Properties"

In the talk I investigate the simple, yet unexplored idea that satisfactory property theories could arise from suitable modifications of standard set theories. I will focus on three main desiderata for a property theory: mathematical adequacy (the theory should be able to recover the ontology of sets as extensional properties), self-application (self-applicable property should provably exist), unification ("semantic" and set theoretic paradoxes should have a unified solution). I will survey some formal options based on a property-theoretic version of the anti-foundation axiom, and discuss a conception of properties, the graph conception, which underpins such options. 

Elaine Pimentel.   

“Axioms as rules: How to reason with mathematical theories”

One of the advantages of using sequent systems as a framework for logical reasoning is that the resulting calculi are often simple, have good proof theoretical properties (like cut-elimination, consistency, etc) and can be easily implemented, eg using rewriting.

Hence it would be heaven if we could add axioms in mathematical theories to first order logics and reason about them using all the machinery already built for the sequent framework. Indeed, the general problem of extending standard proof-theoretical results obtained for pure logic to certain classes of non-logical axioms has been the focus of attention for quite some time now.

The main obstacle for this agenda is that adding non-logical axioms to systems while still maintaining the good proof theoretical properties is not an easy task. In fact, adding naively axioms to sequent systems often result in non cut-free systems. One way of circumventing this problem is by treating axioms as theories, added to the sequent context. This is already in Gentzen's consistency proof of elementary arithmetic. Now the derivations have only logical axioms as premises, and cut elimination applies.

But we can do better by transforming axioms into inference rules. In this talk, we will propose a systematic way of adding inference rules to sequent systems. The proposal will be based on the notions of focusing and polarities. We will also discuss how our framework escalates to hypersequents and systems of rules, and the application of this to modal logics, proofs explanation and SMT solvers.

This is a joint work with Dale Miller, Sonia Marin, Marco Volpe, Francesca Poggiolesi and Yoni Zohar.


Paul Shafer   

"Usual theorems of unusual strength"

We survey recent results in reverse mathematics, highlighting theorems from the general mathematics literature whose logical strength is unusual in some way. The Rival-Sands theorem for partial orders is a Ramsey-theoretic result concerning chains in partial orders of finite width. We show that the Rival-Sands theorem is equivalent to the ascending/descending sequence principle, which is a weak consequence of Ramsey's theorem for pairs (joint with Fiori Carones, Marcone, and Soldà). This gives the first example of a theorem from the modern literature that is characterized by the ascending/descending sequence principle. Ekeland's variational principle concerns approximate minima of lower semi-continuous functions that are bounded below. We show that the localized version of Ekeland's variational principle is equivalent to Pi^1_1-CA_0, even when restricted to continuous functions (joint with Fernández-Duque and Yokoyama). This is unusual because the much weaker system ACA_0 typically suffices to prove theorems about continuous functions. Caristi's fixed point theorem is a consequence of Ekeland's variational principle that concerns fixed points of arbitrary functions that are controlled by lower semi-continuous functions. We show that Caristi's theorem for Borel functions is equivalent to Towsner's transfinite leftmost path principle and therefore has the unusual position of being strictly between ATR_0 and Pi^1_1-CA_0 (joint with Fernández-Duque, Towsner, and Yokoyama).

Contributed Talks

Pietro Brocci

“Minimal variants of axiomatic theories of truth’’

In the first part of the talk, we will present and study the theory KFB, i.e. the minimal variant of the Kripke-Feferman theory of truth which was introduced by J.P. Burgess.  The theory exhibits desirable properties: it refutes the truth-teller and it exceeds the proof-theoretic strength of the regular Kripke-Feferman theory. In particular, the theory is as strong as ID_1, an impredicative theory.

In the second part, we explore if this strategy can be applied to obtain other minimal versions of axiomatic theories of truth. In particular, we focus on minimal variants of the theory PUTB introduced by Volker Halbach. We check that these disquotational theories refute the truth-teller and achieve the same proof-theoretic strength as KFB. 

In the last part, we prove some interpretability relationships between KFB and the new disquotational theories. Finally, we draw philosophical conclusions on the releationship between truth and impredicativity while also sketching  further lines of research. 

Pablo Dopico

“A rose by any other name: more supervaluation-style truth without supervaluations” 

One of the main shortcomings of Saul Kripke’s xed-point semantics based on the Strong Kleene logic, presented for the rst time in [Kri75], is that it leaves many logical truths out of the extension of the truth predicate. Thus, as an alternative, Kripke suggests to construct the xed-point models on the basis of the supervaluationist semantics advanced by van Fraassen [vF66]. What obtains is a supervaluatonist xed-point semantics that has arguably constituted one of the most popular solutions to the paradoxes of self-reference. 

However, the supervaluationist xed-point theory of truth is not free from objections. The nal picture yields a non-compositional theory of truth whose evaluation scheme is highly intransparent and that cannot be N-categorically axiomatized [FHKS15] like the Kripke-Strong Kleene can. For this reason, Johannes Stern [Ste18] has recently advanced a theory (labelled SSK) that also meets the goal of the Kripkean supervaluationist theory (i.e., to include all rst-order logical truths) while allegedly accounting for the failure of composi- tionality, and allowing for a N-categorical axiomatization. 

Our main contribution in this paper is to show that SSK is strikingly similar to a rather understudied theory: Vann McGee’s theory of de nite truth as presented in [McG91]. In the rst part of the paper, we present both theories and prove that McGee’s original theory coincides with the minimal xed point of Stern’s theory, modulo a suitable restriction of the language. In the second part, we show how to generalise McGee’s theory to any starting inductive set, and prove once again that these theories à la McGee coincide with Stern’s SSK xed points. On the basis of this, we submit that McGee’s theory is an alternative way of obtaining supervaluation-style truth without supervaluations. Finally, in the last part of the paper, we o er a proof-theoretic analysis of what we consider to be the most natural rst-order axiomatization of McGee’s theory, showing that it has the same proof-theoretic strength as the well-known theory KF.