Clarification on the use of elements in a categorical environment

Question

At the end of the introduction of the article "Internal Graphs and Internal Groupoids in Mal'cev Categories", Carboni, Pedicchio and Pirovano write as follows:

While working in a category with finite limits, we freely use elements as far as Horn sentences built up from atomic ones and equality are concerned; we use existential quantification only when we can show uniqueness. It is well known that in such a way we can always interpret our statement in a lex category in a valid way.

I don't understand what they are saying. In the article they use elements more or less in every definition, statement or proof, and I don't understand how is this possible since the context is the one of Mal'cev categories. What general results are they using in order to do categorical proofs by using elements?

Any help would be appreciated.

Answer 1

It has been a while since I read that paper, but if I remember correctly the general result they use can be summarised as the following "meta-theorem", taken from these notes :

If $P$ is a statement of the form $\varphi \Rightarrow \psi$, where $\varphi$ and $\psi$ can be expressed as conjunctions of properties in the following list :

1. some finite diagram is commutative;
2. some morphism is an monomorphism;
3. some morphism is an isomorphism;
4. some finite diagram is a limit diagram;
5. some arrow $f:A\to B$ factors through a specified monomorphism $S\to B$.

If this statement $P$ is valid in the category of sets, it is valid in every category.

You can read the proof in the linked notes, but the idea is that for any category $\mathcal{C}$, all these properties are preserved and reflected by the Yoneda embedding $\mathcal{C}\to [\mathcal{C}^{op},\mathbf{Set}]$, so they hold in $\mathcal{C}$ if and only if they hold in $[\mathcal{C}^{op},\mathbf{Set}]$, and this in turn is equivalent to the fact that they hold in $\mathbf{Set}$. This metatheorem also has a dedicated (pre)chapter at the beginning of the book "Mal'cev, Protomodular, Homological and Semi-abelian categories" by Borceux and Bourn.

Answer 2

This is, as the authors state, a well known result of categorical logic. The restrictions stated are exactly what is necessary to produce cartesian logic, and cartesian logic is the internal logic of lex categories. This means, among other things, we can write formulas in cartesian logic and then give them semantics (i.e. interpret them) into any lex category.

For traditional semantics of (multi-sorted) logic, a predicate like $P(x,y)$ where $x$ is of sort $X$ and $y$ is of sort $Y$ gets interpreted as a relation $[\![P]\!]\subseteq[\![X]\!]\times[\![Y]\!]$. A conjunction like $P(x,y)\land Q(x,y)$ becomes $[\![P]\!]\cap[\![Q]\!]$. An entailment like $P(x,y)\vdash Q(x,y)$ becomes $[\![P]\!]\subseteq[\![Q]\!]$. Equality is, of course, just $\{(x,x)\mid x\in [\![X]\!]\}\subseteq[\![X]\!]\times[\![X]\!]$. Finally, full existential quantification $\exists y:Y.P(x,y)$ is interpreted as $\pi_1([\![P]\!])\subseteq[\![X]\!]$, i.e. $\{\pi_1(p)\mid p\in[\![P]\!]\}$.

The categorical semantics just uses the categorical analogues of these constructions. Instead of a subset, we have a subobject $[\![P]\!]\rightarrowtail[\![X]\!]\times[\![Y]\!]$, i.e. an equivalence class of monomorphisms. Intersection is interpreted by pullback along the subobjects. $P(x,y)\vdash Q(x,y)$ says that the subobject $[\![P]\!]\rightarrowtail[\![X]\!]\times[\![Y]\!]$ factors through the subobject $[\![Q]\!]\rightarrowtail[\![X]\!]\times[\![Y]\!]$. Equality is represented by the arrow $\langle id,id\rangle : [\![X]\!]\to[\![X]\!]\times[\![X]\!]$ which is a monomorphism. The interpretation of the existential $\exists y:Y.P(x,y)$ would be the image of the arrow $[\![P]\!]\rightarrowtail[\![X]\!]\times[\![Y]\!]\stackrel{\pi_1}{\to}[\![X]\!]$, but a lex category doesn't have the structure to construct this. (A regular category does though.) However, if we can prove that there is at most one $y$ such that $P(x,y)$ holds for all $x$, formally $P(x,y)\land P(x,z)\vdash y=z$, then it turns out $[\![P]\!]\rightarrowtail[\![X]\!]\times[\![Y]\!]\stackrel{\pi_1}{\to}[\![X]\!]$ is a monomorphism, and we can use it as the interpretation of $\exists y:Y.P(x,y)$ without needing to construct images. Or, to put it a different way, $[\![P]\!]$ is already the image, so the image factorization is trivial.

Caramello provides a similar description of the situation in sections 4 and 5. In particular, cartesian theories in definition 4.5 and cartesian categories in definition 5.5 and finally subsection 5.2.1 describes internal logics and how to map logical constructs to categorical constructs.

The upshot is that we can write logical formulas exactly like we're used to, and as long as we restrict to cartesian logic, those formulas will be making meaningful statements about lex categories. There's also a more term-oriented perspective, the internal language, which in the case of lex categories will look like an algebraic theory except that we allow partial operations defined on equationally-defined subsets.