Revisions - MathOverflow

Return to Answer

spelling

view source

edited Sep 13 at 21:13

Thanks for clarifying your question. The formulation that you and Dorias 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 sⁱ also commutes with s^j. 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.

added 981 characters in body

view source

edited Jan 23 2010 at 21:05

Joel David Hamkins
75.3k●7●187●343

The

Thanks for clarifying your questionof whether a theory or problem is decidable only makes sense when there is a precise decision problem under consideration. Thus, there should be The formulation thatyou and Dorias give seems perfectly reasonable. You have aclear criterion first order language for what counts as a proper questioncategory theory, which must be finitary in naturewhere you canquantify over objects and morphisms, you can composemorphisms appropriately and an unambiguous meaning for when an answer you can express that a givenobject is correctthe initial or terminal object of a given

You have In this language, one can describe various finitediagrams, express whether or not really told us exactly which decision problem you intend to considerthey are commutative, andI believe so on. In particular, one can express that there are several reasonable interpretationscomposition isassociative, totally different etc. and describe what it means to be acategory in naturethis way.An important part of the problem

The question now becomes: is this theory decidable? Inother words, as Pete mentionsis there a computable procedure to determine,given an assertion in this language, whether it holds inall categories?

The answer is formalizing your question preciselyNo.

One way to interpret your question see this is to ask about show even more: one cannot evendecide whether a specific categorygiven statement is true is true in allcategories having only one object. For this, we may consider The reason is that grouptheory is not a category as consisting of decidable theory. There is no computableprocedure to determine whether a bunch of objects, and for any pair given statement in thefirst order language of objects, we may have some morphisms between them, group theory is true in all groups.But the one-point categories naturally include all thegroups (and we have an operation for composing morphisms. This can be viewed define in a single statement in thecontext category-theoretic language exactly what it takes for thecollection of ordinary model theory as a multi-sorted model, with two sorts: objects and morphisms . We have a relation R(a,b,f) which says on that f is a morphism from object a to object b, and we have the composition operation on morphisms. In this way, any given category can be viewed as a first order structuregroup).In Thus, if we could decide category theory, then we coulddecide the first order language translations of this structure, one can describe any given finite diagramthe group theory questions intocategory theory, and ask whether a given diagram commuteswe would be able to decide grouptheory, and so onwhich we can't. (Infinitary diagrams would not seem Contradiction.

The fundamental obstacle to be expressible.)

Another sense One can identify thecollection of your questiontranslations, howeveras exactly those that commutewith s = translation-by-1. Then, one can define addition ascomposition (i.e. addition of exponents) and the dividesrelation is definable by: i divides j iff anything thatyou don't want to consider just one commutes with sⁱ also commutes withs^j. And so on.

added 68 characters in body

view source

edited Jan 23 2010 at 18:43

Joel David Hamkins
75.3k●7●187●343

The question of whether a theory or problem is decidable only makes sense when there is a precise decision problem under consideration. Thus, there should be a clear criterion for what counts as a proper question, which must be finitary in nature, and an unambiguous meaning for when an answer is correct.

You have not really told us exactly which decision problem you intend to consider, and I believe that there are several reasonable interpretations, totally different in nature. An important part of the problem, as Pete mentions, is formalizing your question precisely.

One way to interpret your question is to ask about a specific category. For this, we may consider a category as consisting of a bunch of objects, and for any pair of objects, we may have some morphisms between them, and we have an operation for composing morphisms. This can be viewed in the context of ordinary model theory as a multi-sorted model, with two sorts: objects and morphisms. We have a relation R(a,b,f) which says that f is a morphism from object a to object b, and we have the composition operation on morphisms. In this way, any given category can be viewed as a first order structure. In the first order language of this structure, one can describe any given finite diagram, and ask whether a given diagram commutes, and so on. (Infinitary diagrams would not seem to be expressible.)

In this sense of your question, you are asking whether the theory of a fixed category is decidable, whether thee there is an algorithm to decide the truth of such statements in that category alone, in the language I described. And the answer here is clearly that some categories will be decidable and some will not. If the category is trivial (or finite), then the decision problem will of course be decidable. If the category is even a little bit nontrivial, for examplehowever, if it has number-like objects, for example, that allow you to identify a substructure that simulates the natural numbers, with addition and multiplication (much less would do), then the theory of the category in this sense will interpret arithmetic and therefore be undecidable. The basic phenomenon is that once you are able to speak of numbers, and add and multiply and quantify over the numbers, then you get huge undecidability.

Another sense of your question, however, is that you don't want to consider just one category, but you want a lot whole collections of categories (perhaps of a certain type), and you want to consider functors and whatnot between them. Here, the category theorists will have to set up the decision problem more precisely. But again, if your context has much substance to it at all, then you will likely again have number-like objects that you can add and multiply and quantify over. In this case, your decision problem will again interpret the decision problem for arithmetic, and this is undecidable.

view source

answered Jan 23 2010 at 18:38

Joel David Hamkins
75.3k●7●187●343

In this sense of your question, you are asking whether the theory of a fixed category is decidable, whether thee is an algorithm to decide the truth of such statements in that category alone. And the answer here is clearly that some categories will be decidable and some will not. If the category is trivial (or finite), then the decision problem will be decidable. If the category is even a little bit nontrivial, for example, if it has number-like objects that allow you to identify a substructure that simulates the natural numbers, with addition and multiplication (much less would do), then the theory of the category in this sense will interpret arithmetic and therefore be undecidable. The basic phenomenon is that once you are able to speak of numbers, and add and multiply and quantify over the numbers, then you get huge undecidability.

Another sense of your question, however, is that you don't want to consider just one category, but you want a lot of categories (perhaps of a certain type), and you want to consider functors and whatnot between them. Here, the category theorists will have to set up the decision problem more precisely. But again, if your context has much substance to it at all, then you will likely have number-like objects that you can add and multiply and quantify over. In this case, your decision problem will again interpret the decision problem for arithmetic, and this is undecidable.