Sheaf Semantics

Origin. Grothendieck's sites and sheaves (SGA4, 1963–64, published 1972) supplied the machinery; Lawvere and Tierney's elementary topos (1970) made it logic. Kripke–Joyal forcing is Joyal's reformulation of Kripke's semantics inside a topos; Fourman and Scott, "Sheaves and logic" (1979), and Fourman and Hyland's sheaf models of intuitionistic analysis (1979) are where the model theory was built. Van Dalen and Troelstra's Constructivism in Mathematics (1988) is the standard exposition.

Models. A sheaf is a way of specifying something locally and asking whether the local data glue. Reading logic into that: a formula's truth is not a global verdict but a set of stages at which it holds, and it holds at a stage iff it holds on a cover of that stage. The internal logic that results is intuitionistic, not by stipulation but because "holds on a cover" does not satisfy excluded middle — a formula and its negation can each fail to hold on any cover.

Formalism.

Site: A category C with a Grothendieck topology J: for each object U, a set of covering sieves, closed under pullback, containing the maximal sieve, and transitive. A cover is what counts as "enough local pieces".

Sheaf: A presheaf F : C^op → Set satisfying descent: for every covering sieve S on U, matching families of sections over S glue uniquely to a section over U. Sh(C, J) is the category of sheaves — a Grothendieck topos.

Kripke–Joyal forcing: For a topos E and a formula φ with parameters at stage U: U ⊩ φ ∧ ψ iff U ⊩ φ and U ⊩ ψ U ⊩ φ ∨ ψ iff a cover {Uᵢ → U} with each Uᵢ ⊩ φ or Uᵢ ⊩ ψ U ⊩ φ → ψ iff for all V → U, V ⊩ φ implies V ⊩ ψ U ⊩ ∃x φ(x) iff a cover {Uᵢ → U} and aᵢ ∈ F(Uᵢ) with Uᵢ ⊩ φ(aᵢ) U ⊩ ∀x φ(x) iff for all V → U and a ∈ F(V), V ⊩ φ(a) The disjunction and existential clauses are where classicality dies: a cover may split.

Kripke semantics as the special case: Take C a poset, J trivial (only the maximal sieve covers). Sheaves = presheaves = Kripke models. Intuitionistic Kripke semantics is sheaf semantics on a site with no covers.

Boolean-valued models and forcing: Cohen forcing is sheaf semantics on the double-negation topology of a poset of conditions. Sh_¬¬(P) is Boolean; the internal logic is classical; the model is V^B. Independence proofs are sheaf constructions, which is how set theory and topos theory met.

Sheaf models of analysis: Fourman–Hyland: sheaves on ℝ give models of intuitionistic analysis where every function is continuous. Brouwer's continuity theorem is a theorem about a topos, not a stipulation.

Symbols.

Metatheory. That Kripke semantics, Beth semantics, Boolean-valued models, and realizability are all sheaf or presheaf semantics over different sites is the unification the subject exists for — four constructions invented separately for different purposes, and one theorem behind them. The double-negation topology is the mechanism: it makes any topos Boolean, and applying it to a forcing poset is Cohen's method, so independence in set theory and the internal logic of a topos are the same subject. The Fourman–Hyland models settle a foundational question empirically: intuitionistic analysis is not a restriction of classical analysis but the analysis of a different universe, in which all functions are continuous because the sheaf condition makes them so.

Applies to. Topos-theoretic semantics for intuitionistic logic and type theory. Independence results, via Boolean-valued models. Constructive analysis and its models. Higher-order logic in a topos. Algebraic geometry, where the same machinery does its original work.

Limitations. The apparatus is heavy for what it delivers to a logician: Grothendieck topologies, sites, and descent are a large investment to recover Kripke semantics, which needs none of them. The internal logic is intuitionistic and higher-order, so first-order questions must be asked awkwardly. And sheaf semantics gives models rather than proof theory — it explains why intuitionistic logic is sound for these structures and supplies no calculus, which is why the topos-theoretic and the proof-theoretic accounts of constructivism have never fully merged.

© 2026 Lingenic LLC