[proofplan] The forward direction interprets each ground term inside an arbitrary model of $T$ and uses that interpretation to define a satisfying propositional valuation for any finite family of ground instances. For the converse, propositional compactness gives one truth assignment satisfying all ground instances at once. From this assignment we build the Herbrand structure: its elements are ground terms, its functions are syntactic term-forming operations, and its predicates are read off from the truth assignment. A truth lemma for quantifier-free formulas then shows that every universal axiom of $T$ holds in this Herbrand structure. In the equality case, the ground equality and congruence axioms allow us to quotient ground terms by the equality relation before carrying out the same construction. [/proofplan]

[step:Turn a model of $T$ into propositional satisfying assignments for finite ground fragments]Assume first that $T$ has an $\mathcal L$-structure $\mathcal M$ such that $\mathcal M \models T$. Let $F \subset \operatorname{GI}(T)$ be a finite set of ground instances. For every ground term $t \in \operatorname{HU}(\mathcal L)$, let $t^{\mathcal M} \in M$ denote the value of $t$ in $\mathcal M$. Define a propositional truth assignment \begin{align*} v_F : \{A : A \text{ is a ground atomic } \mathcal L\text{-formula appearing in } F\} &\to \{\mathrm{true},\mathrm{false}\} \end{align*} by declaring, for each ground atomic formula $P(t_1,\dots,t_m)$, \begin{align*} v_F(P(t_1,\dots,t_m)) = \mathrm{true} \quad \Longleftrightarrow \quad \mathcal M \models P(t_1^{\mathcal M},\dots,t_m^{\mathcal M}). \end{align*} Since every member of $F$ is obtained from a universal sentence of $T$ by substituting ground terms, and since $\mathcal M$ satisfies that universal sentence, $\mathcal M$ satisfies each formula in $F$ under the interpretation of its ground terms. Therefore $v_F$ satisfies the propositionalization of every formula in $F$. Because $F$ was arbitrary, $\operatorname{GI}(T)$ is propositionally consistent.[/step]

[guided]Suppose $\mathcal M$ is a model of $T$. We want to show Herbrand consistency, so we fix an arbitrary finite set $F \subset \operatorname{GI}(T)$ and produce a propositional valuation satisfying it. Every ground term $t \in \operatorname{HU}(\mathcal L)$ has a definite value $t^{\mathcal M} \in M$ after interpreting the function and constant symbols in $\mathcal M$. We use these values to assign truth values to ground atomic formulas. Define \begin{align*} v_F : \{A : A \text{ is a ground atomic } \mathcal L\text{-formula appearing in } F\} &\to \{\mathrm{true},\mathrm{false}\} \end{align*} by \begin{align*} v_F(P(t_1,\dots,t_m)) = \mathrm{true} \quad \Longleftrightarrow \quad \mathcal M \models P(t_1^{\mathcal M},\dots,t_m^{\mathcal M}). \end{align*} This valuation is exactly the propositional shadow of the semantic truth in $\mathcal M$. If a formula in $F$ has the form $\varphi(t_1,\dots,t_n)$, then it came from a sentence \begin{align*} \forall x_1 \cdots \forall x_n\, \varphi(x_1,\dots,x_n) \in T. \end{align*} Since $\mathcal M \models T$, the formula $\varphi$ is true in $\mathcal M$ for every tuple of elements of $M$, and in particular for the tuple $(t_1^{\mathcal M},\dots,t_n^{\mathcal M})$. Hence the propositional formula corresponding to $\varphi(t_1,\dots,t_n)$ is satisfied by $v_F$. Thus every finite ground fragment is propositionally satisfiable.[/guided]

[step:Use propositional compactness to obtain one global ground truth assignment] Assume conversely that $\operatorname{GI}(T)$ is propositionally consistent. By the Propositional [Compactness Theorem](/theorems/2748) (citing a result not yet in the wiki: Propositional Compactness Theorem), there exists a truth assignment \begin{align*} v : \{A : A \text{ is a ground atomic } \mathcal L\text{-formula}\} &\to \{\mathrm{true},\mathrm{false}\} \end{align*} such that $v$ satisfies the propositionalization of every formula in $\operatorname{GI}(T)$. [/step]

[step:Build the Herbrand structure from the global truth assignment]Define an $\mathcal L$-structure $\mathcal H$ as follows. Its underlying set is \begin{align*} H := \operatorname{HU}(\mathcal L). \end{align*} For each constant symbol $c$ of $\mathcal L$, define $c^{\mathcal H} := c \in H$. For each $m$-ary function symbol $f$ of $\mathcal L$, define \begin{align*} f^{\mathcal H}: H^m &\to H, \\ (t_1,\dots,t_m) &\mapsto f(t_1,\dots,t_m). \end{align*} For each $m$-ary predicate symbol $P$ of $\mathcal L$, define \begin{align*} P^{\mathcal H} \subset H^m \end{align*} by \begin{align*} (t_1,\dots,t_m) \in P^{\mathcal H} \quad \Longleftrightarrow \quad v(P(t_1,\dots,t_m)) = \mathrm{true}. \end{align*} This defines a well-formed $\mathcal L$-structure because the interpretation of every function symbol maps tuples of ground terms to ground terms, and the interpretation of every predicate symbol is a relation on the appropriate Cartesian power of $H$.[/step]

[guided]We now construct a model directly from the syntax of the language. The domain is the Herbrand universe: \begin{align*} H := \operatorname{HU}(\mathcal L). \end{align*} Thus the elements of $\mathcal H$ are ground terms themselves. The interpretation of function symbols is syntactic. For an $m$-ary function symbol $f$, define \begin{align*} f^{\mathcal H}: H^m &\to H, \\ (t_1,\dots,t_m) &\mapsto f(t_1,\dots,t_m). \end{align*} This is well-defined because if $t_1,\dots,t_m$ are ground terms, then $f(t_1,\dots,t_m)$ is again a ground term. The interpretation of predicates is read from the global truth assignment $v$. For an $m$-ary predicate symbol $P$, define \begin{align*} P^{\mathcal H} \subset H^m \end{align*} by \begin{align*} (t_1,\dots,t_m) \in P^{\mathcal H} \quad \Longleftrightarrow \quad v(P(t_1,\dots,t_m)) = \mathrm{true}. \end{align*} So $\mathcal H$ is the structure whose functions freely generate terms and whose atomic facts are precisely those selected by the compactness-produced valuation $v$.[/guided]

[step:Prove the truth lemma for quantifier-free ground formulas] We claim that for every quantifier-free ground $\mathcal L$-formula $\psi$, \begin{align*} \mathcal H \models \psi \quad \Longleftrightarrow \quad v(\psi^\ast) = \mathrm{true}, \end{align*} where $\psi^\ast$ denotes the propositionalization of $\psi$. The proof is by induction on the construction of $\psi$. If $\psi$ is atomic, the equivalence is exactly the definition of the predicate interpretations in $\mathcal H$. The Boolean connective cases follow from the inductive hypothesis and from the fact that propositionalization preserves the truth tables for negation, conjunction, disjunction, implication, and biconditional. Hence the equivalence holds for all quantifier-free ground formulas. [/step]

[step:Verify every universal axiom in the Herbrand structure] Let \begin{align*} \sigma := \forall x_1 \cdots \forall x_n\, \varphi(x_1,\dots,x_n) \end{align*} be an arbitrary sentence of $T$, where $\varphi$ is quantifier-free. Let $t_1,\dots,t_n \in H$ be arbitrary elements of the Herbrand universe. Since $H = \operatorname{HU}(\mathcal L)$, each $t_i$ is a ground term. The ground instance \begin{align*} \varphi(t_1,\dots,t_n) \end{align*} belongs to $\operatorname{GI}(T)$, so its propositionalization is satisfied by $v$. By the truth lemma, \begin{align*} \mathcal H \models \varphi(t_1,\dots,t_n). \end{align*} Because $t_1,\dots,t_n$ were arbitrary elements of $H$, it follows that \begin{align*} \mathcal H \models \forall x_1 \cdots \forall x_n\, \varphi(x_1,\dots,x_n). \end{align*} Thus $\mathcal H \models \sigma$. Since $\sigma \in T$ was arbitrary, $\mathcal H \models T$, and therefore $T$ is satisfiable. [/step]

[step:Quotient by ground equality when equality is logical] Assume now that equality is included as a logical symbol, and suppose the propositional ground theory consisting of $\operatorname{GI}(T)$ together with all ground equality axioms and ground congruence axioms is propositionally consistent. By propositional compactness, choose a global satisfying truth assignment $v$ for this enlarged ground theory. Define a binary relation $\sim$ on $\operatorname{HU}(\mathcal L)$ by \begin{align*} s \sim t \quad \Longleftrightarrow \quad v(s = t) = \mathrm{true}. \end{align*} The ground reflexivity, symmetry, and transitivity axioms imply that $\sim$ is an [equivalence relation](/page/Equivalence%20Relation). For every $m$-ary function symbol $f$, the ground congruence axioms imply that if $s_i \sim t_i$ for $1 \le i \le m$, then \begin{align*} f(s_1,\dots,s_m) \sim f(t_1,\dots,t_m). \end{align*} Thus the interpretation \begin{align*} f^{\mathcal H}: (H/{\sim})^m &\to H/{\sim}, \\ ([t_1],\dots,[t_m]) &\mapsto [f(t_1,\dots,t_m)] \end{align*} is well-defined. For every $m$-ary predicate symbol $P$, the predicate congruence axioms imply that the relation \begin{align*} ([t_1],\dots,[t_m]) \in P^{\mathcal H} \quad \Longleftrightarrow \quad v(P(t_1,\dots,t_m)) = \mathrm{true} \end{align*} is well-defined on equivalence classes. Interpreting equality as actual equality on the quotient $H/{\sim}$, the same truth-lemma argument proves that every ground instance in the enlarged theory is true in $\mathcal H$. Therefore every universal sentence of $T$ is true in $\mathcal H$, and $T$ is satisfiable. Conversely, if $T$ has a model with equality interpreted as identity, the valuation induced by interpreting ground terms in that model satisfies every finite set of ground instances of $T$ and also satisfies the ground equality and congruence axioms. Hence the equality version has the same equivalence. [/step]