Notes - Logic and Proof MT24, Skolemization
Flashcards
@Define what it means for a formula to be in Skolem form.
It is in the form
\[\forall x_1 \cdots \forall x_n \varphi^\ast\]where $\varphi$ is quantifier-free.
@State and @prove a proposition that lets you convert any logical formula into an equivalent one in Skolem form.
Suppose
\[\forall y_1 \forall y_1 \cdots \forall y_n \exists y_{n+1} \varphi^\ast\]is a sentence where $\varphi^\ast$ is quantifier free. Given a function symbol $f$ of arity $n$ that doesn’t occur in $\varphi$, write
\[\psi = \forall y_1 \forall y_2 \cdots \forall y_n \varphi^\ast [f(y_1, \ldots, y_n)/y_{n+1}]\]Then $\varphi$ and $\psi$ are equisatisfiable.
Proof: Given a model $\mathcal A$ for $\varphi$, obtain a model $\mathcal B$ for $\psi$ by interpreting the Skolem function $f$ by emulating the existential quantifier (given $y _ 1, \ldots, y _ n$, which value of $y _ {n+1}$ satisfied the formula?)
Likewise given a model $\mathcal B$ for $\psi$, obtain a model $\mathcal A$ for $\varphi$ by setting $y _ {n+1} = f(y _ 1, \ldots, y _ n)$.
@Justify why for every first-order formula $\varphi$, there is an equisatisfiable formula $\psi$ in Skolem form.
- Translate the formula into rectified prenex form (a formula is rectified if no variable occurs both bound and free and all quantifiers in formula refer to different variables)
- Repeatedly eliminate the outermost existential quantifier until an equisatisfiable formula in Skolem form is obtained (skolemization).
Convert
\[\forall x \exists y \forall z \exists w (\lnot P(a, w) \lor Q(f(x), y))\]
into an equisatisfiable formula in Skolem form.
@example~