It is well-known that one can have models of any finite-limit theory (say) in any finitely complete category. However, one could be silly and rewrite that theory using things like quantifiers instead of functions: instead of specifying some in the theory one could write where it goes on to specify that this encodes a function. This can then be interpreted in the usual internal logic of a topos via Kripke–Joyal (or stack) semantics.

The resulting model looks a lot different a priori from the model of the finite-limit theory. However, I expect that these should be equivalent somehow (say the categories of models are equivalent). One could phrase this in terms of the extension of the doctrine from finite-limit theories (or whatever fragment one wants: equational, regular, coherent, etc) all the way up to full higher-order logic, and that interpreting the simpler fragment in equivalent ways in the larger fragment leads to something equivalent, no matter how it is convoluted by the richer vocabulary of the larger fragment.

I was wondering if there is anything on this in the literature? Or if it is easy to see? I am only working on instinct.

Hi, correct me if I'm wrong but I think what's going on here is two theories are Morita equivalent (see TST, pg. 59), at least when restricted to models in Grothendieck topoi.

If and are, respectively, the finite-limit theory and its higher-order counterpart and indeed the models in every topos are equivalent, then we have a chain of equivalences , where and are the classifying topoi. Taking corresponding to , and similarly , we get two functors witnessing an equivalence .

I know almost nothing about categorical model theory but isn't trading a function for a a form of 'de-Skolemization'? Skolemization is the inverse process, if I recall correctly, where an existential axiom is traded for an explicit witness.

I don't know where to go from here but since Skolemization is a pretty famous construction, it could be a good keyword for your searches.

It also points out a potential breaking point of the naive reasoning whereby every can be turned into a function, since this smells a lot like AC and some topoi do not have it.

@jwrigley I'm not assuming that the categories of models are equivalent, but am asking if that is the case. Or if anything similar can be shown/is known.

@matteocapucci good point. But I'm not just de-Skolemizing, but asking for *unique* existence. I guess there might be a setting where even a functional, total relation might not come from an actual arrow, but this smells like predicative mathematics, and probably not an issue in a topos.

Consider for instance the definition of a group: one could write it in terms of quantifiers and so on, rather than as an equational theory. The multiplication operation should not just be a vanilla . The identity and inverse are of course not specified uniquely, but they can be proved to be unique, so that's not a problem.

The classifying topos for a given theory in a "sub-geometric" fragment of logic is a category of sheaves on the corresponding syntactic category for the theory in that fragment. For a regular theory, for example, we construct the syntactic (regular) category as a category of regular formulas-in-context. But we get an equivalent classifying topos for the theory whether we take the regular, coherent, or geometric (pretopos) syntactic categories. This is a consequence of the fact that geometric morphisms necessarily preserve all of the constructions which interpret geometric logic.

However, this is not the case for higher order logic: there are geometric morphisms whose inverse image functors do not preserve power objects or exponentials, or which do not commute with universal quantification. It may sometimes be possible to construct a topos which classifies a higher order theory in the sense that models of in a topos correspond to those geometric morphisms which *do *preserve the relevant structure, but at that point it is clear that this will typically be different from the classifying topos for the simpler theory.

As for whether the categories of models will be equivalent, that depends exclusively on whether the simpler theory is constructively/intuitionistically equivalent to the higher-order one.