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.