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? Entries on type theory, model theory, SAT solving and incompleteness link to the matching sections of the free COMP0009 Logic lecture notes.
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 theorem that reduction is confluent: if a term can be run to two different terms, then both can be run on to a common one. It follows that a term has at most one normal form, whatever order its steps are taken in. The course proves it for the combinator calculus by tiling diamonds.
Course notes: COMP0009, Theorem 1.16 · §1.2 Confluence
A function built from application alone, with no variables. In the calculus of Schönfinkel and Curry the two constants K and S suffice: K x y runs to x, and S x y z runs to x z (y z). Combinators are a variable-free model of computation, and the terms that the axioms of a Hilbert system turn out to describe.
Course notes: COMP0009, Chapter 1 §1.1 · Chapter 2 §2.3 Proofs are programs
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.
Course notes: COMP0009, Chapter 6 §6.7 Completeness of NK
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.
Course notes: COMP0009, Chapter 2 §2.3 · Chapter 3 §3.7 Programs as proofs · Chapter 4 §4.5
A question is decidable when some procedure that always terminates answers it correctly for every input. Whether a first-order sentence follows from given hypotheses is undecidable (Church and Turing, 1936): no program answers every instance, although every instance that does follow can be confirmed by searching for a derivation.
Course notes: COMP0009, Chapter 8 §8.1 Computation as a theory
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.
The Davis–Putnam–Logemann–Loveland procedure, the core of SAT solvers: choose a proposition letter, set it true or false, simplify the clauses (unit propagation), and backtrack when a clause is falsified. It decides satisfiability of propositional clause sets; modern solvers extend it with clause learning.
Course notes: COMP0009, Chapter 7 §7.4 DPLL · §7.5 DPLL in practice
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.
See: PtS for First-order Logic
Course notes: COMP0009, Chapter 4 §4.3 Side conditions
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.
A set of sentences Γ entails a sentence A when A is true in every structure in which all the sentences of Γ are true. Entailment is the semantic counterpart of derivability; soundness and completeness say that the two coincide for classical first-order logic.
Course notes: COMP0009, Chapter 6 §6.4 Entailment
The principle that A or not A holds for every A. Classical logic accepts it; intuitionistic logic does not. Adding it to intuitionistic natural deduction (NJ) gives the classical system NK, which is complete for the usual two-valued semantics.
Course notes: COMP0009, Chapter 6 §6.6 Law of the excluded middle · §6.8 Classical and intuitionistic logic
The logic of individuals and their properties: its formulas are built from predicates, functions, equality and the quantifiers ∀ and ∃ ranging over individuals (not over predicates). Its semantics is given by structures, its proofs by natural deduction with quantifier rules and side conditions. It is complete (Gödel) but undecidable (Church and Turing).
Course notes: COMP0009, Chapter 4 §4.1 Predicates and quantifiers · Chapter 6 §6.7 Completeness
The first theorem: a consistent theory that can be listed by a program and is strong enough to express arithmetic leaves some sentence neither provable nor refutable. The second: such a theory cannot prove its own consistency. The course reads them as limits on specification: no finite specification pins down the counting numbers.
Course notes: COMP0009, Chapter 8 §8.3 The first incompleteness theorem · §8.4 The second incompleteness theorem
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.
A set of first-order clauses is unsatisfiable exactly when some finite set of its ground instances (instances with no variables) is unsatisfiable as a propositional problem. It turns first-order search into a sequence of propositional problems that a SAT solver can attempt, and explains why validity can be confirmed but non-validity may never be detected.
Course notes: COMP0009, Chapter 7 §7.7 Herbrand's theorem · §7.8 A procedure for first-order logic
A proof system with many axioms and a single rule, modus ponens. A proof is a list of formulas, each an axiom or following from earlier ones by the rule, so a machine can check it step by step, though proofs are awkward to write by hand. Through the Curry–Howard correspondence a Hilbert proof is a combinator.
Course notes: COMP0009, Chapter 2 §2.1 Formulas, axioms and proofs · §2.3 Proofs are programs
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.
See: An Inferential Semantics for Intuitionistic Logic
Course notes: COMP0009, Chapter 6 §6.8 Classical and intuitionistic logic
A notation for functions in which λx. M is the function sending x to M, applied by substitution. In the simply typed calculus every term has a type, and the types are the formulas of propositional logic: a typing derivation is a natural deduction, and every typed term runs to a normal form.
Course notes: COMP0009, Chapter 3 §3.5 The simply typed λ-calculus · §3.6 Normalisation
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.
Course notes: COMP0009, Chapter 3 §3.1 Derivations in NJ
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.
Course notes: COMP0009, Chapter 3 §3.6 Normalisation
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 set of sentences is satisfiable when some structure makes all of them true. SAT solving is the search for a setting of propositional letters that makes a set of clauses true; the problem is NP-complete, yet modern solvers handle industrial instances with millions of variables. Entailment reduces to it: Γ entails A exactly when Γ together with not A is unsatisfiable.
Course notes: COMP0009, Chapter 7 §7.1 Satisfiability · §7.3 Conjunctive normal form
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.
A way of removing existential quantifiers: each ∃y is replaced by a new function symbol applied to the universally quantified variables before it. The result is satisfiable exactly when the original sentence is, so first-order sentences can be turned into clauses and searched with Herbrand's theorem.
Course notes: COMP0009, Chapter 7 §7.6 From sentences to clauses · §7.9 Prenex and Skolem form
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.
Course notes: COMP0009, Chapter 6 §6.5 Soundness of NJ
The mathematical object that gives a first-order language its meaning: a non-empty domain of individuals together with an interpretation of each constant, function and relation symbol. A sentence is true or false in a structure, and a structure is a model of a theory when it makes every sentence of the theory true.
Course notes: COMP0009, Chapter 6 §6.2 Structures · §6.3 Satisfaction
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.
The calculus of Girard and Reynolds, in which types can be quantified (∀α. T). It is the Curry–Howard counterpart of second-order propositional logic and the theory behind generics in programming languages. Every term runs to a normal form, and a function's type alone yields theorems about it (parametricity).
Course notes: COMP0009, Chapter 5 §5.4 The polymorphic λ-calculus · §5.5 Normalisation and parametricity
A set of sentences that specifies a system: what follows from the specification is what the theory entails. Programs, access policies and arithmetic can all be treated as theories, and asking what a theory can and cannot say is the question that runs through the second half of the COMP0009 notes.
Course notes: COMP0009, Chapter 8 §8.1 Specifications · §8.1 Computation as a theory
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 Interests page.