29
$\begingroup$

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.

$\endgroup$
12
  • $\begingroup$ Compare with this previous question: mathoverflow.net/questions/9930/… $\endgroup$
    – Tom Church
    Jan 23, 2010 at 7:43
  • $\begingroup$ @TC: It does seem related, but even more ambitious. I should say that with my (not so extensive) knowledge of model theory it is not obvious how to formalize this decidability statement. An abelian category is not a "relational structure" in the sense of model theory: in particular, there is no underlying set. I would be interested to see a response which even gives a precise logical meaning to the question. $\endgroup$ Jan 23, 2010 at 9:00
  • 2
    $\begingroup$ You'd need to first be precise about which first-order axiomatization of "the theory of categories" you mean. Most mathematicians work from an axiomatization that starts with ZFC and adds more axioms about certain sets (which "are categories") existing. This is, of course, not the only way to do things: you can axiomatize categories directly. But how to do that is a matter of much debate; there is no clear agreement on which set of axioms to use (especially if you want to talk about Set and __Cat). $\endgroup$
    – Adam
    Jan 23, 2010 at 18:05
  • $\begingroup$ I was about to say the same thing that Adam said, but he said it first. $\endgroup$ Jan 23, 2010 at 18:47
  • 3
    $\begingroup$ Maybe I'm misreading the question, but it made perfect sense to me. The theory of categories has two types O (objects) and A (arrows), the dom,cod:A -> O, a map id:O -> A, and a (possibly partial) operation comp:A x A -> A for composition. The axioms are pretty obvious. It's a bit strange to have a partial composition, but it's not the first time I've seen that happen. I think the same applies to Abelian categories. $\endgroup$ Jan 23, 2010 at 19:16

3 Answers 3

37
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ A simpler answer: Any theory of categories that is "good enough" will also be able to axiomatize set theory, which means immediately that it's undecidable. $\endgroup$ Jan 23, 2010 at 18:51
  • 2
    $\begingroup$ That is true, but one could ask for decidability even in a very restricted kind of category, which may not be able to interpret set theory. (For example, the category of finite graphs with induced subgraph mappings.) My point was that once you have number-like objects that can be added and multiplied (and quantified over), then you will get undecidability. $\endgroup$ Jan 23, 2010 at 19:01
  • $\begingroup$ @Joel David Hamkins: Can you give me a reference for how to embed numbers/addition/multiplication into category-theoretical statements of the kind I or F. G. Dorais were describing? Thanks. $\endgroup$
    – aorq
    Jan 23, 2010 at 19:47
  • $\begingroup$ I edited my answer to explain it. $\endgroup$ Jan 23, 2010 at 21:08
  • $\begingroup$ Thanks for the edit, François! I'm sorry to have misspelled your name back then. $\endgroup$ Sep 13, 2012 at 22:32
23
$\begingroup$

This answer builds on those of F. G. Dorais and Joel David Hamkins to answer your "specific question", the question left open by them, namely whether the theory of abelian categories is decidable.

The answer is still no.

Even the following more limited family of problems is undecidable:

Given words $r, r_1,\ldots,r_m$ in $x_1,\ldots,x_n$ (i.e., each $r_i$ is a finite product of the $x_i$ and their inverses), decide whether it is true that whenever the $x_i$ are interpreted as automorphisms of an object $M$ in an abelian category, $r_1=\cdots=r_m=1_M$ implies $r=1_M$.

If the answer to the corresponding instance of the word problem for finitely presented groups is yes, then the answer to this abelian category question is yes. Conversely if the answer to the word problem instance is no, then we can construct the finitely presented group $G = \langle x_1,\ldots,x_n | r_1,\ldots,r_m \rangle$, form the group ring $\mathbb{Z}G$, and let $M$ be $\mathbb{Z}G$ as a module over itself, which shows that the answer to the abelian category question is no too.

So if there were an algorithm to decide this family of abelian category problems, there would also be an algorithm to decide the word problem for finitely presented groups. But P. S. Novikov proved in 1955 that the latter algorithm does not exist.

$\endgroup$
3
  • 1
    $\begingroup$ Excellent! A neat trick... $\endgroup$ Jan 24, 2010 at 0:32
  • $\begingroup$ Sorry, what is r? $\endgroup$ Jan 24, 2010 at 0:33
  • $\begingroup$ It's just another word, a relation for which you would like to decide whether it is a consequence of the others. (I just omitted the "r," in the boxed statement, but now it's there.) $\endgroup$ Jan 24, 2010 at 1:44
14
$\begingroup$

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).

$\endgroup$
8
  • $\begingroup$ Oh, it looks like you and I hit on the same idea. I was editing my answer when you posted yours! $\endgroup$ Jan 23, 2010 at 21:08
  • $\begingroup$ Yep, I think we got it right this time! I'm not sure about Abelian categories anymore. I don't use them enough to know what to do. $\endgroup$ Jan 23, 2010 at 21:18
  • $\begingroup$ Of course, abelian group theory is a decidable theory. But it seems that abelian category theory could be powerful enough for undecidability. $\endgroup$ Jan 23, 2010 at 21:25
  • 1
    $\begingroup$ @Pete: This problem arises with all theories, e.g. monster models are better thought of as proper classes than just very large sets. This poses no real problem, except for foundational theories such as Set Theory and Category Theory which have a deeper philosophical meaning. The "workaround" for Category Theory is exactly the same as that for Set Theory... $\endgroup$ Jan 23, 2010 at 22:06
  • 1
    $\begingroup$ @Pete: Very interesting question! We interpreted the question as whether the given first order theory is decidable, whether one can compute if a given statement is provable in the theory. By the Completeness Theorem, a statement is provable if and only if it holds in all set-sized categories, as you mention. I claim that in ZFC, this is the same as the set of validites in all class-sized categories, by the Reflection theorem: any statement true in a class, is also true in restriction of that class to a set, some large V_alpha. A similar Lowenheim-Skolem argument works with universes. $\endgroup$ Jan 23, 2010 at 22:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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