I'm interested in trying to understand the generic model in the classifying topos of a particular coherent theory$^1$, and more specifically trying to sort out what non-coherent formulae hold in said model. While I don't expect there to be a formulaic way to do this, it would be nice to see examples of something similar to orient myself. I may be wishing for something that doesn't exist here, but I am looking for references (of any length) such that:
the reference uses the machinery of classifying toposes
the focus is primarily on a particular coherent or geometric theory (as opposed to treatments in which the theory is an auxiliary device)
they specifically discuss features of the generic model (as opposed to being concerned only with the broad structure of the classifying topos).
Ideally, it does not lean heavily on prior knowledge that the theory is Morita equivalent to some non-syntactic site (though if the reference contains a proof of such an equivalence, that's great).
$^1$ I have omitted mention of the theory because I am confident there will be next to no literature on it (and no obvious non-syntactic site to which it is Morita equivalent). But I can supply it if it would be helpful to answering this question for some reason.
Answer
I hope that this draft of mine, to be finished soon, answers exactly your question. I value any feedback you might have!
Briefly (see Theorem 1.1), a formula holds of the generic model of $\mathbb{T}$ if and only if it is provable in intuitionistic logic from the axioms of $\mathbb{T}$ and the Nullstellensatz, a certain axiom scheme.
This is formulated in the context of geometric theories; the draft also contains a short remark (Scholium 3.14) about the coherent situation. The proof only uses the syntactic site, so fulfills your fourth criterion (and also the other three).
No comments:
Post a Comment