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.
Goedel did indeed use the Chinese remainder theorem in his proof of the Incompleteness theorem. This was used in what you describe as the `boring' part of the proof, the arithmetization of syntax. Contemporary researchers often agree with your later assessment, however, that the arithmetization of syntax is profound. This is the part of the proof that reveals the self-referential nature of elementary number theory, for example, since in talking about numbers we can in effect talk about statements involving numbers. Ultimately, we arrive in this way at a sentence that asserts its own unprovability, and this gives the Incompleteness Theorem straight away.
But there are other coding methods besides the Chinese Remainder theorem, and not all of them involve primes directly. For example, the only reason Goedel needed CRT was that he worked in a very limited formal language, just the ring theory language. But one can just as easily work in a richer language, with all primitive recursive functions, and the proof proceeds mostly as before, with a somewhat easier time for the coding part, involving no primes. Other proofs formalize the theory in the hereditary finite sets HF, which is mutually interpreted with the natural numbers N, and then the coding is fundamentally set-theoretic, also involving no primes numbers especially.
Best Answer
According to the following paper:
Carlos R. Videla, On the constructible numbers, Proceedings of the American Mathematical Society Vol. 127, No. 3 (Mar., 1999), pp. 851-860.
The problem has remained open at least until 1999. I think the problem is still open. In the above paper the author proves that the ring of constructible algebraic integers is first-order definable in the field of constructible numbers. The author hopes that $\mathbb{Z}$ should be definable in the ring of constructible algebraic integers and therefore his result would be a partial result towards resolving the problem negatively.