3
$\begingroup$

I'm not certain as to how I should formulate this question; it might be considered a soft question. I am interested in finding a general way to take a category $\mathbb{C}$ and an (elementary) topos $\mathcal{E}$, which we have some chosen semantics for, and constructing a semantics for $\mathbb{C}$ in terms of that of $\mathcal{E}$. For example, suppose we are presented syntactical data for a category $\mathbb{G}$ equivalent to $\mathbf{Grp}$, and we let $\mathcal{E}=\mathbf{Set}$. Then, if we didn't have the axioms of a group object internal to the category of sets, is there some way we might realize the objects of $\mathbb{G}$ as objects of $\mathbf{Set}$ with extra structure, and morphisms as functions respecting this structure? Does it suffice to find a forgetful functor into our semantic topos, and see how it treats objects and what sort of data is forgotten?

I'm guessing that there can be no way to do this given any choice of category and topos, but are there restrictions we can place on each such that such a "relative semantics" can always be built?

Any recommendation of literature that regards this question would also be greatly appreciated. Thank you.

Note: I am not sure that a topos is necessary here. We just happen to have semantics for lots of pretty categories in terms of $\mathbf{Set}$ because it is a nice category to work with in the first place. Perhaps $\mathcal{E}$ can be any category with a semantics chosen?

$\endgroup$
2
$\begingroup$

There is no good way of doing this. For instance, consider a theory $\mathbb{T}$ such that $\mathbb{T}$-models in $\mathbf{Set}$ do not exist. Clearly, going by the category of models in $\mathbf{Set}$ alone, it will be impossible to distinguish $\mathbb{T}$ from the inconsistent theory. There are more sophisticated versions of this phenomenon. For example, the category of complete join semilattices is indistinguishable from the category of $\kappa$-complete join semilattices, where $\kappa$ is the size of the universe. In order to avoid this issue, we must restrict to a fragment of logic for which we have a sufficiently strong completeness theorem, such as coherent logic.

So let $\mathbb{T}$ be a coherent theory and let $\mathcal{M}$ be the category of models of $\mathbb{T}$ in $\mathbf{Set}$. Then $\mathcal{M}$ is an accessible category with colimits of filtered diagrams (but not every such category is the category of models for a coherent theory). Since $\mathbb{T}$ is coherent, there is a category $\mathcal{B}$ together with a set $\mathcal{L}$ of cones over finite diagrams in $\mathcal{B}$ and a set $\mathcal{C}$ of cocones under finite diagrams in $\mathcal{B}$ such that $\mathcal{M}$ is equivalent to the category of functors $\mathcal{B} \to \mathbf{Set}$ that send members of $\mathcal{L}$ to limiting cones and members of $\mathcal{C}$ to colimiting cocones. (Moreover, $\mathcal{B}$, $\mathcal{C}$, and $\mathcal{L}$ are canonical given $\mathbb{T}$.) The category of $\mathbb{T}$-models in a topos $\mathcal{E}$ is defined analogously: it is the category of functors $\mathcal{B} \to \mathcal{E}$ such that send members of $\mathcal{L}$ to limiting cones and members of $\mathcal{C}$ to colimiting cocones.

In the case where $\mathcal{M}$ is the category of models for a Horn theory (or, more generally, a cartesian theory), there is a canonical choice of $\mathbb{T}$ and hence a canonical choice of $\mathcal{B}$, $\mathcal{L}$, and $\mathcal{C}$: namely, $\mathcal{B}^\mathrm{op}$ is a skeleton of the category of finitely presented models, $\mathcal{L}$ is the set of all limiting cones over finite diagrams in $\mathcal{B}$, and $\mathcal{C}$ is empty. This covers the case where $\mathcal{M}$ is the category of models of an algebraic theory.

$\endgroup$
1
  • $\begingroup$ Wow, great answer! Thank you so much. $\endgroup$ Dec 30 '15 at 16:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.