Proof-theoretic semantics

Proof-theoretic semantics is a branch of proof theory and an approach to the semantics of logic in which the meaning of propositions and logical connectives is explained by the role they play within a system of inference. On this view, a proof is not merely a device for establishing that a sentence holds under some prior assignment of meaning; rather, the patterns of correct inference are themselves constitutive of what the logical vocabulary means. The position has both philosophical and technical aspects. Philosophically, it stands in a tradition that takes the proper subject matter of logic to be the relation of logical consequence rather than truth, and that treats meaning as a function of inferential role. Technically, it has been developed through the analysis of Gerhard Gentzen's natural deduction and sequent calculus, through the Brouwer–Heyting–Kolmogorov interpretation of the intuitionistic connectives, and, in its contemporary form, through a family of formal semantics — chief among them base-extension semantics — in which the validity of inferences is defined by reference to provability in systems of atomic rules.

The framework originates in remarks by Gentzen suggesting that the introduction rules of a logical connective provide its definition, while the elimination rules are answerable to those definitions. The technical development of this thought, beginning with Dag Prawitz's work on natural deduction and continuing through Michael Dummett's account of logical harmony and the formal semantics introduced by Peter Schroeder-Heister and Tor Sandqvist, has produced a substantive alternative to the model-theoretic tradition descending from Alfred Tarski. The most recent developments include sound and complete base-extension semantics for first-order classical and intuitionistic logic, established by elementary and constructive means without recourse to truth-functional interpretation, as well as extensions to modal logic and several substructural logics.