Skolemisierung einer Pränexform

Question

 

Vielleicht sind hier ja ein paar Logik-Experten online.

Ich stehe gerade vor einer Frage: 

Ich habe folgende pränexe Form:

∀x ∃z((¬P(x,y) ∨ Q(z,z))

Jetzt muss ich ja zur Skolemisierung die Existenzquantoren entfernen.

In dem Beispiel wird aber vorher noch die freie Variable y existenzquantifiziert, dazu finde ich aber leider nicht viele Informationen. 

Muss das vorher gemacht werden, oder kann in einer Skolemform auch eine freie Variable vorkommen?

Answer 1

> In dem Beispiel wird aber vorher noch die freie Variable y existenzquantifiziert.

Zur Überführung in Klausel-Normalform werden auch noch die Allquantoren entfernt und alle Variablen gelten als implizit allquantifiziert.

Freie Variablen in prädikatenlogischen Formeln werden bezüglich Erfüllbarkeit aber so behandelt, als wären sie existenzquantifiziert.

Wird Klausel-Normalform angestrebt, dann müssen freie Variablen also existenzquantifiziert werden. Das kann aber auch nach der Skolemisierung erfolgen.

> kann in einer Skolemform auch eine freie Variable vorkommen

Ja.

Comments

Danke, es hatte mich auch gewundert.