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$ set $f$ to whichever 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).
Examples
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~
How would you put the following formula
\[\forall x (P(x) \lor \forall x (Q(x)))\]
into rectified prenex form?
Deeper quantifiers override shallow ones, so we may rewrite as
\[\forall x (P(x) \lor \forall y Q(y))\]and then this becomes
\[\forall x \forall y (P(x) \lor Q(y))\]@example~
Convert
\[(\exists x(P(x) \lor Q(x))) \to (\exists x(P(x) \lor \exists x Q(x)))\]
into an equisatisfiable formula in Skolem form.
Rename variables to rectify the formula:
\[(\exists x (P(x) \lor Q(x))) \to (\exists y (P(y) \lor \exists z Q(z)))\]Expand the definition of $\to$:
\[\lnot (\exists x (P(x) \lor Q(x))) \lor (\exists y (P(y) \lor \exists z Q(z)))\]Move negation inwards:
\[(\forall x(\lnot(P(x) \lor Q(x)))) \lor (\exists y (P(y) \lor \exists z Q(z)))\]Take quantifiers out:
\[\forall x \exists y \exists z (\lnot (P(x) \lor Q(x)) \lor P(y) \lor Q(z))\]Replace existential quantifiers with functions:
\[\forall x(\lnot (P(x) \lor Q(x)) \lor P(f(x))\lor Q(g(x,y)))\]@example~ @exam~