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.

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.

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.

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

${\displaystyle {\frac {}{P}}\qquad {\text{and}}\qquad {\frac {P_{1}\quad \cdots \quad P_{n}}{P}}}$

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 semantic clauses governing the logical constants take the following form, where ${\displaystyle {\mathcal {B}}}$ ranges over bases:⁴⁵

${\displaystyle \Vdash _{\mathcal {B}}P\quad {\text{iff}}\quad \vdash _{\mathcal {B}}P\qquad (P{\text{ atomic}})}$

${\displaystyle \Vdash _{\mathcal {B}}\varphi \wedge \psi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi {\text{ and }}\Vdash _{\mathcal {B}}\psi }$

${\displaystyle \Vdash _{\mathcal {B}}\varphi \to \psi \quad {\text{iff}}\quad \varphi \Vdash _{\mathcal {B}}\psi }$

${\displaystyle \Vdash _{\mathcal {B}}\forall x\,\varphi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi [x\mapsto t]{\text{ for every closed term }}t}$

${\displaystyle \Delta \Vdash _{\mathcal {B}}\varphi \quad {\text{iff}}\quad {\text{for every }}{\mathcal {C}}\supseteq {\mathcal {B}},\ {\text{if }}\Vdash _{\mathcal {C}}\psi {\text{ for all }}\psi \in \Delta ,\ {\text{then }}\Vdash _{\mathcal {C}}\varphi }$

Consequence is then defined by quantification over bases: ${\displaystyle \Gamma \Vdash \varphi }$ just in case ${\displaystyle \Gamma \Vdash _{\mathcal {B}}\varphi }$ for every ${\displaystyle {\mathcal {B}}}$ in the chosen class. The quantification over extensions ${\displaystyle {\mathcal {C}}\supseteq {\mathcal {B}}}$ 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.

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

${\displaystyle \Vdash _{\mathcal {B}}\varphi \vee \psi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi {\text{ or }}\Vdash _{\mathcal {B}}\psi }$

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:

${\displaystyle \Vdash _{\mathcal {B}}\varphi \vee \psi \quad {\text{iff}}\quad {\text{for every }}{\mathcal {C}}\supseteq {\mathcal {B}}{\text{ and every atom }}P,\ {\text{if }}\varphi \Vdash _{\mathcal {C}}P{\text{ and }}\psi \Vdash _{\mathcal {C}}P,\ {\text{then }}\Vdash _{\mathcal {C}}P}$

A parallel clause governs the existential quantifier, and ex falso quodlibet is captured by stipulating that ${\displaystyle \Vdash _{\mathcal {B}}\bot }$ just in case ${\displaystyle \Vdash _{\mathcal {B}}P}$ for every atom ${\displaystyle P}$. 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.⁵

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.

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.

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.¹³

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.

The term proof-theoretic semantics was introduced by Peter Schroeder-Heister, in lectures during the 1980s and in print in 1991.¹⁴¹⁵ Schroeder-Heister has emphasised that the project does not invert the traditional relationship between formal derivability and semantic entailment — soundness and completeness remain desirable features of formal systems — but rather reconstructs the semantic notion of consequence in terms of proofs, where proofs are no longer understood exclusively as formal derivations but as constituting the meanings of the logical constants. Together with Lars Hallnäs, Schroeder-Heister has also developed the notion of definitional reflection, a generalisation of Prawitz's inversion principle to inductively defined predicates that provides a bridge between proof-theoretic semantics and logic programming.¹⁶

The dominant twentieth-century paradigm for the semantics of formal languages was established by Tarski, for whom a formula ${\displaystyle \varphi }$ is a consequence of a set of premises ${\displaystyle \Gamma }$ just in case every model of ${\displaystyle \Gamma }$ is a model of ${\displaystyle \varphi }$.¹⁷ On this conception, consequence is the transmission of truth from premises to conclusion across all admissible interpretations, and the meaning of a connective is given by its truth function. Proof-theoretic semantics offers a different account on three connected points.

Order of explanation. For the model-theorist, truth is conceptually prior to inference: an inference is valid because it preserves truth, and the truth-conditions of a sentence are settled before any question of provability arises. For the proof-theoretic semanticist, inference is conceptually prior to truth: the meaning of a connective is settled by its inferential role, and truth, where it figures at all, is a derivative notion.

Locus of meaning. On the model-theoretic account, the meaning of a logical constant is fixed by its associated semantic clause in a structure — for conjunction, the meet operation on truth values; for the universal quantifier, the universal restriction over a domain. On the proof-theoretic account, meaning is fixed by the inference rules governing the constant: the introduction rules of natural deduction, in Gentzen's reading, or the support clauses of base-extension semantics in the contemporary formulation.

Form of consequence. Although both frameworks define consequence as the preservation of a designated semantic property across a class of structures, the structures in question differ markedly. Model-theoretic consequence quantifies over models — interpretations that assign extensions to non-logical vocabulary; base-extension semantics quantifies over bases — collections of inference rules over the atomic vocabulary. The latter has an evident affinity with Kripke semantics for intuitionistic logic, and indeed the monotonicity condition built into the support relation under base extension is a structural counterpart to the persistence condition on Kripke models. The differences, however, are substantive: bases admit a wider variety of inferential resources than is naturally represented by Kripke frames, and the proof-theoretic framework provides semantics for a range of logics — including various substructural logics — for which standard model-theoretic treatments are either unnatural or unavailable.

The two frameworks are not in straightforward competition. Each has produced characteristically different forms of insight, and the proof-theoretic results that depend on translation into model-theoretic resources — notably Makinson's completeness proof for classical propositional logic — exhibit the productive interplay between them. The distinctive philosophical claim of proof-theoretic semantics is that it can stand on its own resources: that the inferential explanation of meaning is not parasitic on a prior model-theoretic account.

The relation between proof-theoretic semantics and classical logic has been a longstanding source of difficulty, since the introduction-rules-as-definitions thesis is often taken to support intuitionistic principles. Dummett described the reconciliation of classical reasoning with an inferentialist semantics as among the most fundamental problems in the theory of meaning.¹⁸ Sandqvist showed that a fragment of classical predicate logic is sound and complete for base-extension semantics when bases are restricted to rules without discharge,⁸ and Makinson subsequently exhibited a correspondence between bases in Sandqvist's sense and classical valuations.¹⁹ Gheorghiu's first-order result completes this line by establishing completeness for full first-order classical logic by native proof-theoretic means.⁵

Timo Eckhardt and David Pym have developed base-extension semantics for modal logic, in which bases play the role of possible worlds and are connected by an accessibility relation subject to constraints reflecting the partial character of bases as descriptions of states of affairs.²⁰ The framework yields sound and complete semantics for the normal modal logics determined by the axioms K, T, 4, and 5; a subsequent adjustment of the conditions on the accessibility relation yields a sound and complete semantics for S5 and its multi-modal generalisations.

Gheorghiu, Tao Gu, and Pym have adapted the framework to substructural logics, in which the standard structural rules of contraction and weakening are restricted.²¹ The basic idea is to render atomic systems resource-sensitive — permitting the discharge of exactly one occurrence of a hypothesis — and to enrich the support relation with an explicit parameter for atomic resources. The resulting semantics is sound and complete for intuitionistic multiplicative linear logic and, with further additive clauses, for its extension with additive connectives; with a second primitive implication and an accompanying context-former, the construction yields a semantics for the logic of bunched implications.

The Symposium on Proof-Theoretic Semantics is a recurring international meeting devoted to the field, held annually since 2019, and serving as the principal venue for the dissemination of new results. Editions have been hosted at several European institutions and have been associated with related workshops at Schloss Dagstuhl and the Banff International Research Station. Among the developments first announced or substantially discussed at the symposia are Stafford's identification of the Piecha–Schroeder-Heister system with an intermediate logic;²² the axiomatisation of so-called Stafford's Logic, announced jointly with Piecha and Schroeder-Heister; Eckhardt and Pym's semantics for public-announcement logic, affording a treatment of epistemic puzzles such as the muddy children puzzle; and Gheorghiu's first-order result. The series has also been the occasion for discussion of philosophical questions — concerning bilateralism, the identity of proofs, so-called semantic pollution, and molecular versus holistic accounts of inferential meaning — that remain open in the field.

Proof-theoretic semantics is one of several traditions that take inference rather than truth as the fundamental semantic notion. It shares philosophical premises with inferential role semantics in the philosophy of language, with the BHK interpretation in the foundations of intuitionism, and with Martin-Löf's intuitionistic type theory, in which propositions are identified with types and proofs with their inhabitants. It is related, through the Curry–Howard correspondence, to substantial parts of theoretical computer science, including the semantics of functional programming languages and the design of proof assistants.