Dear David, I feel I may have something to say here, but I don't fully understand the question or the language of forcing. Is it about whether the sketch should be internal or external? Or is it about whether the internal logic matches the external category theory? Can you state your conjecture in more detail? Whether or not it answers your question, here's a plug for my own recent work on sketches and pretoposes: Sketches for arithmetic universes Arithmetic universes and classifying toposes The sketches are more general than finite limit. They include colimits and list objects, and are intended as an approximation to geometric theories. The pretoposes (where the models live) are arithmetic universes, which have parametrized list objects. In the elementary topos case this is equivalent to assuming an nno. Regards, Steve. On 11/07/2017 00:14, droberts.65537@gmail.com wrote:
Hi all,
I believe that if one has some finite limit sketch S, then models of S in the internal logic of a topos E should be equivalent to external models. I'm thinking here about forcing from the sheaf-theoretic viewpoint, so that some algebraic gizmo in the forced model(=in internal logic of the topos) is none other than that algebraic gizmo internal to the category from the external perspective. Or, that a model in some filterquotient E/~ of a topos E is equivalent to a model in E.
Is there a reference I could point to? Or is it obvious because a finite-limit sketch uses no quantifiers etc? I would guess such reasoning to hold in a much more general setting than a topos, for instance pretoposes or regular categories.
A second question, that I do not know the answer to: how far can one generalise theories (from finite-limit etc) and still get {models in internal logic} ~ {models in the category}? Here "the category" has sufficient structure to interpret the theory.
Thanks, David
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]