Does predicate logic's semidecidability follow from the completeness of predicate logic itself? Does predicate logic's semidecidability follow from the completeness of predicate logic itself (i.e., from Godel's completeness theorem)? From the fact that in predicate logic logical consequence entails derivability follows that every theorem in it has a proof. This is why you can successfully use "Godel numbering" in order to check for every sequence of formulas if it is a proof or not, and, if it is, "write down" the theorem it proves. Of course the decidability of the set of formulas of predicate logic is also a necessary condition.
Am I correct?
 A: Basically yes.
But your terminology is a bit wonky.
The theorems of a predicate logic formal system $S$ (in the usual usage) are the closed wffs (sentences) that are provable in your system $S$ from no premisses. Theoremhood in this sense is semidecidable, in the way you suggest. Enumerate all the strings of symbols, carve out those that are well-formed proofs of closed wffs from no premisses, and write down the final wffs -- that's all mechanical for a properly set-up formal system $S$, where we can decide what's a wff etc. And for this result, no appeal to completeness is needed.
The logical truths of a predicate logic formal system $S$ are the closed wffs which are true on all interpretations. Gödel's completeness theorem tells us that every logical truth is a theorem. The relatively trivial soundness result tells that every theorem is a logical truth. Hence, since we can effectively enumerate the theorems, we can effectively enumerate the logical truths, so the property of being a logical truth is semi-decidable, thanks to Gödel's result.
In sum, note that the claim "predicate logic is semidecidable" is not really clear, and is ambiguous between a claim about theoremhood and a claim about logical truth, only one of which depends on completeness.
