Reference
Plain-language definitions of the central concepts of proof-theoretic semantics and mathematical logic — with links to the explainer pages and research papers that develop each idea in full.
Summary
This glossary collects the recurring vocabulary of proof-theoretic semantics — the programme that takes inference, rather than truth, as the basic concept of meaning. Each entry gives a short, self-contained definition and points to a fuller explainer or to the published research where the concept is put to work. For a narrative introduction, begin with What is proof-theoretic semantics?
A form of proof-theoretic semantics in which a formula counts as valid when it is supported across every extension of a base — a set of inference rules governing atomic statements. Validity is measured not against models, as in truth-conditional semantics, but against all the ways a basic stock of rules might be extended.
See: What is base-extension semantics? · From Basic Proof-theoretic Validity to Base-extension Semantics · PtS for First-order Logic
A substructural logic that places additive and multiplicative connectives side by side, giving two notions of conjunction and implication. BI is the logical basis of separation logic, used to reason about programs that manipulate memory and other resources.
See: PtS for the Logic of Bunched Implications · Semantical Analysis of BI
The property that everything true in the semantics can be proved in the system: if a formula is valid, then it is derivable. Completeness is one half of the bridge between a logic’s proofs and its meanings; the other half is soundness.
The observation that proofs in natural deduction correspond exactly to programs in typed lambda-calculi, and propositions to types. Normalising a proof corresponds to running a program. The correspondence links logic, computation, and the proof theory at the heart of proof-theoretic semantics.
A principle, due to Hallnäs and Schroeder-Heister, which treats the rules that define an atomic statement as exhausting its meaning. Because nothing holds of the atom beyond what the rules establish, one may reason by cases over all the ways it could have been derived.
A fresh variable introduced in the rules for the quantifiers to stand for an arbitrary object about which nothing special is assumed. The freshness condition — that the variable occur nowhere in the surrounding assumptions — is what makes universal reasoning sound.
An inference rule that says what may be drawn from a formula whose main connective is given. The elimination rule for “and”, for instance, lets you pass from “A and B” to either A or B. Its counterpart is the introduction rule.
The requirement that the introduction and elimination rules for a connective be in balance: the eliminations should extract exactly the information the introductions put in — no more, no less. Harmony is a central criterion for whether a connective is meaningful at all.
The view that the meaning of an expression is constituted by its inferential role — the inferences it licenses and the inferences that license it — rather than by an object it denotes. Proof-theoretic semantics is the formal, logical development of inferentialism about the logical constants.
See: What is inferentialism? · Inferentialist Resource Semantics · An Inferential Semantics for Intuitionistic Logic
An inference rule that says under what conditions a formula with a given main connective may be asserted. On Gentzen’s view, the introduction rules define the connective; the elimination rules are then justified as consequences of that definition.
A constructive logic in which to prove a statement is to exhibit a construction for it. The law of excluded middle and proof by contradiction are not generally available. Intuitionistic logic is the historical home of proof-theoretic semantics, and the setting for many of its cleanest results.
A resource-sensitive logic in which each assumption must be used exactly once: premises behave like consumable resources rather than freely repeatable facts. IMLL is a natural testing ground for proof-theoretic semantics beyond the classical and intuitionistic cases.
The dominant, truth-conditional approach to meaning, in which a language is interpreted in abstract structures called models and a sentence’s meaning is the conditions under which it is true. Proof-theoretic semantics is its principal rival: it puts proof, not truth, first.
Contrast: Proof-theoretic semantics
The proof system introduced by Gentzen in which reasoning proceeds by introducing and discharging assumptions, mirroring the way ordinary mathematical arguments are conducted. Its rules come in introduction–elimination pairs, which makes it the natural home of proof-theoretic semantics.
The process of removing detours from a proof — places where a connective is introduced only to be immediately eliminated. A normalised proof is direct, with no such roundtrips. Normalisation is the proof-theoretic counterpart of consistency and underwrites Prawitz’s notion of validity.
The approach to meaning that identifies the meaning of a logical expression with the inference rules governing its use in proofs, rather than with truth conditions or a model. What “and”, “or”, or “if…then” means is fixed entirely by the rules for using it.
See: What is proof-theoretic semantics? · A Survey of Proof-theoretic Semantics
A proof system, also due to Gentzen, that operates on sequents — assertions that some conclusions follow from some assumptions. Its cut-elimination theorem is a landmark result of proof theory and a key tool in proof search.
The property that everything provable in the system is true in the semantics: if a formula is derivable, then it is valid. Soundness guarantees the proof system never proves something meaningless; its partner is completeness.
The basic semantic judgement of base-extension semantics: that a base — possibly together with some assumptions — supports a formula. Support plays the role that satisfaction plays in model-theoretic semantics, but is defined over systems of rules rather than structures.
Prawitz’s notion of a valid argument: one that can be reduced, by removing detours, to a canonical proof ending in an introduction rule. It makes precise the idea that the introduction rules are meaning-giving and everything else must answer to them.
From This Site
For narrative introductions to these ideas, see What is proof-theoretic semantics?, How does logic relate to AI?, and What does a logician do?
To see the concepts at work, browse the Publications, or read the overview of the wider programme on the Research page.