NOL Seminar with Elaine Pimentel
published: 2025-02-17
event date:
2025-02-24
The Nordic Online Logic Seminar
is organised monthly over Zoom, with expository talks on topics of interest for
the broader logic community. The seminar is open for professional or aspiring
logicians and logic aficionados worldwide. If you wish to receive the Zoom ID
and password for it, as well as further announcements, please subscribe here:
https://listserv.gu.se/sympa/subscribe/nordiclogic
Date Monday, 24 February 2025 at 16:00 CET (UTC+1) on Zoom
Speaker Elaine Pimentel (Department of Computer Science, University College London)
Title Proof-theoretic semantics: from intuitionism to classical, from natural deduction to sequents
Abstract
What is the meaning of a logical connective? This is a very difficult and
controversial question, primarily because its answer depends on the underlying
logical framework. In model-theoretic semantics, the meaning of logical
connectives is grounded in mathematical structures that define validity in terms
of truth. Proof-theoretic semantics (PtS), by contrast, offers an alternative
perspective in which truth is replaced by proof. This shift highlights the role
of proofs as the foundation for demonstrative knowledge, particularly in
mathematical reasoning. Philosophically, PtS aligns with inferentialism, which
holds that the meaning of expressions is determined by inference rules. This
makes PtS particularly well-suited for understanding reasoning, as it defines
logical connectives based on their role in inference.
Base-extension semantics (BeS) is a strand of PtS where proof-theoretic validity is defined relative to a given collection of inference rules regarding basic formulas of the language. Although the BeS project has been successfully developed for intuitionistic propositional logic, first-order classical logic and the multiplicative fragment of linear logic among others, its progression as a comprehensive foundation for logical reasoning is still in its early stages.
In this talk, we will explore Pt-S with a focus on BeS. First, we will introduce an ecumenical perspective to BeS, inspired by Prawitz’s proposal of a system combining classical and intuitionistic logics. The aim is to deepen our understanding of logical reasoning disagreements by investigating the ecumenical approach and developing a unified proof-theoretic foundation for logical reasoning.
We will then address a major challenge in PtS, often called its “original sin”, which is its strong reliance on the natural deduction framework. To overcome this, we propose a version of BeS that employs atomic systems based on sequent calculus rules rather than natural deduction. In this approach, structural rules are treated as properties of atomic systems rather than the logical calculus itself. This allows for a semantics of substructural logics to emerge naturally by modifying the underlying atomic systems. Furthermore, this framework supports a Sandqvist-style completeness proof, but instead of extracting a proof in natural deduction, we obtain one in sequent calculus.
This is based is an ongoing and joint work with Victor Barroso-Nascimento, Luiz Carlos Pereira and Katya Piotrovskaya.