Formalizing the Completeness Theorem given languages of infinite cardinality

Question

I am reading Kunen's books on set theory and logic. In his approach, the metatheory is finitistic (which can be approximated in PRA).

This implies that in the finitistic metatheory, one can do formal logic, and come up with finite languages $\mathcal{L}$, describe finite formulas and finite proofs.

However, Kunen stated that once one deals with infinite objects, then the theorems are "formalized in ZFC" since the finitistic metatheory does not allow working with infinite objects such as $\omega$.

Given $\mathcal{L}=\{\epsilon\}$, let $\Lambda$ be a set of sentences of $\mathcal{L}$. Working in ZFC, we can prove the Completeness Theorem:

$$ ZFC \vdash \text{Con}_{\vdash}(\Lambda) \leftrightarrow \text{Con}_{\models}(\Lambda) $$

where $\text{Con}_{\vdash}(\Lambda)$ is syntactic consistency and $\text{Con}_{\models}(\Lambda)$ is semantic consistency.

Since $\mathcal{L}=\{\epsilon\}$ is finite, $\Lambda$ is countable, and the set of proofs and formulas of $\mathcal{L}$ is countable... Hence, the hypothesis $\text{Con}_{\vdash}(\Lambda)$ makes sense in the finitistic metatheory using infinite schemas and the countable ZFC Axioms, i.e. for instance, given finite sets $\varphi_1, \varphi_2$, we can state that there is no set which is a finite proof $\Phi$ of a contradiction from $\varphi_1, \varphi_2$. Since $\varphi_1, \varphi_2$ are finite and in HF, they can be mapped to their corresponding metatheory formulas using ZFC (Kunen uses the weaker TST) and one can say that there is really no metatheoretic proof that gives a contradiction from metatheoretic formulas $\varphi_1, \varphi_2$. I think that $\text{Con}_{\vdash}(\Lambda)$ can be viewed as an abbreviation without having to use infinite sets.

However, what if $|\mathcal{L}|$ is some uncountable cardinal ? In the finitistic metatheory, I think that $\text{Con}_{\vdash}(\Lambda)$ no longer makes sense since we can no longer do the mapping from infinite sets to metatheoretic formulas as the metatheory is finitistic. Does "formalizing within ZFC" in this case mean that when we say $\text{Con}_{\vdash}(\Lambda)$, there is an implicit encoding of $\mathcal{L}$ into an infinite set along with an encoding of the formal logic for proofs and $\vdash$ so that $\text{Con}_{\vdash}(\Lambda)$ involves such an encoding of the formal logic and of the notion of proof in terms of sets, and we no longer use the metatheoretic notion of $\vdash$ ?

• Emil Jeřábek: What is the point of the question? You formalize the completeness throrem in ZFC, not in a finitistic metatheory. Even if the language is finite, a finitistic metatheory cannot deal with $\models$. Kunen says just as much. So what are you trying to achieve?
• Link L: @EmilJeřábek, if $\mathcal{L}$ is of uncountable cardinality, are we still justified to use the metatheoretic $\vdash$ to state the notion $\text{Con}_{\vdash}$ ?
• Emil Jeřábek: Again: we are formalizing the completeness theorem in ZFC, not in the outer metatheory. So we are NOT using metatheoretic $\vdash,ドル or metatheoretic anything for that matter, to state it, irrespective of whether the language is finite or infinite or uncountable. It makes no sense. The whole statement uses only notions defined in ZFC.
• Link L: @EmilJeřábek, ok, it makes sense, I will then treat $\vdash$ as a set
• Jean Abou Samra: I think you are confusing $\mathsf{ZFC} \vdash (\forall \mathcal{L}, \mathsf{Con}_\vdash(\mathcal{L}) \iff \mathsf{Con}_\models(\mathcal{L}))$ with $\forall \mathcal{L}, \mathsf{ZFC} \vdash (\mathsf{Con}_\vdash(\mathcal{L}) \iff \mathsf{Con}_\models(\mathcal{L}))$. The latter doesn't make sense.