Using Herbrand's theorem to prove completeness in first-order logic I was wondering if one can use Herbrand's Theorem to reduce completeness of first-order logic to completeness of propositional logic. I was thinking of the following argument:
If a formula does not have a model then by Herbrand's theorem the set consisting of all ground instances of the formula is propositionally unsatisfiable. So by the completeness of propositional logic there must be a propositional proof deriving a contradiction from a set of ground instances of the formula. But we can turn it into a derivation of a contradiction from our initial formula by just adding enough substitution steps at the top to generate the ground instances used.
Does this argument work?
 A: Let $\vdash_0$ denote the syntactic consequence relation of classical propositional logic, and $\vdash$ the same for classical first-order logic.
Let $\Gamma$ range over sets of first-order sentences. You wish to prove the following. "if $\Gamma$ does not have a model, then you can use classical first-order logic to derive a contradiction from $\Gamma$ (symbolically, $\Gamma \vdash \bot$)". Here's how I read the argument you sketch:


*

*Assume $\Gamma$ does not have a model.

*We put all sentences of $\Gamma$ in prenex form, and extend the language with enough function symbols so that we can Skolemize/Herbrandize. Call the result $\Gamma_h$. Then $\Gamma_h$ still does not have a model.

*Applying Herbrand's theorem to 2, we get some finite subset $F$ of the ground instances of $\Gamma_h$ that does not admit a propositional valuation.

*Applying completeness for propositional logic to 3, we get that classical propositional logic derives a contradiction from $F$, or symbolically $F \vdash_{0} \bot$.

*Since we have $F \vdash_{0} \bot$, we clearly also have $F \vdash \bot$.

*But we have $\Gamma_h \vdash f$ for each $f \in F$, and therefore we must have $\Gamma_h \vdash \bot$.

*Since $\Gamma_h \vdash \bot$, we also have $\Gamma \vdash \bot$.


Is this argument correct? First, let's look at things that could potentially go wrong, but don't.


*

*Steps 5 and 6 are obvious, but if you want to make assurance double sure, you can prove the relevant results by induction on the structure of classical propositional logic proofs.

*Does step 4 work? Sure, the completeness theorem for classical propositional logic says exactly this.

*Do steps 2 and 7 work, and are they circular? I suppose you might be worried about this part. Short answer: yes, they work, and without circularity. You can show step 2 using purely semantic arguments, and step 7 using purely syntactic considerations (e.g. by inspecting sequent calculus proofs).
At this point you should feel reassured that your argument is by-and-large correct, modulo some details, such as a precise treatment of equality in the propositional case. (in fact, I'm fairly sure I've seen this exact argument in the literature, will try to find a reference later)
But there's one additional matter. Based on your comments, the "Herbrand's theorem" you wanted to use was the following: "if a set of sentences has a model, then its set of ground instances admits a propositional valuation". This is half of Herbrand's actual theorem, and in some sense it's the trivial half. For let $\mathcal{M}$ be the said model: then the desired valuation can be obtained by setting a ground instance $\varphi$ true precisely if $M \models \varphi$.
This half simply won't do. To go from step 2 to step 3, you need to use the other direction of Herbrand's theorem, "if a set of sentences does not have a model, then its set of ground instances does not admit a propositional valuation". The way we normally prove this should remind you of standard proofs (e.g. Henkin's) of the model existence theorem.
We will prove the contrapositive, i.e. if the set $\mathcal{F}$ of ground instances of $\Gamma_h$ admits a propositional valuation $v$, then $\Gamma_h$ has a model. Consider the set $T$ of all terms in the (extended) language. Interpret each function symbol $\mathtt{f}$ of arity $n$ as the set $f=\{ (x_1,\dots,x_n,y) \in T^{n+1} \:|\: y = \mathtt{f}(x_1,\dots,x_n) \}$. Interpret each relation symbol $\mathtt{R}$ of arity $n$ as the set $R = \{ (x_1,\dots,x_n) \in T^n \:|\: v(\mathtt{R}(x_1,\dots,x_n)) = \text{true} \}$. Call the resulting structure $\mathcal{M}$: since $\Gamma_h$ has no existential quantifiers, $\mathcal{M} \models \varphi$ precisely if $v(\varphi') = \text{true}$ for any ground instance $\varphi'$ of $\varphi \in \Gamma_h$, as can be verified by a simple induction on the structure of $\varphi$. Note that instead of $\mathcal{F}$, we could have started with all finite subsets of $\mathcal{F}$: if each of these admits a propositional valuation, then by propositional compactness so does the entire set $\mathcal{F}$.  I'd say this is the core of the argument: when the idea of constructing a model from the ground terms forms the core of all standard proofs of completeness, taking a detour via Herbrand might even start feeling like cruft.
