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 -- David Roberts http://ncatlab.org/nlab/show/David+Roberts [For admin and other information see: http://www.mta.ca/~cat-dist/ ]