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. Kripke–Joyal forcing is sound and complete for the internal higher-order logic of a topos: a sentence holds in E exactly when it is forced at the terminal stage, and the internal logic is intuitionistic higher-order logic, for which toposes are complete — every such theory has a classifying topos containing a generic model. Special cases recover the known semantics: on a poset with the trivial topology sheaves are presheaves and forcing is Kripke's clauses; on a complete Heyting algebra the result is Ω-valued models, Fourman and Scott (1979). The double-negation topology is the largest dense one and Sh_¬¬(E) is always Boolean; applied to a poset of forcing conditions it reproduces Cohen's independence proofs in the Scott–Solovay Boolean-valued form. Diaconescu (1975) proved internal choice forces Booleanness, so the intuitionism is not optional. Barr's theorem gives every Grothendieck topos a surjection from the sheaves on a complete Boolean algebra. In Sh(X) the Dedekind reals are the sheaf of continuous real-valued functions, and Fourman and Hyland built sheaf models validating Brouwer's continuity principle and bar induction.

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. Truth is stage-relative and there is no global verdict to fall back on: a topos is not in general two-valued, Ω has many elements, and excluded middle fails. Nor can the classical principles be added piecemeal — by Diaconescu's theorem internal choice already implies Boolean, so a sheaf model with choice is a Boolean-valued model and the constructive content is gone. Interpretation is not stable under change of base: inverse image functors preserve only geometric formulas, so →, ∀ and ¬ are not preserved by geometric morphisms and truth transfers along maps of sites for geometric sequents only. Completeness by points fails, since Grothendieck toposes without points exist and only coherent ones are guaranteed points by Deligne's theorem. The forcing relation quantifies over covers and over all stages below U, so it is not effective, and the semantics supplies no proof calculus, no normalization and no complexity bounds.

© 2026 Lingenic LLC