Skolemization

Mathematical Logic · Axiom Academy

A technique for eliminating existential quantifiers in first-order logic formulas The primary objective of Skolemization is to eliminate existential quantifiers from a first-order logic formula while preserving satisfiability. This transformation is crucial because: Many automated theorem provers work more efficiently without existential quantifiers It simplifies the formula structure for resolution-based provers It makes explicit the dependencies between variables The simplest case of Skolemization occurs when we have a formula of the form: where x is not in the scope of any universal quantifier. In this case, we replace the existentially quantified variable with a Skolem constant . When an existential quantifier appears in the scope of universal quantifiers, we need a more sophisticated approach. For a formula like: The existentially quantified variable y may depend on the universally quantified variable x . We replace y with a Skolem function that takes x as input. 4. Preserves Satisfiability (Not Equivalence) A crucial property of Skolemization is that it preserves satisfiability but not logical equivalence. If the original formula is satisfiable, the Skolemized formula is also satisfiable If the Skolemized formula is satisfiable, the original is also satisfiable However, the formulas may not be logically equivalent The systematic procedure for Skolemizing a formula: Convert to Prenex Normal Form: Move all quantifiers to the front

This is the written version of the interactive lesson above. See the full Mathematical Logic course.