The Speakers

A Sequent Calculus Perspective on Base-Extension Semantics

We define base-extension semantics (Bes) using atomic systems based on sequent calculus rather than natural deduction. While traditional Bes aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a Bes framework more suited to classical semantics. The harmony in classical sequents leads to straightforward semantic clauses derived solely from right introduction rules.

This framework enables a Sandqvist-style completeness proof that extracts a sequent calculus proof from any valid semantic consequence. Moreover, we show that the inclusion or omission of atomic cut rules meaningfully affects the semantics, yet completeness holds in both cases.

Bilateral base-extension semantics

Bilateralism is the position according to which assertion and rejection are conceptually independent speech acts. Logical bilateralism demands that systems of logic provide conditions for assertion and rejection that are not reducible to each other, which often leads to independent definitions of proof rules (for assertion) and dual proof rules, also called refutation rules (for rejection). Since it provides a critical account of what it means for something to be a proof or a refutation, bilateralism is often studied in the context of proof-theoretic semantics, an approach that aims to elucidate both the meaning of proofs (and refutations) and what kinds of semantics can be given if proofs (and refutations) are considered as basic semantic notions. In this paper we present a bilateral version of base-extension semantics—one of the most widely studied proof-theoretic semantics—by allowing atomic bases to contain both atomic proof rules and atomic refutation rules. The semantics is shown to be sound and complete with respect to the bilateral dual intuitionistic logic 2Int. Structural similarities between atomic proofs and refutations allow us to define duality notions for atomic rules, deductions and bases, which may then be used for the proof of bilateral semantic harmony results. Bilateral semantic harmony is shown to be a restatement of the syntactic horizontal inversion principle, whose meaning-conferring character may now be interpreted as the requirement of preservation of harmony notions already present at the core of the semantics.

From Classical to Linear Logic: One Core, Many Translations

Over the last century, several translations of classical logic into intuitionistic logic have been developed—known as negative translations—including those of Kolmogorov, Gödel, Gentzen, Kuroda, and Krivine. In this talk, we present a framework that systematizes these translations via a notion of modular simplification, starting from Kolmogorov’s translation. This leads to a partial order among the classical-to-intuitionistic translations, clarifying their structural relationships and identifying minimal ones—some previously known, and one new.

Building on this, we turn to translations involving linear logic, such as those introduced by Girard. We show that both these and the earlier negative translations can be captured uniformly by viewing each system as an extension of a core logic—intuitionistic linear logic. This common foundation allows us to formalize a unified approach to devising and simplifying such translations recovering the most well-known translations in the literature.

This is joint work with Paulo Oliva and Clarence Protin.