= Solution
The intended <closed-term witness property for quantifier-free existential sentences> needs at least one closed term. Under this hypothesis, suppose the set $\Gamma=\{\neg\phi(t):t\text{ a closed term}\}$ were consistent. By the <Godel completeness theorem>, it has a model $M$. Take the <substructure> $M_0$ whose elements are the interpretations of closed terms. It is nonempty and closed under every function symbol. Atomic formulas and their negations have the same truth values in $M_0$ as in $M$, and induction extends this to every <quantifier-free formula>.
The provable sentence $\exists x\,\phi(x)$ is true in $M_0$ by soundness. Its witness is $t^{M_0}$ for some closed term $t$, so $M\models\phi(t)$, contradicting $M\models\Gamma$. Hence $\Gamma$ is inconsistent. The <compactness theorem> gives a finite inconsistent subset, so completeness and classical propositional reasoning yield
$$
\boxed{\vdash\phi(t_1)\lor\cdots\lor\phi(t_n).}
$$
Without a constant or nullary function, the printed assertion is false as written: in the equality-only language there are no closed terms, but $\exists x\,(x=x)$ is provable. Then $\Gamma$ is empty and consistent. One may repair the usual theorem by assuming a nonempty set of closed terms or adjoining a fresh constant; the latter proves a witness disjunction in the enlarged language, not the missing closed terms in the original one.
Back to article page
