Models of finite-limit sketches in internal logic of a (pre)topos

[David Roberts <droberts.65537@gmail.com>]

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/ ]