From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic

Alexander V. Gheorghiu, David J. Pym

There are two major approaches to proof-theoretic semantics: proof-theor\-etic validity (P-tV) and base(-extension) semantics (B-eS). In this paper, we show that for intuitionistic propositional logic (IPL) the latter may be understood as capturing the declarative content of the former, which proceeds operationally on proofs. In so doing we expose a central problem around negation in proof-theoretic semantics -- viz. the semantic content of \emph{ex falso quodlibet} for IPL. In P-tV, the rule follows as a vacuous implication from the rejection of valid arguments for absurdity, but by augmenting the notion of \emph{base} underpinning proof-theoretic semantics one may use the rule to define absurdity (i.e., absurdity follows when all things are valid). This analysis clarifies the connexions between the two major approaches to proof-theoretic semantics and gives insight into what some mathematical requirements are in general for such semantics.

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment