I follow up the prove from this YouTube video, to prove the completeness theorem, one of the step is to build from a consistent set $\Gamma$ to a set $\Gamma^*$ that satisfy:
- $\Gamma\subset\Gamma^*$
- $\Gamma^*$ is maximum consistent
- For every formula has the form $(\exists x_i\phi)\in\Gamma^* $ there is a constent witness, which means there exists a constent symbol $c$ so that $\phi(x_i;c)\in\Gamma^*$
The prove of this based on a lemma that:
For any consistent set $\Gamma$, and any $(\exists x_i\phi)\in\Gamma$, if there is a constent symbol $c$ that does not appear in any of the $\phi\in\Gamma$ then $\Gamma\cup\{\phi(x_i;c)\}$ is consistent
Thus we can line up all countable formulas $\phi_1,\phi_2,...$ so that constent symbol $c_i$ does not appear in $\Gamma$ and any of the $\phi_j, j<i$ and add them one by one in to the original $\Gamma$
However, if there is uncountable number of formulas, how to prove it?
What's being described here is the process of Henkinizing the theory $\Gamma$ where we extend to a larger theory $\Gamma'\supseteq \Gamma$ in a larger language $L'\supseteq L$ such that $\Gamma'$ remains consistent (provided $\Gamma$ is consistent) and satisfies the witness property: that if $\Gamma'\vdash \exists x \varphi$, then there is a constant symbol $c\in L'$ such that $\Gamma' \vdash \varphi(x/c).$
As I mentioned in the comments, there is a way to do this doesn't rely on an enumeration of formulas and doesn't require the axiom of choice regardless of the size of the language. (It is the next step where we extend a consistent theory to a maximal consistent theory that requires choice in general.)
We build the Henkinization as a countable sequence of extensions $L' = \bigcup_{n=0}^\infty L_n$ and $\Gamma' = \bigcup_{n=0}^\infty \Gamma_n$ where $L_n\subseteq L_{n+1}$ and $\Gamma_n\subseteq \Gamma_{n+1}.$
Start with $L_0 = L$ and $\Gamma_0 = \Gamma$ and proceed by recursion. Let $L_{n+1} = L_n \cup \{c^n_\varphi: \varphi\in \operatorname{form}(L_n)\},$ i.e. each $c^n_\varphi$ is a brand new constant for each $L_n$-formula $\varphi.$ Then we let $\Gamma_{n+1} = \Gamma_n\cup \{\exists x \varphi \to \varphi( x/c_{\varphi}^n): \varphi\in \operatorname{form}(L_{n+1})\}.$
Then we can show that if $\Gamma_n$ is consistent, then $\Gamma_{n+1}$ must also be, and so by induction each $\Gamma_n$ is consistent. It follows that $\Gamma'$ is consistent, since any inconsistency would need to come from a finite number of formulas, and thus from formulas all contained in one of the $\Gamma_n$'s.
It is easy to see that $\Gamma'$ has the witness property, again using the fact that proofs only use a finite number of axioms: If $\Gamma' \vdash \exists x \varphi$ then for some $n$, $\Gamma_n\vdash\exists x \varphi.$ Then, $(\exists x \varphi \to \varphi(x/c_\varphi^n)\in \Gamma_{n+1},$ so $\Gamma_{n+1}\vdash \varphi(x/c_\varphi^n).$
To show that $\Gamma_n$ being consistent implies $\Gamma_{n+1}$ is consistent, assume to the contrary that a $\Gamma_{n+1}$ is inconsistent. This inconsistency must be generated from $\Gamma_n$ and finitely many of the new sentences in $\Gamma_{n+1}$.
There will be fewer symbols flying around if we assume there is just a single sentence of the form $\exists x \varphi \to \varphi(x/c)$ that generates the inconsistency. If this is the case, then $\Gamma_n\vdash \exists x\varphi \land \lnot\varphi(x/c).$ But since $c$ doesn't occur in $\Gamma_n$, universal generalization gives $\Gamma_n \vdash \forall y (\exists x \varphi \land \lnot \varphi(x/y))$, where $y$ doesn't occur in $\varphi$, which is contradictory. So $\Gamma_n$ is inconsistent. This can be straightforwardly extended to the case with finitely many new sentences from $\Gamma_{n+1}.$