Some contributions to sheaf model theory
Andreas Brunner, Charles Morgan, Darllan Pinto
TL;DR
The paper develops a rigorous pure sheaf-model-theory framework using a complete Heyting algebra $\Omega$ as truth-values, defining L-structures over presheaves and sheaves, and developing semantic tools such as term realization, forcing, and a rich morphism taxonomy. It proves preservation theorems for forced truths under various morphisms, constructs directed colimits and shows accessibility for categories of presheaves and sheaves of $L$-structures, and establishes density-based presentability results. By situating these categories within Kamsma's AECat framework, the work enables a robust theory of independence relations (isi-dividing, isi-forking, long Kim-dividing) in the sheaf-theoretic setting. Overall, the results unify preservation, amalgamation, and independence in a Fourman–Scott–Higgs-style framework, offering a foundation for neo-stability-type analyses in sheaf-model-theoretic contexts with potential broad applications.
Abstract
This paper makes contributions to "pure" sheaf model theory, the part of model theory in which the models are sheaves over a complete Heyting algebra. We start by outlining the theory in a way we hope is readable for the non-specialist. We then give a careful treatment of the interpretation of terms and formulae. This allows us to prove various preservation results, including strengthenings of the results of Brunner and Miraglia. We give refinements of Miraglia's work on directed colimits and an analogue of Tarski's theorem on the preservation of $\forall_2$-sentences under unions of chains. We next show various categories whose objects are (pairs of) presheaves and sheaves with various notions of morphism are accessible in the category theoretic sense. Together these ingredients allow us ultimately to prove that these categories are encompassed in the AECats framework for independence relations developed by Kamsma.