Why can't all existential binders be replaced by unique constants during skolemization?

When using skolemization to replace existentially quantified variables in an expression, any existential bound at the top level can be replaced by a new globally unique constant, however if the existential is under a universal quantification it cannot be replaced by a constant. It must be replaced instead by a new globally unique predicate symbol which is applied to all the universally quantified variables in scope.

I don't understand why this must be so, since the uniqueness of the new predicate symbol must surely prevent it from unifying with any other object but itself.

Each step in Skolemization preserves the satisfiability of the formula. If all existentially-bound variables are replaced by constants instead of functions, the modified formula may be unsatisfiable even if the original formula was satisfiable.

Consider the formula , where P is a first-order formula with free variables x and y. If you simply replace y with a new constant c, the resulting formula is logically stronger, as y is allowed to depend on x, but c is not.

In other words, Skolemization relies on the (second-order) logical equivalence , and that is satisfiable iff is. Your suggestion breaks down because is not equivalent to .

For a specific counter-example, suppose that P encodes the following:

• the axioms of group theory with operation * and identity 1,
• the group has order at least 2: , and
• y is the inverse of x: x*y = 1.

Then is satisfiable, since it says "every element of the group has an inverse." But is not satisfiable, since it says "the element c is the inverse to every group element."