Properties preserved and reflected by equivalences of categories My question is related to the following question: Equivalent categories are elementarily equivalent: Formalization?
According to "From a Geometrical Point of View: A Study of the History and Philosophy of Category Theory" by Jean-Pierre Marquis, Freyd characterized the properties that are preserved and reflected by equivalences of categories: they are closed formulas in first-order logic with two sorts (one for arrows and one for objects) with an equality predicate between parallel morphisms and no equality predicate between objects; moreover if one quantifies on arrows, one has to specify the domain and the codomain of the arrows. 
If $I$ is a finite category, then it seems to me clear that one can write in Freyd's language that a category has all limits over $I$. But what about limits over infinite categories? For instance, the property to have all the infinite denumerable products is preserved and reflected by equivalences of categories, right? But how could one write this property in Freyd's language, since one cannot quantify on sets of arrows/objects?
 A: Your interpretation of Freyd's (or Blanc's) theorem is way to broad. It actually says something like:

For every closed first-order formula $\Phi$ (over the bi-sorted language of categories), the following are equivalent:
  
  
*
  
*$\Phi$ is as described in your post (but not really, see below)
  
*for any equivalence $F : \mathbf M \to \mathbf M'$, $\mathbf M \models \Phi$ if and only if $\mathbf M' \models \Phi$
  

In particular, it restricts from the beginning to something expressible in first-order logic (excluding infinite products for example).
The theorem is in fact more general, as it encompasses non-closed formulae. But then, your description is not enough anymore: for example an equivalence of categories does not necessarily reflect equalizers. And, citing Freyd, "for the most perverse of reasons", namely that parallel arrows in the image of an equivalence can come from non-parallel arrows in the source category. (Of course, equivalence preserves and reflects the closed version of this : every parallel pair has an equalizer.) And this is actually the point of Freyd's and Blanc's work: precisely caracterizing the (non-closed) formulae with no perverse twist like this one.
In my opinion, if you want to get a feeling of what is going on, Blanc's paper is much more readable that Freyd's, but that could be a matter of taste. (Also Blanc's paper is in french.)
