Uploaded June 2025 | Updated September 2026, 1 day ago
Recorded as part of the CFvW colloquium on June 18, 2025
On the power and flexibility of base-extension semantics -
Dr. Victor Luis Barroso Nascimento (University College London)
Abstract:
Proof-theoretic semantics (PtS) provides an alternative to model-theoretic semantics by considering proof, not truth, as the basic unit of semantic analysis. This is informed by the philosophical view that our way of engaging with and obtaining knowledge about the world is essentially inferential in nature. Although multiple approaches to PtS are currently being developed, base-extension semantics (BeS) has distinguished itself as one of the most fruitful. In this talk I will present a series of results across multiple contexts with the aim of showing how flexible and powerful BeS is a semantic
framework.
The first result, developed in the context of logical ecumenism, shows that a particular treatment of the absurdity constant allows us to formulate a interesting proof-theoretic concept of classical proof, and by letting it peacefully coexist with the traditional (intuitionistic) concept we obtain semantics for an ecumenical logic.The second result, developed in the context of logical bilateralism, shows that the syntactic structure of bases allows us not only to formulate non-interreducible atomic concepts of proof and of refutation, but also to show that syntactic isomorphisms between them have strong semantic bearing, leading to a principle of semantic harmony according to which the proof and refutation conditions of a connective will be harmonic whenever they preserve a fundamental duality already observed at the atomic level. The third, fourth and fifth results, presented in lesser amount of detail, show that there are at least two ways to enrich the notion of proof by making it resource-sensitive to obtain semantics for intuitionistic linear logic; that by promoting a very simple restriction on the quantification over atoms made in the semantic clauses of BeS for the intuitionistic version of a logic we get a semantics for the classical version of that logic and, finally, that if we build a semantics by considering proofs in multi-succedent sequent calculus instead of natural deduction we obtain a very simple, harmonic semantics for classical logic, which is nevertheless sensitive to how structural features of the logic are handled.
Explore our colloquium schedule on our website: uni-tuebingen.de/en/research/centers-and-institutes/carl-friedrich-von-weizsaecker-center/news-and-events/carl-friedrich-von-weizsaecker-colloquium
Recorded as part of the CFvW colloquium on June 18, 2025
On the power and flexibility of base-extension semantics -
Dr. Victor Luis Barroso Nascimento (University College London)
Abstract:
Proof-theoretic semantics (PtS) provides an alternative to model-theoretic semantics by considering proof, not truth, as the basic unit of semantic analysis. This is informed by the philosophical view that our way of engaging with and obtaining knowledge about the world is essentially inferential in nature. Although multiple approaches to PtS are currently being developed, base-extension semantics (BeS) has distinguished itself as one of the most fruitful. In this talk I will present a series of results across multiple contexts with the aim of showing how flexible and powerful BeS is a semantic
framework.
The first result, developed in the context of logical ecumenism, shows that a particular treatment of the absurdity constant allows us to formulate a interesting proof-theoretic concept of classical proof, and by letting it peacefully coexist with the traditional (intuitionistic) concept we obtain semantics for an ecumenical logic.The second result, developed in the context of logical bilateralism, shows that the syntactic structure of bases allows us not only to formulate non-interreducible atomic concepts of proof and of refutation, but also to show that syntactic isomorphisms between them have strong semantic bearing, leading to a principle of semantic harmony according to which the proof and refutation conditions of a connective will be harmonic whenever they preserve a fundamental duality already observed at the atomic level. The third, fourth and fifth results, presented in lesser amount of detail, show that there are at least two ways to enrich the notion of proof by making it resource-sensitive to obtain semantics for intuitionistic linear logic; that by promoting a very simple restriction on the quantification over atoms made in the semantic clauses of BeS for the intuitionistic version of a logic we get a semantics for the classical version of that logic and, finally, that if we build a semantics by considering proofs in multi-succedent sequent calculus instead of natural deduction we obtain a very simple, harmonic semantics for classical logic, which is nevertheless sensitive to how structural features of the logic are handled.
Explore our colloquium schedule on our website: uni-tuebingen.de/en/research/centers-and-institutes/carl-friedrich-von-weizsaecker-center/news-and-events/carl-friedrich-von-weizsaecker-colloquium
