From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
Alexander V. Gheorghiu, David J. Pym
TL;DR
This work bridges proof-theoretic validity (P-tV) and base-extension semantics (BeS) for intuitionistic propositional logic (IPL) by focusing on an elimination-rule–based P-tV and embedding it within Sandqvist’s BeS. Under carefully specified reductions and base conditions (i.e., supportive reductions and Sandqvist bases), the paper proves that entailment in P-tV and BeS coincide, providing a complete, constructive reading of IPL’s connectives. It discusses constructivity, the role of disjunction, and the status of ex falso quodlibet (EFQ), arguing that EFQ can be treated as a definitional principle within this framework. The results illuminate a coherent, operational correspondence between proofs (arguments) and semantic support, and they point toward extensions to other logics and to classical contexts.
Abstract
Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on 'proof' (as opposed to 'truth'). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of logical constants. This paper demonstrates that the B-eS for intuitionistic propositional logic (IPL) encapsulates the declarative content of a version of P-tV based on the elimination rules. This explicates how the B-eS for IPL works, and shows the completeness of this version of P-tV.