On an Inferential Semantics for Intuitionistic Sentential Logic
Alexander V. Gheorghiu
TL;DR
The paper addresses how to semantically ground intuitionistic propositional logic via a proof-theoretic, rather than model-theoretic, lens. It shows that Sandqvist's base-extension semantics ($B\text{-}eS$) is intimately connected to Mints' resolution-based clausal methods, and that the classical results of soundness and completeness for $B\text{-}eS$ follow from Mints' theorem. By translating subformulas to basic sentences with $(-)^{\flat}$ and encoding them as a clausal system $\mathcal{M}_{\mathbb{X}}$, the authors establish a precise equivalence between base-derivability and clause-derivability, ultimately proving $\Vdash \varphi$ iff $\vdash \varphi$. The work reinforces that proof-search is not merely algorithmic but captures the inferential content of constructive reasoning, offering a bridge between proof-theoretic semantics and resolution methods with potential links to logic programming and broader semantic frameworks.
Abstract
Sandqvist's base-extension semantics (B-eS) for intuitionistic sentential logic grounds meaning relative to bases (rather than, say, models), which are arbitrary sets of permitted inferences over sentences. While his soundness proof is standard, his completeness proof, is quite unusual. It closely parallels a method introduced much earlier by Mints, who developed a resolution-based approach to intuitionistic logic using a systematic translation of formulas into sentential counterparts. In this short note, we highlight the connection between these two approaches and show that the soundness and completeness of B-eS follow directly from Mints' theorem. While the result is modest, it reinforces the relevance of proof-search to proof-theoretic semantics and suggests that resolution methods have a deeper conceptual role in constructive reasoning than is often acknowledged.