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

[Colin McLarty <colin.mclarty@case.edu>]

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