I'm starting Model Theory: An Introduction by David Marker. After reading about an $\mathcal{L}$-theory for a language $\mathcal{L}$, I wanted to try to make a theory of small categories. Can this be done?

My instinct for an approach is to start with a set $X$ of objects and actually create a theory for the morphisms of the category. So I want some "partial operation" $\circ$, which I was going to do by adding a constant symbol $u$, for undefined, and create rules for when I can compose morphisms. I think I could figure that out, but I also really want an axiom like $\forall f \:\exists x\in X\: f\circ 1_x = f$. But of course, I am not allowed to quantify over this random set $X$. Even if I put constants $1_x$ in my language, I also cannot quantify over subsets of the universe. Thoughts?

  • 3
    $\begingroup$ The usual way is to define unary function symbols $s, t$ representing the identity on the source and target of a morphism, respectively. $\endgroup$ Jan 31, 2021 at 10:15

2 Answers 2


Welcome to MSE!

While people have studied notions of model theory with partial functions (though in my experience, the universal algebraists tend to be slightly more excited by these things), there are two possibilities for a cleaner approach. For completeness sake, you can find some information about "partial algebras" here, and "free logic" here.

The first cleaner approach is to simply make composition a relation. After all, a partial function is still a relation, and model theory is perfectly well equipped to handle relations with certain axioms!

Then we might formulate a first order notion of a category as a $2$-sorted theory (with a set $\mathsf{Ob}$ of objects and a set $\mathsf{Mor}$ of morphisms) equipped with three function symbols

  • $\text{dom} : \mathsf{Mor} \to \mathsf{Ob}$
  • $\text{cod} : \mathsf{Mor} \to \mathsf{Ob}$
  • $\text{id} : \mathsf{Ob} \to \mathsf{Mor}$

and one relation symbol

  • $\text{comp} \subseteq \mathsf{Mor} \times \mathsf{Mor} \times \mathsf{Mor}$

Then one can include axioms like

$$ \forall x : \mathsf{Ob} . \forall f : \mathsf{Mor} . \text{dom}(f) = x \to \text{comp}(f,\text{id}(x),f) $$

This axiom says that, if the domain of $f$ is $x$, then $f \circ \text{id}(x)$ is defined and equals $f$.

You might also want an axiom

$$ \forall f : \mathsf{Mor} . \forall g : \mathsf{Mor} . \text{dom}(f) = \text{cod}(g) \to \exists h : \mathsf{Mor} . \text{comp}(f,g,h) $$

This axiom says that for any two composable morphisms, a composite actually exists.

You can imagine similar axioms asserting composition is associative, etc.

As a (fun?) exercise, you should try to list all the axioms in this way. Keep in mind you'll need to add some silly looking axioms like $\forall x : \mathsf{Ob} . \text{dom}(\text{id}(x)) = x$ and an axiom saying that for noncomposable morphisms, a composite doesn't exist.

The other way to handle a theory of categories is to move to something slightly more expressive than first order logic. This is the approach taken by many categorical logicians, as it lets us talk about a theory of categories "internal" to another category. It's a little bit more complicated, so I won't say much about it, but you can find a good discussion in Awodey's Lecture Notes on Categorical Logic. In particular in catlog2a, section 2.3.1.

The idea is to work with a theory that allows "subtypes". This gives us the power to quantify over definable subsets, which is all we need to handle composition. After all, if we have two basic sorts $\mathsf{Ob}$ and $\mathsf{Mor}$, then we can define a new sort

$$ C \triangleq \{ (f,g) : \mathsf{Mor} \times \mathsf{Mor} ~|~ \text{dom}(f) = \text{cod}(g) \} $$

and a function $\circ : C \to \mathsf{Mor}$ denoting composition.

Again, as a (fun?) exercise, you might try to explicitly write down the axioms with this new power at your disposal.

I hope this helps ^_^

  • 3
    $\begingroup$ For the OP: the name for the kind of theory HallaSurvivor refers do in the last section is "essentially algebraic theory" or "finite limit theory". Just to give you some terms to search for if you want to read more. $\endgroup$ Jan 31, 2021 at 10:49
  • 3
    $\begingroup$ You can also make a single-sorted first order theory by identifying objects with their identity morphisms. Which is a little bit unnatural, but it works and stays within the sort of theories that Marker focuses on. $\endgroup$ Jan 31, 2021 at 13:56
  • 1
    $\begingroup$ Thanks! This is a neater approach to theories. It's not quite what I was looking for, but it is in actuality a very practical mindset. Much appreciated! $\endgroup$ Jan 31, 2021 at 18:27

Giving a theory of the morphisms is a good idea. One way to see this is that you want the structure-preserving maps between categories to be functors, and a functor is a functional relationship on objects and morphisms. But notice that a functor $F : \mathcal{C} \to \mathcal{D}$ has to satisfy $1_{F(x)} = F(1_{x})$ for all $x \in \mathcal{C}$, so really you only have to specify how a structure-preserving map between categories acts on arrows: if you want to know how it acts on an object $x$, you just have to look at how it acts on $1_{x}$. Moreover, the category axioms imply that there is a bijection between objects and identity morphisms.

So one thing we could do is to forget about the objects entirely, and cook up a theory whose domain $M$ is intended to be the set of morphisms in a category. We want to give a partially-defined composition relation and impose some axioms on it. Let's use your suggestion, and introduce a constant $u$ representing the "undefined morphism" and a function symbol $\circ : M \times M \to M$. I guess you will have to give some axioms involving $u$, like $\forall f\, (f \circ u = u)$ and such. Alternatively, you could introduce a relation $C \subseteq M \times M$ and make the signature of your function symbol $\circ : C \to M$.

For the identity axiom, we want to make sure there is an identity morphism for every object in the category. But we want to avoid talking about objects directly. But objects are just the things that serve as domains and codomains for morphisms. And (co)domains are used to say which morphisms are composable. The identity axiom says that for every morphism $f : x \to y$ there is a morphism $1_{x} : x \to x$ that's composable with $f$ and such that $f \circ 1_{x} = f$. So we can just say that: $$ \forall f\, \exists e\, (\{f \circ e = f\} \land \forall g\, \{[(g \circ e \not= u) \to (g \circ e = g)] \land [(e \circ g \not= u) \to (e \circ g = g)]\}) $$ and a similar axiom involving things like $e \circ -$. Informally, this says that for every $f$ there is an $e$ that acts like the identity of the domain of $f$. There's no reason to quantify over objects here, because what we're really after is the identity morphism, and that's just a morphism that acts as a unit. Then all that's left is associativity. You can formalize this as the statement that the following are equivalent:

  1. $h \circ g \not= u$ and $g \circ f \not= u$
  2. $(h \circ g) \circ f \not= u$
  3. $h \circ (g \circ f) \not= u$
  4. $(h \circ g) \circ f \not= u$ and $(h \circ g) \circ f = h \circ (g \circ f)$.

Of course, there's always more than one way to give a theory of some mathematical object. For example, you could have a theory with a predicate $O$ that applies to objects and a predicate $M$ that applies to arrows, and ensure identity arrows with a function symbol $1 : O \to M$, or something like this. There are lots of options.

  • 2
    $\begingroup$ Does this idea for the identity axioms actually work? What about a semigroup with two idempotent elements $a,b$ such that $ab=a$ and $ba=b$? $\endgroup$ Jan 31, 2021 at 15:57
  • $\begingroup$ I am also concerned that I will need better axioms for when I am allowed to compose. Something like $\forall f\: \forall g\: (1_x\circ f \neq u \wedge g\circ 1_x\neq u) \rightarrow g\circ f \neq u$. to be an axiom for each identity morphism. This is why I wanted to make constant symbols for them. $\endgroup$ Jan 31, 2021 at 16:56
  • 1
    $\begingroup$ @KevinArlin oops, you're right, thanks, I confused myself with this approach to partial functions. I think it should work now. IIRC, Freyd defines categories as something like this in Abelian Categories, so the idea should work $\endgroup$ Jan 31, 2021 at 16:56
  • 1
    $\begingroup$ @Cobalt_000 that condition follows from the implication 1 -> 2 or 1 -> 3, along with the (corrected) identity axiom $\endgroup$ Jan 31, 2021 at 17:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .