Is there a logical interpretation for equalizer and co-equalizer? 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$.
 A: 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.
A: 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.
