Skolem normal form

In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable. Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover. The simplest form of Skolemization is for existentially quantified variables which are not inside the scope of a universal quantifier. These may be replaced simply by creating new constants. For example, ∃ x P ( x ) {displaystyle exists xP(x)} may be changed to P ( c ) {displaystyle P(c)} , where c {displaystyle c} is a new constant (does not occur anywhere else in the formula). More generally, Skolemization is performed by replacing every existentially quantified variable y {displaystyle y} with a term f ( x 1 , … , x n ) {displaystyle f(x_{1},ldots ,x_{n})} whose function symbol f {displaystyle f} is new. The variables of this term are as follows. If the formula is in prenex normal form, x 1 , … , x n {displaystyle x_{1},ldots ,x_{n}} are the variables that are universally quantified and whose quantifiers precede that of y {displaystyle y} . In general, they are the variables that are quantified universally and such that ∃ y {displaystyle exists y} occurs in the scope of their quantifiers. The function f {displaystyle f} introduced in this process is called a Skolem function (or Skolem constant if it is of zero arity) and the term is called a Skolem term. As an example, the formula ∀ x ∃ y ∀ z . P ( x , y , z ) {displaystyle forall xexists yforall z.P(x,y,z)} is not in Skolem normal form because it contains the existential quantifier ∃ y {displaystyle exists y} . Skolemization replaces y {displaystyle y} with f ( x ) {displaystyle f(x)} , where f {displaystyle f} is a new function symbol, and removes the quantification over y {displaystyle y} . The resulting formula is ∀ x ∀ z . P ( x , f ( x ) , z ) {displaystyle forall xforall z.P(x,f(x),z)} . The Skolem term f ( x ) {displaystyle f(x)} contains x {displaystyle x} , but not z {displaystyle z} , because the quantifier to be removed ∃ y {displaystyle exists y} is in the scope of ∀ x {displaystyle forall x} , but not in that of ∀ z {displaystyle forall z} ; since this formula is in prenex normal form, this is equivalent to saying that, in the list of quantifiers, x {displaystyle x} precedes y {displaystyle y} while z {displaystyle z} does not. The formula obtained by this transformation is satisfiable if and only if the original formula is. 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.