Show that Skolemization preserves satisfiability

98 Views Asked by At

Consider replacing an existential quantifier with a $n$-ary Skolem function symbol $f$ and suppose that there is an $\mathcal{M}$ model that: $\mathcal{M} \models \forall x_1\dots \forall x_n \exists y P(x_1, \dots, x_n, y)$. How can I show there is an $\mathcal{M}'$ interpretation such that:

$\mathcal{M}' \models \forall x_1 \dots \forall x_n P(x_1, \dots, x_n, f(x_1, \dots, x_n))$.