Editing Skolem normal form (section)

==Uses of Skolemization==
One of the uses of Skolemization is within [[automated theorem proving]]. For example, in the [[method of analytic tableaux]], whenever a formula whose leading quantifier is existential occurs, the formula obtained by removing that quantifier via Skolemization may be generated. For example, if <math>\exists x  \Phi(x,y_1,\ldots,y_n)</math> occurs in a tableau, where <math>x,y_1,\ldots,y_n</math> are the free variables of <math>\Phi(x,y_1,\ldots,y_n)</math>, then <math>\Phi(f(y_1,\ldots,y_n),y_1,\ldots,y_n)</math> may be added to the same branch of the tableau. This addition does not alter the satisfiability of the tableau: every model of the old formula may be extended, by adding a suitable interpretation of <math>f</math>, to a model of the new formula.

This form of Skolemization is an improvement over "classical" Skolemization in that only variables that are free in the formula are placed in the Skolem term. This is an improvement because the semantics of tableaux may implicitly place the formula in the [[Scope (programming)|scope]] of some universally quantified variables that are not in the formula itself; these variables are not in the Skolem term, while they would be there according to the original definition of Skolemization. Another improvement that may be used is applying the same Skolem function symbol for formulae that are identical [[up to]] variable renaming.<ref>Reiner Hähnle. Tableaux and related methods. [[Handbook of Automated Reasoning]].</ref>

Another use is in the [[Resolution_(logic)#Resolution_in_first_order_logic|resolution method for first-order logic]], where formulas are represented as sets of [[clause (logic)|clause]]s understood to be universally quantified. (For an example see [[drinker paradox]].)

An important result in [[model theory]] is the [[Löwenheim–Skolem theorem]], which can be proven via Skolemizing the theory and closing under the resulting Skolem functions.<ref>Scott Weinstein, [http://ozark.hendrix.edu/~yorgey/settheory/11-lowenheim-skolem.pdf The Lowenheim-Skolem Theorem], lecture notes (2009). Accessed 6 January 2023.</ref>