1
$\begingroup$

I'm following along an example that takes a formula and converts it into Skolem Normal Form.

In one of the steps, the formula goes $\text{from: }\forall x~P(x) ~\wedge~ \exists x~\forall y~\exists z~\neg Q(x,y,z)\\\quad\text{to: }\exists x~\forall y~\exists z~(P(x)\wedge\neg Q(x,y,z))$

Why did the existential quantifier take preference over the universal quantifier? Aren't they two different scopes and then ∃x,x be replaced by another variable?

| cite | improve this question | |
$\endgroup$
3
$\begingroup$

That is indeed really strange. In fact, not just strange, but these are not equivalent: If you have two objects $a$ and $b$ in your domain, and only $a$ has property $p$, and nothing stands in the $Q$ relationship, then $\exists x\forall y\exists z(Px\land\neg Qxyz)$ is true but $ \forall xPx\land\exists x\forall y\exists z\ \neg Qxyz$ is false.

So, the latter statement is not the former statement in some Skolem normal form.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ So would the correct next step not be: ∀xP(x) Λ ∃w∀y∃z¬Q(w,y,z) where [x2/w] & then proceed to pull the quantifiers to the front? $\endgroup$ – Carmine Reddit Mar 25 '18 at 20:43
  • $\begingroup$ @CarmineReddit Yes, correct. If you are doing this process as preparation for something like resolution, you can actually just take each conjunction individually, and then put each in Skolem Normal Form. But if the task is to find one statement, then yes: replace the second $x$ with a different variable and pull quantifiers in front. $\endgroup$ – Bram28 Mar 25 '18 at 20:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.