Scolemic shape

This article or the following section is not adequately provided with supporting documents ( e.g. individual evidence ). Information without sufficient evidence could be removed soon. Please help Wikipedia by researching the information and including good evidence.

The Skolem form belongs to the mathematical representations of predicate logic in order to formalize arguments and to check their validity. The Skolem form is a logical formula with variables that has no quantifier, or quantifier for short, for existence, ie without “it exists”. This shape was named after the Norwegian mathematician Albert Thoralf Skolem (1887–1963). ${\displaystyle F}$ ${\displaystyle \exists }$

Logical formulas can be fulfilled if at least one assignment of the variable leads to a true statement . Algorithms for checking the satisfiability often use the Skolem form, since every formula can be fulfilled exactly when its Skolem form can be fulfilled. The Skolem form is also a practical intermediate step when a logical formula is to be converted into the normal clause form or when creating a Herbrand universe . ${\displaystyle F}$ ${\displaystyle F}$

The Skolem form has no existential quantifiers , all expressions are dissolved. means “there is at least one ” - with a certain property. Variables that are linked to existential quantifiers are replaced by new function or constant symbols. The arguments of the new function symbols have universal quantifiers - in other words: "It applies to all ". ${\displaystyle \exists }$ ${\displaystyle \exists x}$ ${\displaystyle \exists x}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle \exists }$ ${\displaystyle \forall {}x}$ ${\displaystyle x}$

Algorithm for generating the Skolem shape

A formula is converted into the Skolem form by displaying it as adjusted normal form in prenex normal form , in short as adjusted prenex form. The following algorithm is applied to this formula : ${\displaystyle F_{0}}$ ${\displaystyle F}$

1. ${\displaystyle F}$ have the shape ${\displaystyle F=\forall y_{1}\forall y_{2}...\forall y_{n}\exists xG}$
2. Set ${\displaystyle F':=\forall y_{1}\forall y_{2}...\forall y_{n}G\left[x/f\left(y_{1},...,y_{n}\right)\right]}$
3. The steps are repeated until there is no more existential quantifier. ${\displaystyle F'}$ ${\displaystyle \exists }$

${\displaystyle G\left[x/w\right]}$stands for any formula in which has been replaced by. is a function symbol that does not yet appear in . The arity of is determined by the number of universal quantifiers in front of the symbol to be scolemized. Function symbols with zeros are constants . is also called Skolem function , in the case is a Skolem constant . ${\displaystyle G}$ ${\displaystyle x}$ ${\displaystyle w}$ ${\displaystyle f}$ ${\displaystyle F}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle f}$ ${\displaystyle \forall }$ ${\displaystyle f}$ ${\displaystyle n=0}$ ${\displaystyle f}$

The result is the formula in Skolem form . Other names are Skolemization of or Skolem's normal form. ${\displaystyle F}$ ${\displaystyle F'}$ ${\displaystyle F}$

It should be noted that the described transformation does not necessarily preserve the logical equivalence . The transformation maintains the satisfiability of the formula and is therefore equivalent to satisfiability , but does not preserve the model : Because the function symbol has to be reinterpreted, an interpretation that satisfies the original formula does not necessarily also satisfy the scolemized formula.

example

${\displaystyle F:=\exists x\exists y\forall w\exists z\left(P\left(x,y,w\right)\vee Q\left(z,x\right)\right)}$ is in adjusted prenex form. The above algorithm leads to the following steps:

• First is replaced by the newly introduced zero-digit function : ${\displaystyle \exists {x}}$ ${\displaystyle a}$
  ${\displaystyle F':=\exists y\forall w\exists z\left(P\left(a,y,w\right)\vee Q\left(z,a\right)\right)}$
• ${\displaystyle b}$is then introduced as a replacement for : ${\displaystyle \exists {y}}$
  ${\displaystyle F'':=\forall w\exists z\left(P\left(a,b,w\right)\vee Q\left(z,a\right)\right)}$
• Then it is replaced. The single-digit function is introduced for this. It receives the variable bound by the universal quantifier as an argument , since the universal quantifier comes before the existential quantifier. ${\displaystyle \exists {z}}$ ${\displaystyle f}$ ${\displaystyle w}$
  ${\displaystyle F''':=\forall w\left(P\left(a,b,w\right)\vee Q\left(f\left(w\right),a\right)\right)}$

The formula is now available in Skolem form with the constants , and a single-digit function symbol . ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle f(w)}$