How does skolemisation of lone EXISTS clauses work?

Question

Hi,

If I have a formula like:

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = For All / E = Exists)

The rules of skolemisation say that:

1. if E is outside FA replace with a constant or
2. if E is inside FA replace by a new function contain all the vars from outside the FA as arguments.

So what do I do in this case? Can I just drop the Exists quantifier or do I replace it with a constant?

Thanks!

Answer 1

First write this using standard notation:

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

Now, applying your second skolemisation rule:

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

So I've replaced ∃z with a function containing all vars from outside.

Now, this still isn't in Skolem normal form, because it isn't in conjuctive prenex normal form: the formulas still uses lots of disjunctions (∨). Removing those is left up to you.