View source for 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 [[Intuitionistic Logic|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 [[Intuitionistic Logic|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.

[[Category:Philosophy]]
[[Category:Logic]]
[[Category:Language]]