Is there a logical interpretation for equalizer and co-equalizer?

Question

I know the logical equivalent to several universal constructions. For example product $\times$ is $\land$ and co-product $+$ is $\lor$. The associated arrows are projection and inclusion. The equalizer arrow is an arguably even simpler construction, is there a logical interpretation?

For the co-product, say, I can say "If I know $C$ follows from $A$ and also $C$ follows from $B$, why not store this information in the statement that $C$ follows from $A\lor B$." and I picture the universal property diagram.

Now the equalizer, with two parallel arrows, is a little more tricky. Because if the logic only care for proofs, $C$ from $A$ say, then you've won when there is just one arrow. I figure answer will someone has that there is a sub-assumption $A'$ that's sufficient for the proof of $C$.

Answer 1

Equalizers and coequalizers play an essential role in categorical quantifier logic. (See Makkai and Reyes, First-order categorical logic.)

Equalizers are used to interpret the equality relation (in a first-order language). In particular, let $\{x:t\}$ denote a term in context, which means that $t$ is a term of type $A_1,...,A_n;B$ and $x$ denotes a sequence of variables, including the variables free in $t$. In an interpretation $M$, $M(\{x:t\})$ will be a function from $M(A_1)\times \cdots \times M(A_n)$ to $M(B)$. Then $M(\{x:t=t'\})$ is defined to be the equalizer of the functions $M(\{x:t\})$ and $M(\{x:t'\})$.

Similarly, coequalizers are used to interpret quotient types. In particular, if $E$ is a definable equivalence relation on a sort $A$, and if $p,q:E\to A$ are the projections, then the equalizer $e:A\to A/E$ of $p$ and $q$ gives the projection onto the quotient type.

Answer 2

Your 'logical category' is a preorder, ordered by entailment: objects are propositions, and there is an arrow $A \to B$ if and only if $A$ implies $B$. So there is at most one morphism between any two objects.

Equalizers and coequalizers in preorder categories are kind of boring, since any diagram of the form $$A \overset{f}{\underset{g}{\rightrightarrows}} B$$ must have $f=g$. (Both $f$ and $g$ are just the statement "$A$ implies $B$"!)

So in any preorder category, and in particular your proposition-and-entailment category, we have $$\mathsf{eq}(A \rightrightarrows B) = A \qquad \mathsf{coeq}(A \rightrightarrows B) = B$$ as you can very easily verify.

This even extends to the case where a morphism $A \to B$ is a proof of $B$ from $A$, so that there may be more than one morphism from $A$ to $B$. The key is that any morphism $C \to A$ automatically commutes with the equalizer diagram: just stick the proofs one after the other.