[proofplan] We reduce validity of $F$ to unsatisfiability of the universal Skolem form $U$ of $\neg F$. The ground instances of $U$ form a propositional theory once each ground atomic formula is regarded as a propositional variable. If no finite collection of ground instances is contradictory, propositional compactness gives a truth assignment satisfying all ground instances; from this assignment we build the Herbrand structure satisfying $U$. The desired finite disjunction is exactly the negation of such a finite contradictory family of ground instances. [/proofplan] [step:Reduce validity of $F$ to unsatisfiability of the universal Skolem form] Let \begin{align*} U := \forall y_1 \cdots \forall y_n\, B(y_1,\dots,y_n) \end{align*} denote the Skolemized universal $L'$-sentence obtained from $\neg F$. By the defining equisatisfiability property of Skolemization, the $L$-sentence $\neg F$ is satisfiable if and only if the $L'$-sentence $U$ is satisfiable. More precisely, every model of $\neg F$ expands to an $L'$-model of $U$ by interpreting the Skolem symbols as witnesses, and every $L'$-model of $U$ has an $L$-reduct satisfying $\neg F$. Therefore \begin{align*} F \text{ is valid} &\iff \neg F \text{ is not satisfiable} \\ &\iff U \text{ is not satisfiable}. \end{align*} [guided] The first move is to replace the original validity question by a satisfiability question. A sentence $F$ is valid exactly when its negation has no model. The Skolemization step is designed to preserve satisfiability, not logical equivalence in the original language. Thus we use the following precise fact: $\neg F$ is satisfiable as an $L$-sentence if and only if its Skolemized universal form \begin{align*} U := \forall y_1 \cdots \forall y_n\, B(y_1,\dots,y_n) \end{align*} is satisfiable as an $L'$-sentence. One direction comes from interpreting each new Skolem function symbol as a choice of witnesses for the existential quantifiers removed during Skolemization. The other direction comes from forgetting the interpretations of the new Skolem symbols: if an $L'$-structure satisfies the Skolemized sentence, then its reduct to the original language satisfies the prenex form of $\neg F$, and hence satisfies $\neg F$. Consequently the theorem becomes a statement about when the universal sentence $U$ has no model: \begin{align*} F \text{ is valid} &\iff \neg F \text{ is unsatisfiable} \\ &\iff U \text{ is unsatisfiable}. \end{align*} [/guided] [/step] [step:Rewrite a finite Herbrand disjunction as a finite inconsistency of ground instances] For each tuple \begin{align*} (t_1,\dots,t_n) \in H_{L'}^n, \end{align*} write $B(t_1,\dots,t_n)$ for the ground instance of $B$ obtained by substituting $t_j$ for $y_j$ for every $1 \leq j \leq n$. For fixed tuples $(t_{i,1},\dots,t_{i,n}) \in H_{L'}^n$, $1 \leq i \leq m$, the ground disjunction \begin{align*} \neg B(t_{1,1},\dots,t_{1,n}) \lor \cdots \lor \neg B(t_{m,1},\dots,t_{m,n}) \end{align*} is valid if and only if its negation \begin{align*} B(t_{1,1},\dots,t_{1,n}) \land \cdots \land B(t_{m,1},\dots,t_{m,n}) \end{align*} is unsatisfiable. Thus the theorem is equivalent to proving that $U$ is unsatisfiable if and only if some finite set of ground instances of $B$ is unsatisfiable. [/step] [step:Build a Herbrand model when every finite set of ground instances is satisfiable] Assume that every finite set of ground instances \begin{align*} B(t_1,\dots,t_n), \qquad (t_1,\dots,t_n) \in H_{L'}^n, \end{align*} is satisfiable. Let $\mathcal{A}$ be the set of all ground atomic $L'$-formulas. Regard each element of $\mathcal{A}$ as a propositional variable, and define the propositional theory \begin{align*} \Gamma := \{B(t_1,\dots,t_n) : (t_1,\dots,t_n) \in H_{L'}^n\}. \end{align*} Every finite subset of $\Gamma$ is satisfiable by hypothesis. By the [compactness theorem](/theorems/2748) for propositional logic (citing a result not yet in the wiki: Propositional Compactness Theorem), there exists a truth assignment \begin{align*} v: \mathcal{A} \to \{\mathrm{true},\mathrm{false}\} \end{align*} satisfying every formula in $\Gamma$. We construct an $L'$-structure $\mathcal{M}_v$ as follows. Its universe is \begin{align*} |\mathcal{M}_v| := H_{L'}. \end{align*} For each constant symbol $c$ of $L'$, define $c^{\mathcal{M}_v} := c \in H_{L'}$. For each $k$-ary function symbol $f$ of $L'$, define \begin{align*} f^{\mathcal{M}_v}: H_{L'}^k &\to H_{L'} \\ (s_1,\dots,s_k) &\mapsto f(s_1,\dots,s_k). \end{align*} For each $k$-ary relation symbol $R$ of $L'$, define \begin{align*} R^{\mathcal{M}_v} := \{(s_1,\dots,s_k) \in H_{L'}^k : v(R(s_1,\dots,s_k)) = \mathrm{true}\}. \end{align*} By induction on ground terms, every ground term $t \in H_{L'}$ is interpreted in $\mathcal{M}_v$ as itself. By induction on quantifier-free ground formulas, every quantifier-free ground $L'$-formula $C$ satisfies \begin{align*} \mathcal{M}_v \models C \iff v(C) = \mathrm{true}, \end{align*} where the value $v(C)$ is computed from $v$ by the usual Boolean truth tables. Since $v$ satisfies every member of $\Gamma$, we have \begin{align*} \mathcal{M}_v \models B(t_1,\dots,t_n) \end{align*} for every $(t_1,\dots,t_n) \in H_{L'}^n$. Every element of $|\mathcal{M}_v|$ is a closed $L'$-term. Hence, for arbitrary $a_1,\dots,a_n \in |\mathcal{M}_v|$, there are ground terms $t_1,\dots,t_n \in H_{L'}$ with $a_j=t_j$ for each $1 \leq j \leq n$. Therefore \begin{align*} \mathcal{M}_v \models B(a_1,\dots,a_n) \end{align*} for all $a_1,\dots,a_n \in |\mathcal{M}_v|$, and so \begin{align*} \mathcal{M}_v \models \forall y_1 \cdots \forall y_n\, B(y_1,\dots,y_n). \end{align*} Thus $U$ is satisfiable. [guided] We now prove the key contrapositive direction: if no finite set of ground instances contradicts itself, then the whole universal Skolem sentence has a model. Let $\mathcal{A}$ be the set of all ground atomic $L'$-formulas. Since $B$ is quantifier-free, every ground instance $B(t_1,\dots,t_n)$ can be viewed as a propositional formula whose propositional variables are the ground atoms appearing in it. Define \begin{align*} \Gamma := \{B(t_1,\dots,t_n) : (t_1,\dots,t_n) \in H_{L'}^n\}. \end{align*} The hypothesis says that every finite subset of $\Gamma$ is satisfiable. Therefore, by the compactness theorem for propositional logic (citing a result not yet in the wiki: Propositional Compactness Theorem), there is a truth assignment \begin{align*} v: \mathcal{A} \to \{\mathrm{true},\mathrm{false}\} \end{align*} such that every formula in $\Gamma$ evaluates to true under $v$. The next task is to turn this propositional truth assignment into a first-order structure. The natural universe is the Herbrand universe itself: \begin{align*} |\mathcal{M}_v| := H_{L'}. \end{align*} This set is nonempty because, by hypothesis, we added a fresh constant symbol if $L'$ had no closed term. Constants and function symbols are interpreted syntactically. Thus a constant symbol $c$ denotes the closed term $c$, and a $k$-ary function symbol $f$ is interpreted by the map \begin{align*} f^{\mathcal{M}_v}: H_{L'}^k &\to H_{L'} \\ (s_1,\dots,s_k) &\mapsto f(s_1,\dots,s_k). \end{align*} Relations are interpreted using the truth assignment. For a $k$-ary relation symbol $R$, put \begin{align*} R^{\mathcal{M}_v} := \{(s_1,\dots,s_k) \in H_{L'}^k : v(R(s_1,\dots,s_k)) = \mathrm{true}\}. \end{align*} This construction is arranged so that syntax and semantics agree on ground formulas. First, an induction on ground terms shows that every ground term $t \in H_{L'}$ denotes itself in $\mathcal{M}_v$. The base case is a constant symbol, which was interpreted as itself. The induction step follows from the definition of $f^{\mathcal{M}_v}$: if $s_1,\dots,s_k$ denote themselves, then $f(s_1,\dots,s_k)$ also denotes itself. Second, an induction on quantifier-free ground formulas shows that, for every quantifier-free ground formula $C$, \begin{align*} \mathcal{M}_v \models C \iff v(C) = \mathrm{true}. \end{align*} For atomic formulas this is exactly the definition of the relation interpretations. The Boolean connectives are handled by the ordinary truth tables for $\neg$, $\land$, $\lor$, and any other propositional connectives used in $B$. Since $v$ satisfies every formula in $\Gamma$, it follows that \begin{align*} \mathcal{M}_v \models B(t_1,\dots,t_n) \end{align*} for every tuple of ground terms $(t_1,\dots,t_n) \in H_{L'}^n$. But every element of the universe $|\mathcal{M}_v|$ is itself a ground term. Therefore, if $a_1,\dots,a_n \in |\mathcal{M}_v|$ are arbitrary, then they are closed terms in $H_{L'}$, and the corresponding ground instance gives \begin{align*} \mathcal{M}_v \models B(a_1,\dots,a_n). \end{align*} This is precisely the satisfaction condition for the universal sentence \begin{align*} \mathcal{M}_v \models \forall y_1 \cdots \forall y_n\, B(y_1,\dots,y_n). \end{align*} Thus $U$ is satisfiable. [/guided] [/step] [step:Derive the finite Herbrand contradiction from validity of $F$] Assume $F$ is valid. By the first step, $U$ is unsatisfiable. If every finite set of ground instances of $B$ were satisfiable, the previous step would produce a Herbrand structure satisfying $U$, contradicting the unsatisfiability of $U$. Hence there exist $m \geq 1$ and tuples \begin{align*} (t_{i,1},\dots,t_{i,n}) \in H_{L'}^n, \qquad 1 \leq i \leq m, \end{align*} such that the finite set \begin{align*} \{B(t_{i,1},\dots,t_{i,n}) : 1 \leq i \leq m\} \end{align*} is unsatisfiable. By the finite rewriting step, the disjunction \begin{align*} \neg B(t_{1,1},\dots,t_{1,n}) \lor \cdots \lor \neg B(t_{m,1},\dots,t_{m,n}) \end{align*} is quantifier-free valid. [/step] [step:Recover validity of $F$ from a finite valid Herbrand disjunction] Conversely, suppose there exist $m \geq 1$ and tuples \begin{align*} (t_{i,1},\dots,t_{i,n}) \in H_{L'}^n, \qquad 1 \leq i \leq m, \end{align*} such that \begin{align*} \neg B(t_{1,1},\dots,t_{1,n}) \lor \cdots \lor \neg B(t_{m,1},\dots,t_{m,n}) \end{align*} is quantifier-free valid. Its negation \begin{align*} B(t_{1,1},\dots,t_{1,n}) \land \cdots \land B(t_{m,1},\dots,t_{m,n}) \end{align*} is therefore unsatisfiable. If $U$ had an $L'$-model $\mathcal{M}$, then the universal quantifiers in $U$ would imply \begin{align*} \mathcal{M} \models B(t_{i,1},\dots,t_{i,n}) \end{align*} for every $1 \leq i \leq m$, because each $t_{i,j}$ denotes an element of $|\mathcal{M}|$. Thus $\mathcal{M}$ would satisfy the unsatisfiable finite conjunction above, a contradiction. Hence $U$ is unsatisfiable. By the first step, $\neg F$ is unsatisfiable, and therefore $F$ is valid. [/step]