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.