The third meeting of the Southern Logic Seminar (SLS) will be held on the afternoon of Tuesday 5 September at the University of Birmingham. The meeting will take place in room LG06 in the Old Gym on the main Edgbaston campus.
Participants are encouraged to join the SLS community on Slack, which is used for announcements and coordination. Please contact one of the SLS organisers to be added.
The meeting is supported by a London Mathematical Society Joint Research Groups grant, with additional funding from the UKRI Future Leaders Fellowship Structure vs. Invariants in Proofs (StrIP) and local support from the School of Computer Science at the University of Birmingham.
The programme below is provisional and is subject to change.
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 Room LG06 in the Old Gym on the main Edgbaston campus.
Realizing Continuity Principles Using Effectful Computations. Vincent Rahli, University of Birmingham
The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as MLTT and System T, and is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or references. In this talk, we will present a class of intuitionistic theories that features stateful computations, such as reference cells, and will explain how to extend these theories with continuity axioms such that they have some computational content in the sense that modulus of continuity of a functional on the Baire space is directly computed using the stateful computations enabled in the theory. We will further show how this result can be applied to derive more general continuity principle, and in particular an inductive continuity principle that implies the former notion as well as a uniform variant. If time permits we will also discuss the impact of having effectful computations on other standard axioms such as the Law of Excluded middle and Markov's Principle.
Compressing first-order proofs in deep inference using epsilon-terms. Cameron Allett, University of Bath
In recent years, there has been interest in developing proof systems for first-order classical logic which, for a certain class of tautologies, admit cut-free proofs that are non-elementarily shorter than in traditional Gentzen systems. In this talk, I will introduce "falsifiers", a novel logic defined in the language of Hilbert's epsilon-calculus which enjoys these speedups. Although the epsilon-calculus has its historical roots in Hilbert's program and was initially designed to establish a consistency proof for arithmetic, I shall demonstrate that expanding the language of first-order logic by epsilon-terms can be used to improve certain proof-theoretic normalisation properties and to characterise the semantic behaviour of the non-elementary speedups.
Semantics according to the `meaning-as-use' principle. Alexander Gheorghiu, University College London
Typically, we think of semantics according to the denotational plan in which the meaning of the logical constants is given according to what they say about `truth' in a model --- an abstract mathematical structure. This is not the only way. The 'meaning-as-use' principle is the idea that the meaning of a word is its use in language, can we give a semantics of a logic according to this plan? Since logic is the study of reasoning, we may sensibly fix the 'use' of a logical constant to mean the inferential role, which sets this project in the philosophical paradigm of inferentialism. Such semantics have a long history in logic and have been delivered for intuitionistic, classical, modal, and substructural logics under the umbrella of Proof-theoretic Semantics (P-tS). While P-tS can simply simulate the more traditional possible world semantics, it can also be substantially different. This talk presents the central ideas of P-tS and how they relate to the more main-stream approaches to semantics in logic.
Can proof-nets help in infinitary cut-elimination? Abhishek De, University of Birmingham
Over the past two decades, non-wellfounded and cyclic proof theory has captured the attention of logicians. Such proofs generally come with a 'progress' condition that ensures soundness. From the Curry-Howard perspective, progress conditions bear resemblance to the guardedness condition found in (co)recursive programming. Naturally, these conditions serve as sufficient criteria for guaranteeing the productivity of the infinite cut-elimination process within non-wellfounded proofs. In this talk, I will explore the various complexities inherent in the realm of infinitary cut-elimination and will propose a notion of canonical proof objects, specifically in the form of proof-nets, as a potential avenue for effectively managing these intricacies.
Should Type Theory replace Set Theory as the Foundation of Mathematics? Thorsten Altenkirch, University of Nottingham
Modern Mathematics is based on set theory but there is an alternative: type theory. What is the difference between types and sets? What happens when we base Mathematics on types instead of sets? I will try to answer these questions in my talk. The talk is related to my paper https://arxiv.org/pdf/2111.06368.pdf which appeared in Global Philosophy 33 (1), 21