There are a lot of theorems in basic homological algebra, such as the five lemma or the snake lemma, that seem like they'd be more easily proven by computer than by hand. This led me to consider the following question: is the theory of categories decidable?
More specifically, I was wondering whether or not statements about abelian categories can be determined true or false in finite time. Also, if they can be determined to be false, is it possible to explicitly describe a counterexample? If it is known to be decidable, is anything known about the complexity? (Other decidable theories often have multiply-exponential time complexities.) If it is known to be undecidable, say by embedding the halting problem, then can I change my assumptions a bit and make it decidable? (For example, maybe I shouldn't be looking at abelian categories after all.)
Thanks in advance.
Edit: It appears a clarification is needed. My goal was to consider the minimal theory that could state things like the five lemma, but not necessarily prove them. For example, I want to say:
If in an abelian category, you have a bunch of maps $0\to A \to B \to C\to 0$ and $0\to A' \to B' \to C'\to 0$ which make up two short exact sequences and some more maps $a:A\to A'$, $b:B\to B'$, $c:C\to C'$ which commute with the previous maps, and $a$ and $c$ are isomorphisms, then $b$ is an isomorphism, too.
Sentences of this form would be inputs to a program, which decides if this statement is in fact true in ZFC (or your other favorite axiomatization of category theory). The point here is that I am restricting the sentences one can input into the program, but keeping ZFC or whatnot as my framework.
I hoped (perhaps naively) that if I restricted the class of sentences, it might be decidable whether or not these statements were true. For example, I imagined that every such theorem is either proven by diagram chasing, or it is possible to find a concrete example of maps among, say, R-modules that contradict the result.