FB18 - Das Forum für Informatik

fb18.de / Bachelorstudieng / PM Formale Informatik

Skolemisierung

Skolemisierung 2008-07-21 17:48
Corvin
Hallo,

ich habe folgende Frage zur Skolemisierung:

In welcher Reihenfolge holt man die Quantoren nach vorne? Denn \forall x \exists y ist ja was anderes als \exists y \forall x
Welche Regeln sind dort zu beachten?

wiki+foren gaben mir leider keine Antwort

Schöne grüße
Corvin

RE: Skolemisierung 2008-07-21 18:16
rothose86
Hi,

prinzipiell hast du recht. Das \forall x \exists y unterschiedlich sind.
Doch in unserem Fall beim Pränexerstellen ist es egal(meiner Meinung nach).
Denn du darfst die Quantoren ja nur nach vorne holen, wenn die Variable im Andern Teil nicht gebunden auftaucht! D.h. zB (\forall x P(x) and \exists z Q(z) ) . Hier darfst du das \forall x ja nur vorziehen, weil es auf der anderen Seite des und nicht auftaucht. Und da es auf der anderen Seite nicht auftaucht, ist die Reihenfolge für die Quantoren egal.
Wäre zB die Formel (\forall x P(x) and \exists z Q(z,x)) gegeben, dann dürftest du das \forall x auch nicht vorziehen. Dort wäre die Reihenfolge auch nicht mehr egal….

Naja kann mich auch irren….

RE: Skolemisierung 2008-07-21 20:58
Anonymer User
Danke für die schnelle Antwort!

nur eine Frage stellt sich mir noch:

Wenn es egal ist, bekomme ich doch, je nach dem was ich zuerst nach vorne gezogen habe, unterschiedliche Skolemfunktionen (-konstante), oder nicht?
oder ist das auch wieder egal?

RE: Skolemisierung 2008-07-21 21:00
rothose86
Jap denn bei Skolemfunktionen geht es ja nur um ERFÜLLBARKEITSÄQUIVALENZ, das die nicht äquivalent sind ist sowieso klar.

RE: Skolemisierung 2008-07-21 22:34
Corvin
sauber - Danke ^^