Foundational Questions
An introduction to the view that the meaning of logical expressions is determined by inference rules governing their use in proofs — not by truth conditions or reference to a model.
Summary
Proof-theoretic semantics is an approach to meaning in logic and philosophy that identifies the meaning of a logical expression with the inference rules governing its use in proofs, rather than with truth conditions or a set-theoretic model. The programme holds that what a logical constant — such as “and,” “or,” or “if…then” — means is fixed entirely by the rules that permit its introduction and elimination within a system of proof. The field is associated with Gerhard Gentzen, Michael Dummett, and Dag Prawitz, and remains an active area of research in mathematical logic and the philosophy of language.
The dominant tradition in the philosophy of language, following Frege and Tarski, takes truth conditions as fundamental: to understand a sentence is to know under what circumstances it would be true. Proof-theoretic semantics challenges this at its root.
The alternative proposal is that meaning is determined by use in inference. What it means to say “A and B” is given not by any model or truth-maker, but by the rules: you may assert “A and B” if you can assert both “A” and “B” separately, and from “A and B” you may derive either conjunct. These introduction and elimination rules, taken together, constitute the meaning of conjunction.
More broadly, the meaning of any logical expression is exhausted by its inferential role: the patterns of reasoning it supports. This is sometimes called inferentialism about logical constants, and proof-theoretic semantics provides its formal development.
An inference rule specifies a transition: given certain premises, a certain conclusion may be drawn. In natural deduction, rules come in pairs — an introduction rule, which explains when a connective may be asserted, and an elimination rule, which explains what follows from it.
The proof system developed by Gentzen in which reasoning proceeds by introducing and discharging assumptions. Natural deduction is the standard framework for proof-theoretic semantics, because its structure mirrors ordinary mathematical and deductive reasoning.
A logical connective is harmonious if its introduction rules and elimination rules are in balance: the elimination rules extract precisely the information the introduction rules put in, neither more nor less. Harmony is a formal criterion for the coherence of a logical system, analogous to consistency in model-theoretic terms.
A proof that introduces a connective only to immediately eliminate it contains a detour. Normalisation theorems establish that such detours can always be removed, yielding a direct proof. This is the proof-theoretic counterpart of semantic consistency.
A framework developed to give a rigorous semantics for systems of inference, defining what it means for a proof to be valid across all possible extensions of an atomic base — a set of rules for atomic statements. This provides proof-theoretic semantics with a formal completeness theory.
The formal tools of proof-theoretic semantics originate with Gerhard Gentzen, whose 1935 papers introduced natural deduction and the sequent calculus. Gentzen observed that the meaning of a logical constant is determined by its introduction rules, a remark that would later become the cornerstone of the semantic programme.
Michael Dummett gave the idea its philosophical grounding in the 1970s, arguing that a theory of meaning for a language must be manifested in the use speakers make of that language — in their inferential practice — rather than in the grasp of abstract truth conditions. This led him to advocate for intuitionistic logic as the logically revisionary consequence of a meaning-theoretic approach.
Dag Prawitz developed the mathematical theory in parallel, establishing the connection between proof normalisation and semantic validity, and formulating the first precise version of proof-theoretic validity.
Contemporary work extends the programme to classical logic, first-order logic, modal and substructural logics, and applies its concepts to questions in the philosophy of language, philosophy of mathematics, and the foundations of artificial intelligence.
Philosophy of logic. Proof-theoretic semantics offers an account of logical consequence that is independent of set-theoretic models, making it attractive to those who are sceptical of platonism about mathematical objects. It provides a criterion — harmony — for distinguishing well-formed from ill-formed logical systems.
Philosophy of mathematics. If meaning is constituted by proof, then mathematical existence becomes a question of what can be constructed and demonstrated, not what inhabits a Platonic realm. This connects proof-theoretic semantics to constructivism and intuitionism in the foundations of mathematics.
Philosophy of language. By grounding meaning in inferential practice, the framework offers an alternative to both truth-conditional and use-theoretic approaches that is formally precise and amenable to mathematical study.
Artificial intelligence. A system that reasons, rather than merely predicts, must be able to trace its outputs back to principled inferential steps. Proof-theoretic semantics provides formal criteria for this distinction: whether an AI system's conclusions are genuinely inferential or statistically approximate. This is increasingly urgent as AI systems are deployed in contexts requiring genuine accountability.
Common Questions
They are closely related but not identical. Inferentialism, in the tradition of Robert Brandom, is a broad philosophical position about the nature of meaning and conceptual content. Proof-theoretic semantics is the specific mathematical development of inferential ideas within formal logic, providing precise definitions and theorems. One can be an inferentialist without working in proof-theoretic semantics, and vice versa.
Historically, many practitioners argued that the approach favoured intuitionistic logic, since classical logic’s connectives proved resistant to harmonious formulation. Contemporary research — including Gheorghiu’s work — has developed proof-theoretic semantics for classical logic, showing that the commitment to inferentialism need not entail logical revisionism.
Proof theory is the mathematical study of formal proofs — their structure, transformations, and complexity. Proof-theoretic semantics uses the tools of proof theory to address semantic questions: what expressions mean, what makes an argument valid, what constitutes a logical consequence. Proof theory is a mathematical discipline; proof-theoretic semantics is a philosophical one, albeit a formally rigorous one.
The Curry–Howard correspondence is an observation that proofs in natural deduction correspond to programs in typed lambda-calculi, and propositions correspond to types. Proof-theoretic semantics draws on similar structural observations about proofs but pursues semantic rather than computational conclusions. The correspondence is a productive technical tool for the field, particularly in work on the computational content of proofs.
From This Site
Gheorghiu’s published research applies and extends proof-theoretic semantics across several logics. See the Publications page for papers on classical, intuitionistic, first-order, and substructural proof-theoretic semantics.
For the connection to artificial intelligence, see How does logic relate to AI?
For an overview of how this work fits into a broader research programme, see the Research page.