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 graphsexpressible 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.

acategory of finite graphs" mean "the objects of C may be identified with a set of finite graphs, and the morphisms of C may be identified with graph morphisms, in a way such that the standard relations apply"? And are you allowing graphs with loops or not? Or do you mean "thecategory of finite graphs", as in the comment? – Matt F. Feb 27 at 22:30