Bases
A base is a set of inference rules over atomic sentences: rules that conclude an atom outright, or conclude an atom from others, sometimes under discharged assumptions. Bases take the place of models, but are made of rules rather than objects.
Summary
Base-extension semantics (B-eS) is a form of proof-theoretic semantics in which the validity of a formula is defined relative to bases — sets of inference rules governing atomic sentences — rather than relative to models. A formula counts as valid when it is supported in every extension of every base. Introduced by Tor Sandqvist to present classical logic without assuming bivalence, the framework has been extended by Gheorghiu and collaborators to first-order, linear, bunched, and arithmetical settings.
The core idea
In model-theoretic semantics, a logical language is interpreted in abstract structures called models, and a formula $\phi$ follows from assumptions $\Gamma$ when every model of $\Gamma$ is a model of $\phi$. Truth in a structure is the basic notion, and consequence is truth-preservation.
Base-extension semantics replaces models with bases. A base $\mathcal{B}$ is a set of inference rules over atomic sentences — the simplest statements of the language, without logical structure. In place of truth-in-a-model, B-eS uses a support relation, written ${\Vdash}_{\mathcal{B}}$, read “the base $\mathcal{B}$ supports…”. The meaning of each logical connective is then given by a clause explaining what it takes for a base to support a formula built with that connective.
The defining move is quantification over base extensions. A formula is valid when it is supported no matter how the base is extended with further atomic rules:
$\Gamma \Vdash \phi$ iff for every base $\mathcal{B}$, if ${\Vdash}_{\mathcal{B}}\,\psi$ for all $\psi \in \Gamma$, then ${\Vdash}_{\mathcal{B}}\,\phi$.
Validity is thus robustness across all the ways a basic stock of inferential commitments might be filled in — an account of consequence grounded in inference rather than in reference to objects.
Key concepts
The support relation
Support, ${\Vdash}_{\mathcal{B}}$, is the basic semantic judgement: that a base — possibly together with assumptions — supports a formula. It plays the role satisfaction plays in model-theoretic semantics, but is defined over systems of rules.
Extension and monotonicity
One base extends another by adding atomic rules. Validity quantifies over all extensions, which builds a Kripke-like monotonicity into the semantics: what a base supports, its extensions continue to support. This is what makes the account well-behaved for intuitionistic logic.
Completeness by simulation
Completeness is typically proved not by constructing a canonical model but by simulating a formal derivation inside a base tailored to the inference. The technique is elementary — it avoids canonical models, König’s lemma, and bar induction — and reveals how inferential content drives the semantics.
Bivalence-free classical logic
A striking feature of the framework is that it can present classical logic without presupposing that every sentence is either true or false. This makes B-eS attractive to those who doubt that meaning rests on a two-valued notion of truth.
How this research develops the framework
Base-extension semantics was introduced by Tor Sandqvist, building on the proof-theoretic validity of Michael Dummett and Dag Prawitz. Gheorghiu’s research extends and clarifies the framework across several logics:
Foundations. From Basic Proof-theoretic Validity to Base-extension Semantics connects Dummett and Prawitz’s basic validity to B-eS for intuitionistic propositional logic, and An Inferential Semantics for Intuitionistic Sentential Logic relates the semantics to Mints’ resolution method, recovering soundness and completeness as corollaries.
First-order logic. Proof-theoretic Semantics for First-order Logic (Logic Journal of the IGPL, 2025) gives an elementary, constructive, and native proof of soundness and completeness for the B-eS of classical and intuitionistic first-order logic.
Substructural logics. Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic and Proof-theoretic Semantics for the Logic of Bunched Implications extend the framework to resource-sensitive settings, where assumptions behave like consumable resources.
Arithmetic. Truth, Support, and Arithmetic uses the support relation to give a precise reading of Gödel’s second incompleteness theorem. For an overview of the whole programme, see A Survey of Proof-theoretic Semantics.
Why it matters
Philosophy of logic. B-eS gives a rigorous, completeness-bearing semantics for the inferentialist idea that meaning is grounded in rules of inference rather than in reference — and it does so even for classical logic, without assuming bivalence.
Substructural and resource reasoning. Because bases are systems of rules, the framework adapts naturally to logics where assumptions are used a limited number of times, connecting proof-theoretic meaning to reasoning about resources.
Artificial intelligence. A semantics built from inference rules makes the structure of valid reasoning explicit and checkable — relevant to the question of when a system genuinely reasons rather than merely predicts. See How does logic relate to AI?
Common Questions
Frequently asked
How does base-extension semantics differ from possible-world semantics?
They are closely related: quantifying over base extensions resembles quantifying over accessible worlds, and both yield a monotone, intuitionistically well-behaved semantics. The difference is what the points are. In Kripke semantics they are worlds at which atoms are simply true or false; in base-extension semantics they are bases — systems of inference rules — so meaning is tied to inference rather than to assignments of truth.
Why does completeness avoid canonical models?
Because the semantics is about rules, completeness can be shown by simulating a derivation inside a carefully chosen base rather than by assembling a maximal consistent set into a model. This simulation method is mathematically elementary and makes transparent how the inferential content of the logic is recovered from the semantics.
Which logics have a base-extension semantics?
Classical and intuitionistic propositional and first-order logic, intuitionistic multiplicative linear logic, and the logic of bunched implications all have base-extension semantics, and the programme continues to expand — for instance to modal and arithmetical settings. The relevant papers are linked above.
From This Site
Related pages
Base-extension semantics is one strand of proof-theoretic semantics, the broader programme that takes inference rather than truth as basic. For the philosophical position underlying it, see What is inferentialism?
For precise definitions of the key terms — base, support, completeness, and the rest — see the Glossary; for the full body of research, see the Publications page.