How to skolemize multiple combinations of universal and existential quantifieres?

Question

What is the skolemized form of (∀u∃v a(u,v)) ∧ (∀x∃y a(x,y)) ?

I am unsure, because there are different perenex normal forms possible:

• ∀u∃v ∀x∃y (a(u,v) ∧ a(x,y))
• ∀u∀x ∃v∃y (a(u,v) ∧ a(x,y))
• …

There would different skolemized forms follow:

• ∀u ∀x (a(u,f(u)) ∧ a(x,g(u,x)))
• ∀u∀x (a(u,f(u,x)) ∧ a(x,g(u,x)))

In my mind, they are not equivalent to each other. Or am I here wrong?

Answer 1

Yes, prenex normal forms are not unique for a given FO formula, and, correspondingly, Skolemizations are not unique. A simpler example for the same "scope escape" I think you are trying to show is the formula ∃xAx → ∃yBy, with prenex forms ∀x∃y (Ax → By) and ∃y∀x (Ax → By), and respective skolemizations ∀x (¬ Ax ∨ Bf(x)) and ∀x (¬ Ax ∨ B a), with a a constant.

Now, the pertinent question is whether the non-equivalence of those formulae matters for your particular problem. If it does, perhaps Skolemization is not the best tool for you: Skolemization is a process designed to preserve satisfiability of formulae, sometimes at the expense of equivalence.

(and in any case, it is a good exercise to see why distinct skolemizations of a single formula are equisatisfiable, if only on the examples above)