Category theory from the first order logic point of view

Question

$\DeclareMathOperator{\Id}{Id} \DeclareMathOperator{\Obj}{Obj} \DeclareMathOperator{\Arr}{Arr} \DeclareMathOperator{\Dom}{Dom} \DeclareMathOperator{\Cod}{Cod}$

MacLane defines "metacategories" purely axiomaticaly. When we look at it from perspective of first order logic we see that "metacategories" is a first order theory consisting following signature:

• two unary predicates $\Obj,\Arr$
• two unary functions $\Dom,\Cod$
• binary function $\circ$
• unary function $\Id$

and axioms for domain, codomain, composition unity. I wrote this axioms in the appendix.

Next, we can define a category as a model in this first order theory. Given two categories, we can also define a functor as a structure map.

Question. Is there some source which treats the whole category theory from this point of view?

For example I do not know how to define natural transformation in this language.

---

Appendix. Axioms for category theory :

• $(\forall f)(\Arr(f) \rightarrow (\Obj(\Dom(f)) \wedge \Obj((\Cod(f)))$
• $(\forall f,g)((\Arr(f)\wedge\Arr(g)\wedge\Cod(f)=\Dom(g))\rightarrow \Arr(g\circ f))$
• $(\forall a)(\Obj(a)\rightarrow((\Arr(\Id(a))\wedge \Dom(\Id(a))=a=\Cod(\Id(a))\wedge (\forall f)(\Arr(f)\rightarrow ((\Dom(f)=a\rightarrow f\circ\Id(a)=f)\wedge(\Cod(f)=a\rightarrow \Id(a)\circ f=f))))$
• $(\forall f,g,h)((\Arr(f)\wedge\Arr(g)\wedge\Arr(h)\wedge\Cod(f)=\Dom(g)\wedge \Cod(g)=\Dom(h))\rightarrow h\circ ((g\circ f) = (h\circ g)\circ f))$

Answer 1

This would be very unusual, for two important reasons.

First, models in sets are not enough. It is important to consider large categories, such as Set or AbGrp or Top or Cat.

Secondly, category theory develops its own take on first-order logic — it would be a wasted effort (and somewhat counter-philosophical) to study the subject in the traditional set-oriented version of logic.

However, one does study categories as models — we call such a thing an internal categories.

---

Regarding your specific note on natural transformations, there are several paths that might lead you there.

The first is that you can show the product has a right adjoint, so that there is a natural bijection

$$ \hom(\mathcal{C} \times \mathcal{D}, \mathcal{E}) \cong \hom(\mathcal{C}, \mathcal{E}^{\mathcal{D}}) $$

This means that you can treat $\mathcal{D}^\mathcal{C}$ as the category of morphisms from $\mathcal{C}$ to $\mathcal{D}$. A natural transformation, then, is an arrow in this category.

A similar phenomenon happens, for example, in abelian groups, which allows you to construct the abelian group of morphisms from one group to another.

Now, assuming you didn't think to show that, one can still draw inspiration from it; since arrows can be viewed as morphisms $\hom(\uparrow, \mathcal{C})$, where $\uparrow$ means the arrow category, even if you didn't know that $\mathcal{E}^\mathcal{D}$ existed, one can still draw inspiration from the idea of the adjunction above and define a natural transformation to be a morphism $\uparrow \times \mathcal{C} \to \mathcal{D}$.

And this whole thing is similar to topology, and one might be tempted to mimic the definition of a homotopy.

Answer 2

First-order PA and first-order ZF are usually presented as mono-sortal -- in PA, every "thing" (every object in the domain of quantification) is a "number", and in ZF, "every" thing is a set. A first-order category theory, if trying to preserve this practice, could become a mono-sortal first-order "arrow theory". One could shrink the signature presented in the axiomatization above by eliminating the Arr predicate, since every thing, including objects, could be an arrow -- the objects would be the id-arrows. In that treatment, every arrow goes from one id-arrow to another id-arrow, and id-arrows are the ones that go from themselves to themselves (i.e. are fixpoints of both the domain/"source" and codomain/"target" operators). A group could be a monoid where all the arrows go from and to the same one object, which is a distinguished arrow that is the group's identity element and is defined to compose with all the others accordingly. All of the "actual structure" of a category would be in a model's definition of the composition operator. Unfortunately, since that operator is partial (if there is more than one object in the category, it is possible for some arrows not to compose with others at all because their target and source don't dovetail), the resulting axiomatization would need to write composition as a ternary predicate since the usual definition of a first-order language doesn't allow "partial" term-constructors.

William Hatcher gave this as a first-order axiomatization.

C.1. $\forall x_1[ d(c(x_1)) = c(x_1) \wedge c(d(x_1)) = d(x_1) ]$

The domain of the codomain of $x_1$ is the codomain of $x_1$, and the codomain of the domain of $x_1$ is the domain of $x_1$.

C.2. $\forall x_1x_2x_3x_4 [ K(x_1,x_2,x_3) \wedge K(x_1,x_2,x_4)\rightarrow x_3=x_4]$

The composition of $x_1$ with $x_2$ is unique when it is defined.

C.3. $\forall x_1x_2[ \exists x_3[ K(x1,x2,x3)]\leftrightarrow c(x_1)=d(x_2)$ ]

The composition of $x_1$ with $x_2$ is defined if and only if the codomain of $x_1$ is the domain of $x_2$.

C.4. $\forall x_1x_2x_3[ K(x_1,x_2,x_3)\rightarrow d(x_3)=d(x_1) \wedge c(x_3)=c(x_2) ]$

If $x_3$ is the composition of $x_1$ with $x_2$ then the domain of $x_3$ is the domain of $x_1$ and the codomain of $x_3$ is the codomain of $x_2$.

C.5.$\forall x_1[ K(d(x_1),x_1,x_1) \wedge K(x_1,c(x_1),x_1)]$

For any $x_1$, the domain of $x_1$ is a left identity for $x_1$ under composition and the codomain is a right identity.

C.6. $\forall x_1x_2x_3x_4x_5x_6x_7 [ ( K(x_1,x_2,x_4) \wedge K(x_2,x_3,x_5) \wedge K(x_1,x_5,x_6) \wedge K(x_4,x_3,x_7) )\\\rightarrow x_6=x_7 ]$ Composition is associative when it is defined.

Any model of this theory is a category. Unfortunately, however, that would beg the question of what to use as a model-construction language. First-order logic is typically associated with models constructed in a set theory such as ZF. That would defeat the whole purpose of this as an alternative foundation, as well as limiting us to "small" or "internal" categories.