Converting formulas to Skolem form.

Question

I am trying to convert the following two formulas to their Skolem form. I did my work, but not completely sure about them, and have some questions about some steps of Skolemization:

Formula 1: ∀x∃y∀z∃w (¬Q(f(x),y) ∧ P(a,w))

Step 1: ∀x∃y∀z∃w (¬Q(f(x),y) ∧ P(a, w)) (already rectified?)

Step 2: ∃x₁∀x ∃y ∃w (¬Q(f(x), y) ∧ P(x₁, w)) (rectified and closed + RPF?)

Step 3: ∀x (¬Q(f(x), g(x)) ∧ P(a, h(x)) (Skolem form?)

Formula 2: ∀z(∃y(P(x,g(y),z))∨¬∀xQ(x))

Step 1: ∀z(∃y(P(x, g(y), z)) ∨ ¬∀x₁Q(x₁)) (rectified?)

Step 2: ∃x∀z (∃y (P(x, g(y), z)) ∨ ¬∀x₁Q(x₁)) (rectified + closed?)

Step 3: ∃x∀z∃y∃x₁((P(x, g(y), z) ∨ ¬Q(x₁)) (RPF?)

Step 4: ∀z ((P(a), g(f(z)), z) ∨ ¬Q(h(z)) (Skolem?)

My first questions is, in the first formula, variable z does not occur in the formula, therefore can we directly remove it with its quantifier?

Other question is, when we bound the free variables, we bound them with an existential quantifier. Should we add the free variables' existential quantifier to the very beginning of the quantifier list? (for example, in the second formula, in step 2, we use existential quantifier to bound x, and I added ∃x to the beginning of the whole formula, is that the case?)

I'd be very happy if you could help me with this situations. Also, any feedback about the Skolemization process would be appreciated. Thank you very much in advance.

Answer 1

The usual presentations of first-order predicate logic syntactically allow vacuous quantification.Rewriting a formula deleting vacuously binding quantifier leaves the formula logically equivalent. Hence, it is appropriate to drop the quantifer $\forall z$ from the formula

$$\forall x\exists y\forall z\exists w(\neg Q(f(x),y)\wedge P(a,w))$$

---

As for the next question, suppose we have got a rectified formula $\phi(x_{1},x_{2}\ldots, x_{n}, y_{1}, y_{1}\ldots, y_{m})$ in which the variables $y_{k}$ occur free, that is, $\phi$ is already an open formula.

The next step is to produce a closed formula $\phi'$ that is satisfiably equivalent to $\phi$. So, we existentially quantify all the free variables and get

$$\exists y_{1}\exists y_{2}\cdots\exists y_{m}\phi(x_{1}, x_{2}\ldots, x_{n}, y_{1}, y_{2}\ldots, y_{m})$$

This is the proper procedure. Note that, by Skolemisation, we aim at equisatisfiability with the original formula, not the stricter logical equivalence with it. Thus, one could choose between alternatives in the procedure so long as they preserve satisfiability. It should be noted that there is a practice of treating free variables as universally quantified to drop all universal quantifiers later to get clausal normal form.

Answer 2

Yes, you can drop the $\forall z$ in the $\forall x \exists y \forall z \exists w (¬Q(f(x),y) \land P(a,w))$ formula

Also, no need to introduce an existential for a constant ... only to have it changed back by a constant later on. You can just leave the constant.

So, for the first one, you can go from

$$\forall x \exists y \forall z \exists w (¬Q(f(x),y) \land P(a,w))$$

to

$$\forall x \exists y \exists w (¬Q(f(x),y) \land P(a,w))$$

to

$$\forall x \exists y \exists w (¬Q(f(x),g(x)) \land P(a,h(x)))$$

The free variable $x$ in the second formula can likewise be kept alone .. having a free variable is typically treated more like a universal than an existential so you definitely don;t want to introiduce an existential for it. So here, you can go from

$$\forall z(\exists y(P(x,g(y),z))\lor \neg \forall x Q(x))$$

to

$$\forall z \exists y(P(x,g(y),z)\lor \exists x \neg Q(x))$$

to

$$\forall z \exists y(P(x,g(y),z)\lor \exists x_1 \neg Q(x_1))$$

to

$$\forall z \exists y \exists x_1 (P(x,g(y),z)\lor \neg Q(x_1))$$

to

$$\forall z (P(x,g(f(z)),z)\lor \neg Q(h(z)))$$