The Speakers

Translations between bases in Base-extension Semantics

Girard showed that using the exponentials of linear logic, one may embed classical and intuitionistic sequents into linear logic. In particular, such translations give concrete ways of translating intuitionistic sequents into intuitionistic linear sequents.

Since the introduction of a sound and complete semantics Base-extension Semantics (BeS) for Intuitionistic Linear Logic (ILL) there has been a natural question about the relationship between bases which support intuitionistic sequents (those defined by Sandqvist) and the bases used to support ILL sequents; namely, can one translate a base used to support an intuitionistic sequent into one that supports a linear sequent? In this talk, I aim to shed some light on these base translations and show that in fact, such translations exist and that these base translations allow us to recover the Girard translations.

Generalised Base-extension Semantics

Since Sandqvist introduced sound and complete base-extension semantics (B-eS) for intuitionistic propositional logic (IPL), there have been several extensions to substructural logics, including fragments of intuitionistic linear logic (ILL) and the logic of bunched implications (BI). We extend these works to a broader class of natural deduction systems, emphasizing a generic approach behind these semantics: elimination rules are derived from introduction rules through definitional reflection, logical connective clauses are formulated in terms of their elimination rules, and completeness is established via atomic encoding. Consequently, the B-eS for IPL and (fragments of) ILL emerge as special cases of this generic framework. Building on these insights, we further explore possible generalizations where sequents exhibit richer algebraic structures, such as bunches, and try to introduce a category-theoretic perspective to the picture where proofs, rather than simple provability, matter.

Reductive logic, proof-theoretic semantics, and coalgebra

Technologies supporting automated reasoning about things like natural language and the correctness/security of systems are a big part of modern life. Indeed, they underpin society's interaction with the systems delivering commerce and government. Their underlying mathematics is 'reductive' logic, wherein one reasons backwards from putative conclusions to sufficient assumptions. This stands in contrast to 'deductive' logic wherein one reasons forwards from established assumptions to conclusions.

Reductive logic needs a philosophical and mathematical foundation. The appropriate logical theory of inference is 'proof-theoretic semantics'. We will talk about how to use proof-theoretic semantics to deliver a foundation for reductive logic, based on inference, that supports reasoning-based technologies.