I would like to know if the set of undecidable problems (within ZFC or other standard system of axioms) is decidable (in the same sense of decidable). Thanks in advance, and I apologize if the question is too basic.
[Math] Is the set of undecidable problems decidable
lo.logicmodel-theory
Related Solutions
The mortality problem for $3\times 3$ matrices: given a finite set $F$ of $3\times 3$ integer matrices, decide whether the zero matrix is a product of members of $F$ (with repetitions allowed). This was proved unsolvable by Michael Paterson, Studies in Applied Mathematics 49 (1970), 105--107, doi: 10.1002/sapm1970491105.
The corresponding problem for $2\times 2$ matrices is apparently still open.
Edit (11 September 2016): The problem for $2\times 2$ matrices is apparently still open, despite the solution of a seemingly similar problem mentioned in Igor Potapov's answer below.
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.
Related Question
- Using Consistency to Create New Axioms in Set Theory – Logic
- [Math] How to think like a set (or a model) theorist.
- Difference Between ZFC+Grothendieck, ZFC+Inaccessible Cardinals, and Tarski-Grothendieck Set Theory
- [Math] Are the two meanings of “undecidable” related
- Spectral Gap – How Undecidable Is It?
Best Answer
No, in fact the situation is even worse than that. The set $T$ of all (Gödel codes for) sentences that are provable from ZFC is computably enumerable; the set $F$ of all sentences that refutable from ZFC is also computably enumerable. These two sets $T$ and $F$ form an inseparable pair: $T \cap F = \varnothing$ but there is no computable set $C$ such that $T \subseteq C$ and $F \cap C = \varnothing$.
In other words, there is no finite algorithm that can reliably tell whether a sentence is "not provable" or "not refutable." This is much weaker than asking for an algorithm to tell us whether a sentence is independent or not (in which case we could determine whether it is provable or refutable by waiting until it enters $T$ or $F$).
This remains true if ZFC is replaced by PA and some still weaker theories.