Skolemizáció

Skolemizáció is a process in mathematical logic used to eliminate existential quantifiers from formulas. It is named after Norwegian mathematician Thoralf Skolem. The goal of Skolemization is to transform a formula containing existential quantifiers into an equivalent formula in prenex normal form, where all quantifiers appear at the beginning of the formula, and all existential quantifiers are replaced by Skolem functions or Skolem constants.

The basic idea is that if there exists an object satisfying a certain property, we can introduce a new function (or constant) that represents that object. For instance, if we have a formula like $\exists y P(x, y)$, which reads "there exists a y such that P(x, y) holds", Skolemization replaces this with $P(x, f(x))$, where $f$ is a new function symbol called a Skolem function. This function $f$ is understood to map $x$ to the specific $y$ that satisfies $P(x, y)$. If the existential quantifier is not dependent on any other variables, like $\exists y P(y)$, it is replaced by a Skolem constant, say $c$, resulting in $P(c)$.

Skolemization is a crucial step in many automated theorem-proving procedures and in the process of converting first-order logic formulas into a form suitable for resolution. It preserves satisfiability, meaning that a formula is satisfiable if and only if its Skolemized form is satisfiable. However, it does not preserve logical equivalence in general, as the Skolemized formula may have different models than the original formula. The introduced Skolem functions or constants are interpreted in a way that makes the transformed formula true whenever the original was true, but they might introduce additional interpretations not present in the original.