How Skolemization Works
Skolemization works by applying a second-order equivalence in conjunction to the definition of first-order satisfiability. The equivalence provides a way for "moving" an existential quantifier before a universal one.
where
- is a function that maps x to y.
Intuitively, the sentence "for every x there exists a y such that R(x,y)" is converted into the equivalent form "there exists a function f mapping every x into a y such that, for every x it holds R(x,f(x))".
This equivalence is useful because the definition of first-order satisfiability implicitly existentially quantifies over the evaluation of function symbols. In particular, a first-order formula is satisfiable if there exists a model and an evaluation of the free variables of the formula that evaluate the formula to true. The model contains the evaluation of all function symbols; therefore, Skolem functions are implicitly existentially quantified. In the example above, is satisfiable if and only if there exists a model, which contains an evaluation for, such that is true for some evaluation of its free variables (none in this case). This can be expressed in second order as . By the above equivalence, this is the same as the satisfiability of .
At the meta-level, first-order satisfiability of a formula can be written with a little abuse of notation as, where is a model and is an evaluation of the free variables. Since first-order models contain the evaluation of all function symbols, any Skolem function contains is implicitly existentially quantified by . As a result, after replacing an existential quantifier over variables into an existential quantifiers over functions at the front of the formula, the formula can still be treated as a first-order one by removing these existential quantifiers. This final step of treating as can be done because functions are implicitly existentially quantified by in the definition of first-order satisfiability.
Correctness of Skolemization can be shown on the example formula as follows. This formula is satisfied by a model if and only if, for each possible value for in the domain of the model there exists a value for in the domain of the model that makes true. By the axiom of choice, there exists a function such that . As a result, the formula is satisfiable, because it has the model obtained by adding the evaluation of to . This shows that is satisfiable only if is satisfiable as well. In the other way around, if is satisfiable, then there exists a model that satisfies it; this model includes an evaluation for the function such that, for every value of, the formula holds. As a result, is satisfied by the same model because one can choose, for every value of, the value, where is evaluated according to .
Read more about this topic: Skolem Normal Form
Famous quotes containing the word works:
“I shall not bring an automobile with me. These inventions infest France almost as much as Bloomer cycling costumes, but they make a horrid racket, and are particularly objectionable. So are the Bloomers. Nothing more abominable has ever been invented. Perhaps the automobile tricycles may succeed better, but I abjure all these works of the devil.”
—Henry Brooks Adams (1838–1918)