This is a question from the chapter V (Completeness Theorem) of the UTM textbook of mathematical logic, written by H.-D. Ebbinghaus, J. Flum and W. Thomas.
The following exercise shows that the assumption “$\mathrm{free}(\Phi)$ is finite” in 2.1 is necessary.
2.5 Exercise. Let $S$ be arbitrary and let $\Phi = \{v_0\equiv t | t\in T^S\} \cup \{\exists v_0\exists v_1 \neg v_0\equiv v_1\}$. Show that $\mathrm{Con}\Phi$ holds and there is no consistent set in $L^S$ which includes $\Phi$ and contains witness.
(Theorem 2.1 shows that if $\mathrm{Con}\Phi$ and $\mathrm{free}(\Phi)$ is finite, then it can be extended to a consistent set $\Psi$ such that $\Psi$ contains witness)
I think that I can prove the second part by some sequent calculus. However, I am a little bit confused about why $\mathrm{Con}\Phi$ holds. Here is what I thought:
To prove $\mathrm{Con}\Phi$, it is sufficient to show that $\mathrm{Sat}\Phi$, thus I need to find an interpretation $\mathfrak{I}$ such that $\mathfrak{I}\models \Phi$. Suppose the domain $A$ of $\mathfrak{I}$ is a set of two distinct elements $a_0$ and $a_1$. Define the assignment of $\mathfrak{I}$ as $\beta(x)=a_0$ for all variable $x$. (edit: I should have also interpreted all functions to functions whose range is $\{a_0\}$ and all constants to $a_0$) From here it easy to learn that $\mathfrak{I}$ satisfies all formula from $\{v_0\equiv t | t\in T^S\}$. To show that $\mathfrak{I}\models \exists v_0\exists v_1 \neg v_0\equiv v_1$, from the definition of satisfaction relation we have
$$\mathfrak{I}\models \exists v_0\exists v_1 \neg v_0\equiv v_1$$
iff there is an $u_0\in A$ such that
$$\mathfrak{I}\frac{u_0}{v_0}\models \exists v_1 \neg v_0\equiv v_1 $$
iff there are $u_0, u_1\in A$ such that
$$(\mathfrak{I}\frac{u_0}{v_0})\frac{u_1}{v_1}\models \neg v_0\equiv v_1 $$
Set $u_0$ to $a_0$, and $u_1$ to $a_1$, and the $v_0$ in the last line became $a_0$ whereas $v_1$ is substituted to $a_1$. Thus $\mathfrak{I}\models \exists v_0\exists v_1 \neg v_0\equiv v_1$ does holds because $a_0\ne a_1$. (QED)
The problem is that it doesn’t seem to involve the fact that $\mathrm{free}(\Phi)$ is finite. Of course, $T^S$ can be infinite. But how does that influence the result? Did I miss anything?
EDIT: $\mathrm{free}(\phi)$ in this book means the free variables within the formula $\phi$. $T^S$ means the set of $S$-terms, where $S$ is the underlying symbol set, such as $c_0$, $fv_0$, etc. $L^S$ is the set of $S$-formulas, e.g. $\forall v_0 \neg v_0 \equiv v_0$.
Best Answer
Your proof of $\mathrm{Con}\,\Phi$ is missing a detail: $S$ may contain function symbols, so you need to say what you're doing with those. (You want e. g. $v_0 \equiv fv_5$ to hold in your interpretation, where $f \in S$ is a function symbol.)
(Edit: the above paragraph is wrong in two ways. First, you don't handle constants either; second, "detail" isn't the right word. It would be correct to say that in order to make your solution right, you need to 1) say what (the structure underlying) $\mathfrak{I}$ does with constants and function symbols and 2) prove by an induction on terms that $\mathfrak{I}$ is a model for all equations in $\Phi$. Maybe your "it is easy to see" means "it is an easy induction", which is true if you give the right interpretations, but you definitely need to give interpretations.)
Other than that, I see no problems with your proof. The fact that $\mathrm{free}(\Phi)$ is infinite doesn't matter for the first part of the exercise. It matters for the second part, and I point out below where exactly it matters. (Spoilered because it contains a fairly complete solution.)