Some contributions to presheaf model theory, II -- back and forth
Andreas Brunner, Charles Morgan, Darllan Conceição Pinto
TL;DR
The paper adapts back-and-forth arguments to presheaf model theory over a complete Heyting algebra, develops transfinite refinements of partial isomorphisms and Scott-Karp style invariants, and integrates infinitary languages and forcing semantics. It proves a network of equivalences linking partial isomorphism refinements, invariant hierarchies, and Ehrenfeucht-Fraïssé style games, culminating in generalized Karp-type results for presheaves and $L_{\\infty\\lambda}$-structures. It further extends the framework with unnesting and the $L^{\\square}$ language, showing that square connectives, nullary substitutions, and forcing semantics are semantically interchangeable and useful for capturing model similarity at high quantifier ranks. The work unifies multiple hierarchies of model-theoretic similarity in presheaf contexts, providing a robust Fraïssé-type toolkit for intuitionistic truth-value settings and paving the way for new Fraïssé-style results for presheaves. Overall, it offers a comprehensive, transfinite, and algebra-valued extension of classical model-theoretic back-and-forth analysis to presheaves of models.
Abstract
We discuss the back and forth technique in the context of presheaf model theory. The essence of the back and forth technique lies in showing the relationship between various hierarchies which calibrate similarity between two models and, more generally, between two pairs consisting of a model and a tuple from it. In this paper we define several such hierarchies for presheaf models (and tuples of sections from them): those based on the degree of extendibility of partial isomorphisms through literal back and forth conditions, on sharing specific, abstract invariants which we define (the $F^α_{M,\bar{a}}$ of §\ref{function_analysis} for example), on agreeing on the (truth) values of instantiations of formulae up to a given amount of quantifier completity, on the existence of winning strategies for player II in certain Ehrenfeucht-Fraïssé-type games and, finally, on satisfying certain infinitary sentences that arise in the construction of Scott sentences. We ultimately show that all of these hierarchies align.