Categorical Proof-Theoretic Semantics
David Pym, Eike Ritter, Edmund Robinson
TL;DR
This work unifies proof-theoretic semantics with category theory by recasting Sandqvist's base-extension semantics for intuitionistic propositional logic in a presheaf topos. It shows how atoms, connectives, and especially disjunction can be interpreted categorically using products, exponentials, and a second-order elimination-based construction, with natural transformations capturing validity. The main results establish soundness and completeness of the NJ system with respect to this categorical model, clarifying the role of disjunction and its interpretation. The approach highlights a deep link between proof theory and categorical logic, connecting base-extension semantics, Kripke/presheaf models, and sheaf-theoretic perspectives. The framework provides a proof-relevant semantic account that preserves justification-structures while aligning with standard intuitionistic metatheory.
Abstract
In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic (IPL) raises some technical and conceptual issues. We relate Sandqvist's (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist's constructions. This naturality includes Sandqvist's treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist's semantics can also be viewed as the natural disjunction in a category of sheaves.