# Proof-Theoretic Semantics

**Origin.** Gentzen's remark (1934–35) that the introduction rules "define" the connectives and the eliminations are consequences of that definition. Prawitz turned it into a programme in *Natural Deduction* (1965) and "Ideas and results in proof theory" (1971); Dummett gave it the philosophical case in *The Logical Basis of Metaphysics* (1991). The term is Schroeder-Heister's (1991); Francez's *Proof-Theoretic Semantics* (2015) is the textbook.

**Models.** Meaning is given by proof conditions, not truth conditions — and the proof conditions are the inference rules. The programme's content is the constraint this puts on which rules count: a connective cannot be introduced by any rules you like, or Prior's tonk defines a connective that collapses the logic. What separates legitimate rules from tonk is harmony, and saying what harmony is has been the subject's central task for fifty years.

**Formalism.**

*The founding problem — Prior's tonk (1960):*
  A ⊢ A tonk B      (introduction, like ∨I)
  A tonk B ⊢ B      (elimination, like ∧E)
Composing them gives A ⊢ B for arbitrary A, B.
The rules are individually unobjectionable and jointly catastrophic.
So rules alone do not confer meaning; some condition on rule-pairs is needed.

*Inversion principle (Prawitz, after Lorenzen):*
Whatever the elimination rule extracts from a formula must already have been
required by its introduction rule. Nothing is got out that was not put in.
The elimination is *determined* by the introduction, not chosen alongside it.

*General elimination (Schroeder-Heister, von Plato):*
Read the introduction rules as a definition and derive the elimination mechanically:
  Γ ⊢ A ∧ B    Δ, A, B ⊢ C
  ─────────────────────────  ∧E_gen
        Γ, Δ ⊢ C
The GE form is the inversion principle made into a schema.

*Harmony:*
Intro and elim are harmonious when the elimination is no stronger than the introduction warrants
and no weaker than it permits. tonk's rules are not: the elimination extracts B, and nothing in
the introduction put B in.
Formalizations: local soundness and completeness (Pfenning–Davies); normalization as the criterion (Prawitz);
conservativity over the connective-free fragment (Belnap 1962, the first answer to Prior).

*Validity of arguments (Prawitz):*
A closed derivation is valid if it reduces to canonical (introduction-ending) form.
An open derivation is valid if every closing instance is.
Consequence is defined by this, not by preservation of truth — the semantics is the reduction relation.

*The classical problem:*
Intuitionistic natural deduction is harmonious.
Classical negation is not: reductio (¬¬A ⊢ A) has no introduction rule to be in harmony with,
and adding it breaks normalization's subformula property.
So the programme, taken straight, argues for intuitionistic logic — which Dummett embraced
and most of its inheritors have tried to escape.

*Bilateralism (Rumfitt 2000, Smiley):*
Take assertion and denial as two primitive forces.
Rules govern +A and −A; classical negation becomes harmonious under the pair.
The escape route from Dummett's conclusion, at the cost of a second speech act.

**Symbols.**

| Symbol | Unicode | Name | Meaning |
|--------|---------|------|---------|
| tonk | — | Prior's connective | The counterexample that started it |
| ⊢ | U+22A2 | Derivability | The semantic primitive here |
| ∧E_gen | — | General elimination | Elimination derived from introduction |
| + / − | — | Assertion / denial | Bilateralism's two forces |
| ⇝ | U+21DD | Reduction | Detour conversion; validity is reducibility |

**Metatheory.** Belnap's 1962 answer to Prior — a connective is legitimate if its rules conservatively extend the logic without it, and uniquely determine it — was the first formal criterion and is still the cleanest, though it makes legitimacy depend on what the logic already had. Harmony formalized as normalization gives intuitionistic logic and not classical, which is the programme's most consequential result and its most contested: Dummett took it as an argument for anti-realism, Rumfitt's bilateralism as a defect in the unilateral framing, and Read's "general-elimination harmony" as a technical fix. The relation to Curry–Howard is exact — the inversion principle is the β-reduction, and harmony is subject reduction — which is why the same programme is the semantics of both proofs and programs.

**Applies to.** The justification of the logical laws. Logical inferentialism and the meaning-is-use tradition. The intuitionism debate, where it is the strongest argument on the anti-realist side. Type theory, where harmony is a design constraint on introduction/elimination pairs. The design of new connectives, where it says what makes one well-defined.

**Limitations.** No agreed definition of harmony after sixty years — conservativity, normalization, local soundness-and-completeness, and general-elimination harmony are inequivalent and each has counterexamples the others miss. The classical result cuts both ways: an argument that the correct logic is intuitionistic is a reductio for most of its audience, and the repairs (bilateralism, multiple conclusions, classical harmony) each buy classicality by changing the framework, which is the move the programme was supposed to forbid. And the programme says nothing about the atomic sentences, so it is a semantics for the connectives resting on a semantics it does not supply.

© 2026 Lingenic LLC