Must skolem functions depend on unused variables?

102 Views Asked by At

When converting formulas to CNF, we replace existentially quantified variables with Skolem functions that depend on surrounding universally quantified variables. For example, in

∀x ∃y p(x,y)

the value of y depends on the particular x, so y will be replaced by f(x).

What if the universally quantified variable was unused in the existentially quantified formula, i.e. is not a free variable in the body of the existential quantifier?

∀x ∃y p(y)

Can we simplify matters by ignoring x completely and just replacing y with a Skolem constant a?

1

There are 1 best solutions below

0
On BEST ANSWER

Basically yes, but as sticklers for details we shouldn't literally refer to $p({\bf a})$ as the Skolemization of $\forall x\exists y(p(y))$. Rather, we should say that $\forall x\exists y(p(y))$ is equivalent to $\exists y(p(y))$, and the Skolemization of the latter is $p({\bf a})$ for a fresh constant symbol ${\bf a}$.

This is a bit hair-splitting, but it is the technically accurate way to do things; in particular, there is a serious difference between adding a unary function symbol versus a constant (= nullary function) symbol to a language.