Is there a definition of a category in a single formal logic string?

Question

I would like to be able to present a complete definition of a category in a fully technical and formal notational language, in a single line. How might this be possible?

Answer 1

If you accept classical first-order logic as an example of a fully technical and formal notational language (whatever that means), then you can get a positive answer by writing the universal closure of the conjunction of the following formulae as a single line. I leave finding a sufficiently long line as an exercise for the reader. Also, you did not reveal anything about your intended use case for a complete definition of category in a single line, so I can't guarantee that you'll find this presentation useful.

1. $D(D(f)) = D(f) = C(D(f))$
2. $C(C(f)) = C(f) = D(C(f))$
3. $g\circ f = gf \rightarrow D(gf) = D(f) \wedge C(gf) = C(g)$
4. $(\exists! gf. g \circ f = gf) \leftrightarrow C(f) = D(g)$
5. $f \circ D(f) = f$
6. $C(f) \circ f = f$
7. $(g \circ f = gf \wedge h \circ g = hg) \rightarrow (h \circ gf = hgf \wedge hg \circ f = hgf)$

where $f,g,h,gf,hg,hgf$ are all first-order variable names ranging over the sort of morphisms, while $D,C$ are first-order unary function symbols (read as "the identity morphism on the domainof " and "the identity morphism on the codomain of" respectively), and $\_\circ\_=\_$ is a ternary relation symbol.

The first three conjuncts fix a couple of elementary facts about how co/domains of morphisms behave, the fourth conjunct ensures that one can compose two morphisms precisely if they share co/domains, the fifth and sixth conjuncts state that the identity morphisms indeed act as identities, and the seventh asserts associativity of composition.

Any (small) category in the usual sense constitutes a model for the one-line axiom above, and vice versa every model gives rise to a category in the usual sense. So this gives a complete definition of category in a single line in fully technical and formal language - at least as much as anything else can have a definition in a fully technical and formal language.