[proofplan] Validity of $F$ makes $\neg F$ unsatisfiable. The syntactic transformations used in refutation search preserve unsatisfiability in the appropriate equisatisfiable sense, so the Skolemized universal clause set $\mathcal{C}$ has no model. [Herbrand's theorem](/theorems/2359) then converts this first-order unsatisfiability into propositional unsatisfiability of finitely many ground Herbrand instances. Finally, propositional completeness gives a ground contradiction, and the lifting property for first-order resolution turns the ground refutation into a first-order refutation. [/proofplan] [step:Pass from validity of $F$ to unsatisfiability of its negation] Let $\mathcal{L}$ be the original first-order signature of $F$. Since $F$ is valid, every $\mathcal{L}$-structure $\mathcal{M}$ satisfies $F$. Hence no $\mathcal{L}$-structure satisfies $\neg F$, so $\neg F$ is unsatisfiable. [guided] The refutation search begins with $\neg F$, so the first task is to translate validity into unsatisfiability. Validity of $F$ means that for every $\mathcal{L}$-structure $\mathcal{M}$, \begin{align*} \mathcal{M} \models F. \end{align*} Therefore there is no $\mathcal{L}$-structure $\mathcal{M}$ for which $\mathcal{M} \models \neg F$. This is exactly the statement that $\neg F$ is unsatisfiable. [/guided] [/step] [step:Transfer unsatisfiability to the Skolemized clause set] Let $\mathcal{L}_{\mathrm{Sk}}$ denote the signature obtained from $\mathcal{L}$ by adjoining the Skolem function symbols introduced during Skolemization. Let $\mathcal{C}$ be the resulting set of universal clauses, and let $\bigwedge \mathcal{C}$ denote the universal closure of their conjunction. Prenexing preserves logical equivalence, conversion of the quantifier-free matrix into conjunctive clause form preserves logical equivalence, and [Skolemization preserves satisfiability](/theorems/4654) and unsatisfiability for the refutation task: $\neg F$ is satisfiable over $\mathcal{L}$ if and only if $\bigwedge \mathcal{C}$ is satisfiable over the expanded signature $\mathcal{L}_{\mathrm{Sk}}$. Since $\neg F$ is unsatisfiable, $\mathcal{C}$ has no $\mathcal{L}_{\mathrm{Sk}}$-model. [guided] We must check that the syntactic preprocessing used by refutation search has not changed the satisfiability question. Prenexing replaces $\neg F$ by a logically equivalent prenex sentence. Converting the quantifier-free matrix into conjunctive normal form also preserves logical equivalence. Skolemization is slightly different: it need not preserve literal equivalence in the original signature, but it does preserve satisfiability after expanding the signature by the new Skolem function symbols. Thus, if the Skolemized universal clause set $\mathcal{C}$ had an $\mathcal{L}_{\mathrm{Sk}}$-model, forgetting the interpretations of the new Skolem symbols would give an $\mathcal{L}$-model witnessing satisfiability of the original prenex form of $\neg F$. Conversely, any model of the existential requirements in the prenex form can be expanded by choosing Skolem functions. Therefore $\neg F$ is satisfiable exactly when $\mathcal{C}$ is satisfiable over the Skolem extension. Since the previous step proved that $\neg F$ is unsatisfiable, the Skolemized clause set $\mathcal{C}$ is also unsatisfiable. [/guided] [/step] [step:Apply Herbrand's theorem to obtain finitely many contradictory ground instances] Let $\mathcal{L}_{H}$ denote $\mathcal{L}_{\mathrm{Sk}}$ if $\mathcal{L}_{\mathrm{Sk}}$ has at least one constant symbol; otherwise let $\mathcal{L}_{H}$ be the expansion of $\mathcal{L}_{\mathrm{Sk}}$ by one fresh constant symbol. Let $H(\mathcal{L}_{H})$ be the Herbrand universe of $\mathcal{L}_{H}$. By construction $H(\mathcal{L}_{H})$ is nonempty. A ground substitution over $H(\mathcal{L}_{H})$ is a map sending each variable in a clause to a ground term in $H(\mathcal{L}_{H})$. By Herbrand's theorem for universal clause sets (citing a result not yet in the wiki: Herbrand's Theorem), an unsatisfiable universal clause set has a finite propositionally unsatisfiable set of ground instances. Since $\mathcal{C}$ is unsatisfiable and $H(\mathcal{L}_{H})$ is nonempty, there exist clauses $C_1,\dots,C_m \in \mathcal{C}$ and ground substitutions $\sigma_1,\dots,\sigma_m$ over $H(\mathcal{L}_{H})$ such that \begin{align*} \Gamma := \{C_1\sigma_1,\dots,C_m\sigma_m\} \end{align*} is propositionally unsatisfiable. [guided] At this point all quantifiers in $\mathcal{C}$ are universal. Thus every clause in $\mathcal{C}$ represents all of its ground instances. The Herbrand universe $H(\mathcal{L}_{H})$ is the set of all ground terms built from the constants and function symbols of $\mathcal{L}_{H}$. If $\mathcal{L}_{\mathrm{Sk}}$ has no constant symbol, the definition of $\mathcal{L}_{H}$ adds one fresh constant; this is the standard harmless convention ensuring that ground terms exist and is exactly the convention used in the theorem statement. Herbrand's theorem for universal clause sets says precisely that first-order unsatisfiability of $\mathcal{C}$ is witnessed at the ground level: if no structure satisfies $\mathcal{C}$, then some finite family of ground instances of clauses from $\mathcal{C}$ is already propositionally inconsistent. Applying that theorem to the unsatisfiable set $\mathcal{C}$ in the language $\mathcal{L}_{H}$ gives clauses $C_1,\dots,C_m \in \mathcal{C}$ and ground substitutions $\sigma_1,\dots,\sigma_m$ over $H(\mathcal{L}_{H})$ such that the finite ground clause set \begin{align*} \Gamma := \{C_1\sigma_1,\dots,C_m\sigma_m\} \end{align*} has no truth assignment satisfying all of its clauses. This is the desired finite Herbrand contradiction. [/guided] [/step] [step:Derive a propositional contradiction from the finite ground clause set] The set $\Gamma$ is a finite set of ground clauses. Since it is propositionally unsatisfiable, completeness of propositional clause refutation (citing a result not yet in the wiki: Completeness of Propositional Resolution) gives a finite derivation of the empty clause from $\Gamma$. [guided] The clauses in $\Gamma$ contain no variables. Therefore each ground atom appearing in $\Gamma$ can be treated as an atomic proposition. The statement that $\Gamma$ is propositionally unsatisfiable means that no Boolean valuation of these ground atoms makes every clause in $\Gamma$ true. Completeness of propositional clause refutation says that every finite unsatisfiable set of propositional clauses has a finite derivation of the empty clause. Applying this result to the finite ground clause set $\Gamma$ gives a finite propositional contradiction. [/guided] [/step] [step:Lift the ground contradiction to first-order resolution] Each clause in $\Gamma$ is an instance of a clause in $\mathcal{C}$. By the lifting property for first-order resolution with factoring (citing a result not yet in the wiki: [Lifting Lemma](/theorems/2437) for Resolution), every ground resolution refutation from instances of clauses in $\mathcal{C}$ is the ground instance of a first-order resolution refutation from $\mathcal{C}$. Hence first-order resolution derives the empty clause from $\mathcal{C}$ in finitely many steps. Combining the preceding steps, refutation search on the Skolemized clause form of $\neg F$ has a finite ground contradiction among Herbrand instances, and the corresponding first-order resolution search has a finite refutation. [guided] The finite contradiction obtained above is ground: it uses only particular Herbrand instances of clauses from $\mathcal{C}$. First-order resolution is designed to avoid enumerating all such ground instances by using unifiers. The lifting property states that if a contradiction can be derived by resolving ground instances of first-order clauses, then there is a corresponding first-order resolution derivation whose substitutions instantiate to that ground derivation. Since every member of $\Gamma$ has the form $C_i\sigma_i$ with $C_i \in \mathcal{C}$, the hypotheses of the lifting property apply. Therefore the ground refutation from $\Gamma$ lifts to a finite first-order resolution refutation from the original Skolemized clause set $\mathcal{C}$. This proves both the finite Herbrand basis claim and the refutation-search consequence. [/guided] [/step]