A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Skolemization is the process of replacing existential quantifiers with function symbols (Skolem functions) that witness the existence claims. When a formula ∃x φ(x) is true, we can replace it with φ(f(y₁,...,yₙ)) where f is a new function and y₁,...,yₙ are universally quantified variables. This transformation preserves satisfiability and is crucial for converting formulas into a form suitable for automated reasoning.
You've studied prenex normal form — the process of pulling all quantifiers to the front so a formula looks like Q₁x₁ Q₂x₂ ... Qₙxₙ φ where φ is quantifier-free. Skolemization takes the next step: it eliminates existential quantifiers entirely, replacing them with Skolem functions that serve as explicit witnesses, producing an equisatisfiable universal formula.
The core idea: whenever you have ∃y P(y), there must be some specific element witnessing the existence. Instead of leaving it as an unnamed entity, introduce a new function symbol f and write P(f(x₁,...,xₖ)) where x₁,...,xₖ are all the universally quantified variables in scope. For example, ∀x ∃y (y > x) becomes ∀x (f(x) > x), where f is a new "choice function" mapping each x to some y greater than it. With nested quantifiers, ∀x ∃y ∀z ∃w R(x,y,z,w) becomes ∀x ∀z R(x, f(x), z, g(x,z)) — the Skolem function for w depends on both x and z because those are the universal variables in scope when w is introduced.
The critical property: a formula φ is satisfiable if and only if its Skolemization Sk(φ) is satisfiable. Given a model for φ, you can define the Skolem functions by picking witnesses (using the axiom of choice if needed); given a model for Sk(φ), the existential witnesses are just the values of the Skolem functions. Notice this is not logical equivalence — Sk(φ) may be stronger than φ in some models — but satisfiability is preserved, and that is what matters for automated theorem proving.
After Skolemization, the resulting formula is universal — all remaining quantifiers are ∀. Universal formulas can be grounded by replacing each variable with a term from the Herbrand universe (the set of all ground terms built from constants and function symbols). The Herbrand theorem says: a universal formula is unsatisfiable if and only if some finite set of ground instances is propositionally unsatisfiable. This reduces first-order reasoning to propositional reasoning over ground instances. Resolution-based automated theorem provers work entirely on clausal forms of Skolemized formulas — they take the negation of the goal, Skolemize, convert to clausal form, and try to derive the empty clause by resolution. Skolemization is thus the bridge from expressive first-order logic to the mechanically tractable, implementable algorithms of modern automated reasoning.