Proof-theoretic semantics

Proof-theoretic semantics is an approach to the meaning of logical constants in which the meaning of a connective is given not by its truth conditions (as in model-theoretic semantics) but by its proof rules — specifically, its introduction and elimination rules in a natural deduction system. The approach originates with Gerhard Gentzen's 1934 work on natural deduction and was developed philosophically by Michael Dummett and Dag Prawitz as a response to verificationism.

The central claim: the meaning of a logical constant is exhausted by its inferential role. To know what negation means is to know what follows from a negation, and what counts as establishing one — not to know what negation corresponds to in some external structure of possible worlds or truth values. This is a radical departure from model-theoretic semantics and aligns proof-theoretic semantics with anti-realism about meaning.

The approach raises acute questions that remain unresolved: Does harmony between introduction and elimination rules guarantee that the meaning of every connective is well-defined? Can classical logic be given a proof-theoretic semantics, or does proof-theoretic semantics necessarily lead to intuitionism? Dummett argued for the latter: if meaning is verification-transcendent, the notion of truth exceeds the evidence available to any finite reasoner, and classical logic is based on a metaphysics we cannot validate. This is either the deepest argument against classical logic or the most instructive illustration of how philosophy of language can produce logical revisionism from premises that seem purely conceptual.