Is Haskell Curry's unconventional way of defining True(x) incorrect?
Correct in the sense that: Successor(Successor(Successor(0))) = 3 is correct and thus true and Successor(Successor(Successor(0))) = 7 is incorrect and thus untrue.
We begin by postulating a certain non void, definite class {E} of statements, which we call elementary statements...
The statements of {E} are called elementary statements to distinguish them from other statements which we may form from them or about them in the U language...
A theory (over {E}) is defined as a conceptual class of these elementary statements. Let {T} be such a theory. Then the elementary statements which belong to {T} we shall call the elementary theorems of {T}; we also say that these elementary statements are true for {T}. Thus, given {T}, an elementary theorem is an elementary statement which is true. A theory is thus a way of picking out from the statements of {E} a certain subclass of true statements…
The terminology which has just been used implies that the elementary statements are not such that their truth and falsity are known to us without reference to {T}.
Curry, Haskell 1977. Foundations of Mathematical Logic. New York: Dover Publications, 45
"... the elementary theorems of {T} ... are true for {T}."
In the middle of his third paragraph above Haskell Curry seems to be defining
semantic True({T}, x) on the basis of syntactic Theorem({T}, x). Is this correct?
There is no recursive structure in "A theory (over {E}) is defined as a conceptual class of these elementary statements. Let {T} be such a theory." It is merely a collection of statements. It is perhaps unfortunate that Curry uses the term "elementary theorems" which seems to have induced in you unintended baggage related to recursive definability. – Eric Towers
In its most generic sense a theorem of a formal system could be construed as the decision of membership of the membership algorithm of the recursive language defining this formal system.
A language L on Σ is said to be recursive if there exists a Turing machine M that accepts L and halts on every w in Σ+. In other words, a language is recursive if and only if there exists a membership algorithm for it. (Linz 1990:288).
Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company.
After extensive commenting, OP has established "Theorem({T},x)" to mean "there is a membership algorithm in the recursive language of U that decides membership of x in T."
The answer to your question is: No. Curry makes no requirement that membership in {T} is decidable in U or in {E}.
Curry follows the standard (model theoretic for first-order logics) method of asserting a theory, defined as a particular collection of sentences, to be true, then determining whether that theory is satisfiable by some model. (Satisfiability, completeness, and consistency relate this model theoretic method to the recursive decision scheme you have in mind.)