It seems to me the key point here is that the generalized element characterizations of finite limits (in any category) look just like the usual element characterizations in sets. The elements defined over any object T of an equalizer for parallel arrows f,g:A-->B are exactly those T elements x:T-->A with fx=gx, and the elements defined over T of a product AxB are exactly the pairs <x,y> of one T-element x:T-->A and one y:T-->B. The same does not hold even for colimits let alone quantifiers. Of course when I say the elements "are" these i could as well say they "correspond to" those in the obvious way. That is an issue for precise foundations. Does that seem to you to be the point? Colin On Mon, Jul 10, 2017 at 7:14 PM, David Roberts <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
-- David Roberts http://ncatlab.org/nlab/show/David+Roberts
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]