I'm referring to Awodey's Category Theory, precisely to the chapter 3.1 on duality principle. Here it is first stated the formal duality: if a statement in the language of category theory can be proved only by the axioms of category theory, also the dual statement (which Awodey specifies formally how to obtain) can be proven, for the axioms are self-dual. Instead the conceptual duality amounts to: if a statement is true interpreted in any category, the dual statement is too. This is justified saying that if a statement is true interpreted in a category $C$, its dual is true interpreted in $C^{op}$ (is this a consequence of the fact that the duality reflects and preserve equality? Is "$=$" the only predicate in the language of categories?); and obviously all the dual categories are just all the categories.
About the relationship between (the "strongness" of) these duality principles, I'd like to know if a statement true in all the categories is provable by the axioms; the converse I'd say is true already. In a certain sense this should be a completeness property, but I'd say that it has not much in common with the first order logic, already by the facts that the structure is made of two sets (objects and arrows) and the composition is defined only on some pairs of arrows for example. Thanks in advance.
Best Answer
Yes, every first-order statement about categories which is true in all categories (in fact it suffices to consider only small categories) is provable from the category theory axioms, and to deduce this from the usual completeness theorem for first-order logic it suffices to write down a first-order axiomatization of small categories.
This can be done as follows: we think of a small category entirely in terms of its set $\text{Arr}$ of arrows. Objects are encoded as identity arrows which we'll isolate later. Then we introduce two functions $s, t : \text{Arr} \to \text{Arr}$ which send an arrow to its source (identity arrow) and its target (identity arrow); the identity arrows are exactly the arrows which are fixed points of both $s$ and $t$. To encode composition we add a ternary predicate $\{ f \circ g = h \} \subset \text{Arr}^3$ describing which pairs of arrows compose to which. Then we write down a bunch of first-order axioms which can be found here.
I don't have a clear sense of how powerful the first-order language of categories is off the top of my head though. The technical restriction to small categories here, which is probably removable, means this result doesn't directly apply to interesting large categories such as $\text{Set}$ or $\text{Vect}$.