Thanks for clarifying your question. The formulation that
you and Dorais give seems perfectly reasonable. You have a
first order language for category theory, where you can
quantify over objects and morphisms, you can compose
morphisms appropriately and you can express that a given
object is the initial or terminal object of a given
morphism. In this language, one can describe various finite
diagrams, express whether or not they are commutative, and
so on. In particular, one can express that composition is
associative, etc. and describe what it means to be a
category in this way.
The question now becomes: is this theory decidable? In
other words, is there a computable procedure to determine,
given an assertion in this language, whether it holds in
all categories?
The answer is No.
One way to see this is to show even more: one cannot even
decide whether a given statement is true is true in all
categories having only one object. The reason is that group
theory is not a decidable theory. There is no computable
procedure to determine whether a given statement in the
first order language of group theory is true in all groups.
But the one-point categories naturally include all the
groups (and we can define in a single statement in the
category-theoretic language exactly what it takes for the
collection of morphisms on that object to be a group).
Thus, if we could decide category theory, then we could
decide the translations of the group theory questions into
category theory, and we would be able to decide group
theory, which we can't. Contradiction.
The fundamental obstacle to decidability here, as I
mentioned in my previous answer (see edit history), it the
ability to encode arithmetic. The notion of a strongly
undecidable
structure
is key for proving various theories are undecidable. A
strongly undecidable theory is a finitely axiomatizable
theory, such that any theory consistent with it is
undecidable. Robinson proved that there is a strongly
undecidable theory of arithmetic, known as Robinson's Q. A
strongly undecidable structure is a structure modeling a
strongly undecidable theory. These structures are amazing,
for any theory true in a strongly undecidable structure is
undecidable. For example, the standard model of arithmetic,
which satisfies Q, is strongly undecidable. If A is
strongly undecidable and interpreted in B, then it follows
that B is also strongly undecidable. Thus, we can prove
that graph theory is undecidable, that ring theory is
undecidable and that group theory is undecidable, merely by
finding a graph, a ring or a group in which the natural
numbers is interpreted. Tarski found a strongly undecidable
group, namely, the group G of permutations of the integers
Z. It is strongly undecidable because the natural numbers
can be interpreted in this group. Basically, the number n
is represented by translation-by-n. One can identify the
collection of translations, as exactly those that commute
with s = translation-by-1. Then, one can define addition as
composition (i.e. addition of exponents) and the divides
relation is definable by: i divides j iff anything that
commutes with si also commutes with
sj. And so on.
I claim similarly that there is a strongly undecidable
category. This is almost immediate, since every group can
be viewed as the morphisms of a one-object category, and
the group is interpreted as the morphisms of this category.
Thus, the category interprets the strongly undecidable
group, and so the category is also strongly undecidable. In
particular, any theory true in the category is also
undecidable. So category theory itself is undecidable.
There's a big difference between teaching category theory and merely paying attention to the things that category theory clarifies (like the difference between direct products and direct sums). In my opinion, the latter should be done early (and late, and at all other times); there's no reason for intentional sloppiness. On the other hand, teaching category theory is better done after the students have been exposed to some of the relevant examples.
Many years ago, I taught a course on category theory, and in my opinion it was a failure. Many of the students had not previously seen the examples I wanted to use. One of the beauties of category theory is that it unifies many different-looking concepts; for example, left adjoints of forgetful functors include free groups, universal enveloping algebras, Stone-Cech compactifications, abelianizations of groups, and many more. But the beauty is hard to convey when, in addition to explaining the notion of adjoint, one must also explain each (or at least several) of these special cases. So I think category theory should be taught at the stage where students have already seen enough special cases of its concepts to appreciate their unification. Without the examples, category theory can look terribly unmotivated and unintuitive.
Best Answer
Etale cohomology, whose definition and study would be inconceivable without the use of categorical methods, underlies the construction of many interesting Galois representations as well as the entire context for Deligne's work on the Riemann Hypothesis for varieties over finite fields and its various generalizations, and work of Taylor et al. on Sato-Tate.
The concept of moduli schemes and the study of their non-trivial properties (and reasons for their existence) would likewise be impossible without the systematic use of categorical reasoning, and these underlie Faltings' work on the Mordell conjecture, the work of Drinfeld/Lafforgue on global Langlands correspondence for function fields, the work of Wiles et al. on modularity of Galois representations, the work of Mazur/Merel on torsion in elliptic curves over number fields, the use of Heegner points by Gross-Zagier...and the role of Galois cohomology in all of these matters (informed through homological reasoning) is utterly pervasive.
There's so much more which could be said, but I think the above is quite sufficient to make it clear that categorical and homological methods are ubiquitous throughout the deepest parts of modern algebraic number theory.