Is it a weakness of Henkin's completeness proof that consistency is undecidable? An important step in Henkin's proof of the completeness of first-order logic is the construction of maximally consistent sets of sentences from the original set $\Gamma$. In order to do this, he describes a series of steps whereby we add the next (from an arbitrary numbering) sentence that is consistent with the set we have accumulated thus far ($\Gamma_{0i}$), to produce the next set ($\Gamma_{0i+1}$).
What bothers me about this is that there is no decision procedure for determining whether a sentence is consistent with a set of sentences. So are we supposed to consult some oracle to determine whether we can add the next sentence to the set?
 A: This is indeed a real thing. However, I wouldn't call it a weakness, just a feature of the topic: non-computable things are more relevant here than they are in many other contexts.
Briefly, here's the situation. Henkin's proof breaks into multiple pieces:

*

*If $T$ is a complete consistent first-order theory with the witness property (also called the Henkin property), then the term structure $Term(T)$ of $T$ is in fact a model of $T$.


*Every consistent theory $S$ is (possibly after expanding the language appropriately) a subtheory of a theory $T$ which is consistent, complete (with respect to the new language) and has the witness property.
The first step is totally "effective:" we can build a copy of $Term(T)$ computably from $T$ assuming $T$ has the desired hypotheses. However, the second step is not effective, and indeed the whole result is not:

There is a consistent computable theory with no computable model.

For example, this is a consequence of Tennenbaum's theorem. Add a new constant symbol $c$ to the usual language of first-order Peano arithmetic $\mathsf{PA}$, and consider the new theory $$A=\mathsf{PA}\cup\{c>1+...+1\mbox{ ($n$ times)}: n\in\mathbb{N}\}.$$ The theory $A$ is satisfiable by compactness, but by Tennenbaum it can have no computable model. *(We can also get a single sentence which has a model but has no computable model with a bit more thought, so the "infinitely many axioms" thing is really superficial here.)
Put another way, the completeness theorem is "classically true but computably false." But (to my mind anyways) non-computable things aren't particularly ontologically mysterious: some things are computable, some things aren't, and the appearance of non-computable objects in reasonably concrete arguments should be construed not as evidence that those arguments are flawed but rather that those objects are less inaccessible than they may at first appear.
If this sort of thing interests you, you should look up reverse mathematics: this is basically the study of how much "computational power" different theorems of mathematics have. From the perspective of reverse mathematics, the completeness theorem sits at the same level as (for example) the theorem that $[0,1]$ is compact or the theorem that every infinite binary tree has an infinite path.
