6
$\begingroup$

$\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))$
$\endgroup$
12
  • $\begingroup$ You mean $\operatorname{Obj}(a)\to\ldots$ in the third axiom, I suppose $\endgroup$ – Hagen von Eitzen Aug 5 '17 at 14:40
  • $\begingroup$ What's $\text{Arr}$? $\endgroup$ – Andrew Tawfeek Aug 5 '17 at 14:42
  • 1
    $\begingroup$ @AndrewTawfeek: I presume $\mathrm{Obj}(a)$ is interpreted to mean that $a$ is an object and $\mathrm{Arr}(f)$ is interpreted to mean that $f$ is an arrow. $\endgroup$ – Clive Newstead Aug 5 '17 at 14:43
  • $\begingroup$ Maybe a two-sorted language could be more appropriate here since in category theory, asking what $Dom(a)$ is when $a$ is an object can seem weird. $\endgroup$ – Maxime Ramzi Aug 5 '17 at 14:43
  • 2
    $\begingroup$ You might want to include an axiom like $$(\forall x)(\mathrm{Obj}(x) \Leftrightarrow \neg \mathrm{Arr}(x))$$ to ensure that everything is an object, or a morphism, but not both. Another possibility is to say that every element is an arrow, and refer to objects by instead referring to their identity arrows. Another possibility is to use first-order logic with dependent sorts, which is perhaps more natural from the perspective of a category theorist. $\endgroup$ – Clive Newstead Aug 5 '17 at 14:51
8
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ To be clear, the cartesian closure condition holds for small categories but usually not for locally small or large categories. So "arrow in $\mathbf{Set}^\mathbf{Set}$" can't be used, but the "inspired" approach of a functor $\uparrow\times\mathbf{Set}\to\mathbf{Set}$ works fine. Of course this is only an issue if one wants to capture non-small categories. As you point out, to do this requires considering something more than normal set theoretic models (at least in a "usual" set theory). $\endgroup$ – Derek Elkins left SE Aug 7 '17 at 1:06
  • 1
    $\begingroup$ I agree with your first reason, but I think considering models beyond $\mathbf{Set}$ doesn't lead to any contradiction. As for the second one. I can't see why this approach is a waste of effort. I believe that intertwining theories is not always a bad idea. In our case, I was just curious how Godel Completeness Theorem would look like applied to category theory (treated as a first order theory). $\endgroup$ – Fallen Apart Aug 8 '17 at 14:30
7
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.