The theory of categories is undecidable. By the theory of categories I mean the theory with two types Ob (objects) and Ar (arrows) together with operations dom:Ar → Ob, cod:Ar → Ob, 1:Ob → Ar, and o:Ar×Ar→Ar (possibly partial composition), and the obvious axioms.
One way to see this is to interpret the theory of groups — which is undecidable by a beautiful theorem of Trakhtenbrot — within the theory of pointed categories, that is categories with a distinguished object * (which is an inessential extension). Indeed, the definable set of invertible arrows from * to * form a group, and every group can be interpreted as the set of arrows in a category with * as its only object. I suspect that the theory of Abelian categories is not decidable either, but I haven't tried to prove that (yet).
