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.

Philosophical motivation

The conception of meaning at the heart of proof-theoretic semantics is most easily made vivid by an everyday example. Asked what Tammy is a vixen means, one does not ordinarily produce a set of objects together with the assignment of an extension to the predicate; one says, rather, that to call Tammy a vixen is to commit oneself to her being female and being a fox, and to grant in return the inference that anyone who is both is a vixen. The contention of the proof-theoretic semanticist is that the same pattern of explanation can be made precise for the logical vocabulary, and that doing so yields a semantics with at least as much technical substance as any alternative.

The thesis has a long philosophical pedigree. The view that meaning is given by inferential role — sometimes called inferentialism, following Robert Brandom — has been traced through Wilfrid Sellars to the Begriffsschrift of Gottlob Frege. Dummett gave the position its most sustained articulation in the philosophy of language, on which a theory of meaning must explain what it is to understand an expression, and to understand an expression is to be capable of using it correctly — competence with the inferences governing a logical constant being constitutive of grasp of its meaning. Proof-theoretic semantics is, in effect, the working out of this conception in the formal setting of symbolic logic.

Base-extension semantics

The principal contemporary framework for proof-theoretic semantics is base-extension semantics. It defines the meaning of the logical constants not in terms of truth in a model but in terms of a support relation between collections of inference rules and formulas.

Atomic systems and bases

An atomic system is a finite or infinite collection of rules over a stock of atomic (non-logical) sentences. Two forms of rule are typically admitted: zero-premise rules of the form

together with, in some settings, rules involving discharge of atomic assumptions. An atomic system represents what one might call a system of inferential commitments concerning the atomic vocabulary, antecedent to any commitment about the logical constants. A basis is a class of admissible atomic systems; different choices of basis correspond, as it will turn out, to different logics.

The support relation

The semantic clauses governing the logical constants take the following form, where ranges over bases:

Consequence is then defined by quantification over bases: just in case for every in the chosen class. The quantification over extensions in the clauses for inference is a structural counterpart to the monotonicity built into Kripke semantics for intuitionistic logic, and ensures that consequence is preserved as new atomic rules are added.

Disjunction, existence, and absurdity

The clauses for disjunction, existence, and absurdity merit separate comment, since the most natural readings of these connectives turn out not to characterise intuitionistic logic. The reading

validates the Kreisel–Putnam axiom, a schema admissible but not derivable in intuitionistic propositional calculus; the resulting logic has been identified by Will Stafford as a variant of inquisitive logic. Sandqvist accordingly proposed an alternative clause modelled on the second-order definition of disjunction familiar from System F and from Prawitz's thesis:

A parallel clause governs the existential quantifier, and ex falso quodlibet is captured by stipulating that just in case for every atom . Under these clauses, the choice of admissible bases — whether the basis admits rules with discharge of hypotheses, and at what level — determines which logic is captured by the support relation.

Soundness and completeness

Sandqvist showed that intuitionistic propositional logic is sound and complete for the support relation when the basis admits rules with discharge of atomic assumptions, and that classical logic restricted to implication, absurdity, and the universal quantifier is sound and complete when the basis is restricted to rules without discharge.

The full first-order case — both classical and intuitionistic — was settled by Alexander V. Gheorghiu in 2025, who established sound and complete base-extension semantics for first-order logic in both varieties, by elementary, constructive, and proof-theoretically native means. The result is significant on several counts. It treats the two logics within a uniform framework, differing only in the admissible basis. It dispenses with the bar-induction techniques required by Sandqvist's earlier classical proof. And, unlike David Makinson's earlier completeness proof for classical propositional logic — which reduced the question to truth-functional semantics by exhibiting a correspondence between bases and classical valuations — it establishes completeness without appeal to the model-theoretic reading of classical logic, thereby exhibiting the inferential resources of the framework on their own terms.

The proof proceeds by a simulation technique, originally due to Sandqvist for the propositional intuitionistic case and substantially extended for the first-order classical setting. Given a candidate consequence, one constructs a base whose atomic rules mimic the introduction and elimination steps of a Hilbert system over the subformulas of the formulas in question; supplementary devices, including the use of eigenvariables drawn from a reserved pool of constants, handle the simulation of quantifier rules and open formulas. From a putative proof of validity, one extracts a derivation in the corresponding axiomatic calculus.

The reduction of the difference between classical and intuitionistic first-order logic to a difference in the admissible basis is one of the more striking features of the framework. The semantic clauses for the connectives are identical in the two cases; the logical character of consequence is fixed entirely at the pre-logical level, by the inferential resources of the atomic systems themselves.

Historical development

Gentzen

Gerhard Gentzen's 1934–35 dissertation, Untersuchungen über das logische Schließen (Investigations into Logical Deduction), introduced natural deduction and the sequent calculus and established the cut-elimination theorem for the latter. In a passage that has shaped subsequent reflection, Gentzen remarked that the introduction rules of a connective represent "as it were, the definitions of the symbols concerned", while the elimination rules are "no more, in the final analysis, than the consequences of these definitions". The thesis that the introduction rules fix meaning and the elimination rules are answerable to them is the seed from which proof-theoretic semantics has grown.

Prawitz and the validity of arguments

The first attempt to develop a semantic theory along Gentzen's lines is due to Dag Prawitz, whose Natural Deduction: A Proof-Theoretical Study (1965) proved a normalization theorem: every derivation in intuitionistic natural deduction reduces to a normal form in which no formula is first introduced and then immediately eliminated. A corollary is that every closed derivation reduces to one whose final step is an introduction rule, a result that lies at the heart of the Curry–Howard correspondence and of intuitionistic type theory.

In Ideas and Results in Proof Theory (1971), Prawitz proposed a notion of validity for arguments — trees of formulas constructed using inference steps that need not themselves be rules of any given formal system — defined relative to a fixed system of atomic rules and a class of admissible reduction operations. Prawitz conjectured that intuitionistic natural deduction is complete with respect to this notion: every valid argument can be replicated as a derivation in the system. The conjecture was subsequently refuted by Piecha, de Campos Sanz, and Schroeder-Heister, who showed that the most direct formal articulation of Prawitz's idea yields a logic strictly stronger than intuitionistic logic. The relationship between proof-theoretic validity in Prawitz's sense and the base-extension semantics now generally used has been studied by Alexander V. Gheorghiu and David Pym, who identify conditions under which the two coincide.

Dummett and harmony

Michael Dummett developed the philosophical implications of the Gentzen–Prawitz programme over several decades, culminating in The Logical Basis of Metaphysics. Building on a suggestion of Nuel Belnap arising from the case of the connective tonk, Dummett introduced the notion of logical harmony: a system of inferential rules is in harmony when it is always possible to recover analytic proofs from arbitrary demonstrations, as guaranteed for the sequent calculus by cut-elimination and for natural deduction by normalization. A language lacking harmony admits incoherent forms of inference and is liable to inconsistency. Dummett took the framework to support an anti-realist conception of meaning on which the meaning of a statement is given by its assertibility conditions rather than its truth conditions, and argued — at length, and not without controversy — that the resulting position naturally supports intuitionistic rather than classical principles.

Schroeder-Heister and the naming of the field