Given the signature $\lbrace \mathsf{dom}, \mathsf{cod}, \mathsf{id},\circ \rbrace$ and the axioms of category theory – which are expressible in the signature's first-order (FO) language – I wonder
- which (relevant) properties of categories as a whole
- which properties of and relations between individuals (= objects and morphisms) inside a category
- which other concepts and constructions
are expressible in category theory's first-order language – and which are genuinely not.1
(For graph theory there is a highly elaborate investigation of expressibility of properties in different languages - FO, SO, MSO - basically driven by Bruno Courcelle.)
The following properties are easily seen to be FO-expressible:
being a initial/terminal object
being a product/coproduct
being a monic/epic (morphism)
being a groupoid (category)
What - among other things - is not clear to me is how being a subobject of $A$ might be FO-expressible? Officially a subobject of a given object $A$ is a specific equivalence class of morphisms with codomain $A$ (as a subclass of individuals this is not an FO-definable individual) which corresponds naturally to an isomorphism class of objects (ditto). But maybe being an element of this isomorphism class is FO-expressible, eventually?
This becomes interesting when we ask if being connected is a FO-expressible property of objects (= graphs) in the category of finite graphs:
(Note: As a property of graphs as a whole connectedness is provably not expressible by a closed formula in the FO-language of graphs with signature $\lbrace R\ \rbrace$)
On the other hand:
Is the property of being a category of finite graphs expressible by a closed formula in the FO-language of categories?
1 Properties of categories "as a whole" are expressed by closed formulas. $n$-ary relations between individuals are expressed by formulas with $n$ free individual variables.