From Basic Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
From MaRDI portal
Abstract: 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.
This page was built for publication: From Basic Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6506762)
