Category theory from the first order logic point of view

2.3k Views Asked by At

$\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))$
1

There are 1 best solutions below

2
On BEST ANSWER

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.