Skolemform

Eine Formel ${\displaystyle F_{0}}$ wird in die Skolemform gebracht, indem sie als bereinigte Normalform in der Pränex-Normalform dargestellt wird, kurz als bereinigte Pränexform. Auf diese Formel ${\displaystyle F}$ wird der folgende Algorithmus anwendet:

1. ${\displaystyle F}$ habe die Form ${\displaystyle F=\forall y_{1}\forall y_{2}...\forall y_{n}\exists xG}$
2. Setze ${\displaystyle F':=\forall y_{1}\forall y_{2}...\forall y_{n}G\left[x/f\left(y_{1},...,y_{n}\right)\right]}$
3. Die Schritte werden wiederholt, bis ${\displaystyle F'}$ keinen Existenzquantor ${\displaystyle \exists }$ mehr enthält.

${\displaystyle G\left[x/w\right]}$ steht für eine beliebige Formel ${\displaystyle G}$, in der ${\displaystyle x}$ durch ${\displaystyle w}$ ersetzt wurde. ${\displaystyle f}$ ist ein in ${\displaystyle F}$ noch nicht vorkommendes ${\displaystyle n}$-stelliges Funktionssymbol. Die Stelligkeit ${\displaystyle n}$ von ${\displaystyle f}$ ist bestimmt durch die Anzahl der Allquantoren ${\displaystyle \forall }$ vor dem zu skolemisierenden Symbol. Nullstellige Funktionssymbole sind Konstanten. ${\displaystyle f}$ heißt auch Skolemfunktion, im Fall ${\displaystyle n=0}$ ist ${\displaystyle f}$ eine Skolemkonstante.

Als Ergebnis erhält man die Formel ${\displaystyle F}$ in Skolemform ${\displaystyle F'}$. Andere Bezeichnungen sind Skolemisierung von ${\displaystyle F}$ oder auch Skolem’sche Normalform.

Zu beachten ist, dass bei der beschriebenen Umformung nicht notwendigerweise die logische Äquivalenz erhalten bleibt. Die Umformung erhält zwar die Erfüllbarkeit der Formel und ist somit erfüllbarkeitsäquivalent, ist aber nicht modellerhaltend: Weil das Funktionssymbol neu interpretiert werden muss, erfüllt eine Interpretation, welche die ursprüngliche Formel erfüllt, nicht notwendigerweise auch die skolemisierte Formel.

${\displaystyle F:=\exists x\exists y\forall w\exists z\left(P\left(x,y,w\right)\vee Q\left(z,x\right)\right)}$ ist in bereinigter Pränexform. Der oben aufgeführte Algorithmus führt zu folgenden Schritten:

• Zuerst wird ${\displaystyle \exists {x}}$ durch die neu eingeführte nullstellige Funktion ${\displaystyle a}$ ersetzt:
  ${\displaystyle F':=\exists y\forall w\exists z\left(P\left(a,y,w\right)\vee Q\left(z,a\right)\right)}$
• ${\displaystyle b}$ wird danach als Ersetzung für ${\displaystyle \exists {y}}$ eingeführt:
  ${\displaystyle F'':=\forall w\exists z\left(P\left(a,b,w\right)\vee Q\left(z,a\right)\right)}$
• Dann wird ${\displaystyle \exists {z}}$ ersetzt. Dafür wird die einstellige Funktion ${\displaystyle f}$ eingeführt. Sie erhält als Argument die per Allquantor gebundene Variable ${\displaystyle w}$, da der Allquantor vor dem Existenzquantor steht.
  ${\displaystyle F''':=\forall w\left(P\left(a,b,w\right)\vee Q\left(f\left(w\right),a\right)\right)}$

Nun liegt die Formel in Skolemform mit den Konstanten ${\displaystyle a}$, ${\displaystyle b}$ und dem einstelligen Funktionssymbol ${\displaystyle f(w)}$ vor.