Seite 1 von 2

Herbrandmodell und Skolemisierung

Verfasst: 23. Aug 2011 17:38
von bafnai
Hallo,
ich habe Fragen bezüglich des Herbrandmodells und der Skolemisierung.

Zuerst zum Herbrandmodell:
Es geht um die Interpretation der Funktions- und Relationssymbole.
Wie ein Funktionssymbol interpretiert wird, wenn es keine weiteren Funktionssymbole gibt ist einleuchtend, aber wie geht man bei mehreren Funktionssymbolen vor und wie erkennt man generell die Interpretationen der Relationen?

Als Beispiel (Übungsblatt 5, H1, https://www3.mathematik.tu-darmstadt.de ... bung12.pdf):
\(S = (c, f , g, P, L, R)\)
\(H = (T_0(S), c^H, f^H, g^H, P^H, L^H, R^H)\)
\(T_0(S) =\){\(c, f(c), g(c), f(g(c)), g(f(c)), …\)}


Und zur Skolemisierung:
Hier geht es um das Setzen der Skolemkonstanten.
Trivial ist dieser Fall: \(\exists\) \(E\)x wird zu \(E\)c
Aber was ist in folgenden Fällen:

1. \(\forall\)x \(\exists\)y (\(E\)xy \(\wedge\) \(R\)y)
Wird es zu \(\forall\)x (\(E\)xf(x) \(\wedge\) \(R\)f(x)) oder zu \(\forall\)x (\(E\)xf(x) \(\wedge\) \(R\)c)?

2. \(\forall\)x \(\exists\)y (\(E\)x \(\wedge\) \(R\)y)
Wird es zu \(\forall\)x (\(E\)x \(\wedge\) \(R\)f(x)) oder zu \(\forall\)x (\(E\)x \(\wedge\) \(R\)c)?

MfG bafnai

Re: Herbrandmodell und Skolemisierung

Verfasst: 23. Aug 2011 18:29
von fscheepy
Dazu hätte ich auch noch eine Frage:
Bei der Übung 13 G1(a) wird ja nach der SKNF gefragt. Wieso wird da das a durch die (0-stellige?) Funktion f ersetzt? Ich dachte man ersetzt den Existenzquantor und die zugehörige Variable einfach mit einer Konstanten, wenn diese Variable nicht von einer anderen abhängt?

Re: Herbrandmodell und Skolemisierung

Verfasst: 23. Aug 2011 19:38
von dschneid
bafnai hat geschrieben:Zuerst zum Herbrandmodell:
[...] wie geht man bei mehreren Funktionssymbolen vor und wie erkennt man generell die Interpretationen der Relationen?
In einem Herbrandmodell werden die Funktionssymbole immer als sie selbst interpretiert. Da macht es keinen Unterschied, wenn die Signatur mehrere Funktionssymole enthält. Möglicherweise verstehe ich dich falsch.

Es gibt keine allgemeine Methode, geeignete Interpretation der Relationen zu finden, denn die konkrete Wahl muss ja von den Formeln, welche das Modell erfüllen soll, abhängen. Ein sehr praktischer Trick ist es aber, zu versuchen, die Formeln trivialerweise wahr zu machen. Wenn die Formeln zum Beispiel Implikationen sind, dann sollte man versuchen, die Prämisse immer falsch sein zu lassen. In den allermeisten Übungs- und Klausuraufgaben kann man ein passendes Herbrand-Modell konstruieren, indem man die Relationen immer falsch oder immer richtig wahr sein lässt, also dafür die leere Menge oder die gesamte Trägermenge (bzw. für mehrstellige Relationen entsprechende kartesische Produkte der Trägermenge mit sich selbst) wählt. Wenn man das im Hinterkopf hat, kann man die Lösung sehr schnell finden.
bafnai hat geschrieben:Und zur Skolemisierung:
[...] was ist in folgenden Fällen:

1. \(\forall\)x \(\exists\)y (\(E\)xy \(\wedge\) \(R\)y)
Wird es zu \(\forall\)x (\(E\)xf(x) \(\wedge\) \(R\)f(x)) oder zu \(\forall\)x (\(E\)xf(x) \(\wedge\) \(R\)c)?

2. \(\forall\)x \(\exists\)y (\(E\)x \(\wedge\) \(R\)y)
Wird es zu \(\forall\)x (\(E\)x \(\wedge\) \(R\)f(x)) oder zu \(\forall\)x (\(E\)x \(\wedge\) \(R\)c)?
Es ist in beiden Fällen die erste Formel, weil die existenzquantifizierte Variable \(y\) durch eine einstellige Skolem-Funktion \(f\) ersetzt wird, denn es gibt die allquantifizierte Variable \(x\) weiter außen. Insbesondere sind in der ersten Skolemisierung die beiden \(y\) Vorkommnisse derselben Variable, müssen also auch gleich ersetzt werden.
fscheepy hat geschrieben:Wieso wird da das a durch die (0-stellige?) Funktion f ersetzt? Ich dachte man ersetzt den Existenzquantor und die zugehörige Variable einfach mit einer Konstanten, wenn diese Variable nicht von einer anderen abhängt?
Weil eine 0-stellige Funktion nur eine schmissige Art ist, eine Konstante darzustellen. Eine 0-stellige Funktion muss ja immer denselben Wert haben, denn es gibt kein Argument, das ihn in verschiedenen Fällen unterschiedlich machen könnte; also sind alle 0-stelligen Funktionen konstant. Du kannst dir \(f\) hier also auch als Konstante denken.

Re: Herbrandmodell und Skolemisierung

Verfasst: 23. Aug 2011 20:04
von bafnai
Hallo,
zuerst bezüglich
dschneid hat geschrieben: In einem Herbrandmodell werden die Funktionssymbole immer als sie selbst interpretiert. Da macht es keinen Unterschied, wenn die Signatur mehrere Funktionssymbole enthält. Möglicherweise verstehe ich dich falsch.
Wenn man Übungsblatt 5, G1, b)
  • \(S = (c, f_y , P)\)
    \(H = (T_0(S), c^H, f_y^H, P^H)\)
    \(T_0(S) =\){\(c, f(c), f(f(c)), …\)}
betrachtet, ist es klar, dass \(f_y^H(f^n c) =ff^n c\) gilt.
Wenn die Trägermenge aber so aussieht
  • \(T_0(S) =\){\(c, f(c), g(c), f(g(c)), g(f(c)), …\)}
weiß ich ehrlich gesagt nicht, wie ich die Interpretationen formulieren soll.

dschneid hat geschrieben: Es ist in beiden Fällen die erste Formel, weil die existenzquantifizierte Variable \(y\) durch eine einstellige Skolem-Funktion \(f\) ersetzt wird, denn es gibt die allquantifizierte Variable \(x\) weiter außen.
Sähe es so aus
  • \(\exists\)y \(\forall\)x (\(E\)x \(\wedge\) \(R\)y)
könnte man dann \(R\)y durch \(R\)c ersetzen?

MfG bafnai

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 23. Aug 2011 20:22
    von dschneid
    bafnai hat geschrieben:Wenn man Übungsblatt 5, G1, b)
    • \(S = (c, f_y , P)\)
      \(H = (T_0(S), c^H, f_y^H, P^H)\)
      \(T_0(S) =\){\(c, f(c), f(f(c)), …\)}
    betrachtet, ist es klar, dass \(f_y^H(f^n c) =ff^n c\) gilt.
    Wenn die Trägermenge aber so aussieht
    • \(T_0(S) =\){\(c, f(c), g(c), f(g(c)), g(f(c)), …\)}
    weiß ich ehrlich gesagt nicht, wie ich die Interpretationen formulieren soll.
    Ich denke, du machst es dir etwas zu kompliziert. In einer Herbrand-Struktur ist die Interpretation jedes Funktionensymbols \(f\) aus der Signatur, wenn ich mich recht erinnere, vollständig definiert durch \(f^\mathcal{H}(t_1, \dots, t_n) := f(t_1^\mathcal{H}, \dots, t_n^\mathcal{H})\) mit beliebigen Termen \(t_1, \dots, t_n \in T_0(S)\) (oder ohne Klammern um die Argumente, je nach Gusto). Diese Definitionen sind unabhängig von allen anderen Funktionensymolen, und deswegen funktioniert das bei mehreren solchen genau so gut wie bei nur einem. Im Übrigen würde ich in der Klausur diese Definitionen nicht extra hinschreiben, weil die Interpretation der Funktionen ja durch die Definition eines Herbrand-Modells schon vorgegeben ist. (Ich habe in den Übungen immer geschrieben, die Funktionen werden interpretiert "wie üblich".) Das sollte in der Klausur kein Problem sein; das einzig Interessante sind die Interpretationen der Relationen.
    bafnai hat geschrieben:Sähe es so aus
    • \(\exists\)y \(\forall\)x (\(E\)x \(\wedge\) \(R\)y)
    könnte man dann \(R\)y durch \(R\)c ersetzen?
    So ist es.

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 23. Aug 2011 20:24
    von fscheepy
    dschneid hat geschrieben: Weil eine 0-stellige Funktion nur eine schmissige Art ist, eine Konstante darzustellen. Eine 0-stellige Funktion muss ja immer denselben Wert haben, denn es gibt kein Argument, das ihn in verschiedenen Fällen unterschiedlich machen könnte; also sind alle 0-stelligen Funktionen konstant. Du kannst dir \(f\) hier also auch als Konstante denken.
    Achso, danke für die Antwort. Wäre es denn falsch, statt einer 0-stelligen Funktion eine Konstante einzusetzen bzw. hinzuschreiben?

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 23. Aug 2011 20:28
    von dschneid
    Nein, wie gesagt, mathematisch gesehen ist das genau dasselbe.

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 24. Aug 2011 16:22
    von fscheepy
    Danke nochmal.


    Was bedeutet bei der Übung 12, G1 in der Musterlösung der Hinweis "Wenn man einen Quantor aus der Prämisse einer Implikation herauszieht, muss man ihn dualisieren!"?
    Kann mir vielleicht jemand ein Beispiel dazu geben? Ich verstehe nicht so ganz, was hier mit dem dualisieren gemeint ist.

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 24. Aug 2011 16:58
    von bafnai
    Hallo,
    hierzu noch einmal
    dschneid hat geschrieben:In den allermeisten Übungs- und Klausuraufgaben kann man ein passendes Herbrand-Modell konstruieren, indem man die Relationen immer falsch oder immer wahr sein lässt, also dafür die leere Menge oder die gesamte Trägermenge (bzw. für mehrstellige Relationen entsprechende kartesische Produkte der Trägermenge mit sich selbst) wählt.
    Als Beispiel H1 (b) von Übungsblatt 5:
    (1)\(\forall xRxf(x)\)
    (2)\(\forall xLxg(x)\)
    (3)\(Pc\)
    (4)\(\forall x \forall y (Lxy\rightarrow Rxy)\)
    (5)\(\forall x \forall y ((Px\wedge Rxy)\rightarrow Py\)

    Lösung:
    Sei \(T_0 := \{c\} \\)und \(T_{n+1} := \{f(t); g(t): t\in T_n\}\). Dann ist \(T := \bigcup\ _{n \in \mathbb N} \ T_n\)die Trägermenge der Sätze aus (a). Das Herbrandmodell \(H := (T ,R^H,L^H, P^H)\) mit \(R^H = L^H = T\times T\)und \(P^H = T\)erfüllt dann die Sätze.

    Ganz abgesehen von der interessanten Bildung der Trägermenger:
    Es heißt \(T\times T\), da es zweistellige Relationssymbole sind, aber warum überhaupt \(T\)?
    \(R\) zum Beispiel steht nur im Zusammenhang mit \(f\). In \(T\) ist aber auch noch \(g\) enthalten.


    Ich verstehe auch immer noch nicht, woran man bei FO-Formeln erkennt, ob diese erfüllbar bzw. unerfüllbar sind.


    MfG bafnai

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 24. Aug 2011 23:06
    von dschneid
    bafnai hat geschrieben:Es heißt \(T\times T\), da es zweistellige Relationssymbole sind, aber warum überhaupt \(T\)?
    Wenn man \(T \times T\) wählt, dann heißt das nur, dass \(Rxy\) und \(Lxy\) einfach immer wahr sind, also für alle möglichen Paare von Termen, die man für \(x\) und \(y\) einsetzen kann. Es funktioniert natürlich auch mit einer weniger allgemeinen Wahl (sich so eine zu überlegen, ist eine sehr gute Übung), aber das ist mit Abstand die einfachste, und es ist ja nur nach einem Herbrand-Modell gefragt; es kann durchaus mehrere geben. Nur ist der Trick hier eben, in der Klausur nicht lange nach komplizierten, möglichst eleganten Modellen zu suchen, sondern schnell die brachiale Wahl zu sehen.
    bafnai hat geschrieben:Ganz abgesehen von der interessanten Bildung der Trägermenger:
    Diese Definition generiert induktiv alle Terme, die man aus den Konstanten- und Funktionensymbolen bauen kann. Man fängt mit der einzigen Konstante an, und dann werden Mengen von immer längeren Termen gebildet (jeder Term in einem \(T_n\) hat gerade \(n\) Funktionsanwendungen auf \(c\)). Alle diese Mengen zusammen (also einfach alle Terme beliebiger Länge) ergeben die gesamte Trägermenge. Die Idee ist: \(c\) ist ein Term, und wenn man schon einen Term hat und eine der Funktionen darauf anwendet, dann ist das wiederum auch ein Term.
    bafnai hat geschrieben:Ich verstehe auch immer noch nicht, woran man bei FO-Formeln erkennt, ob diese erfüllbar bzw. unerfüllbar sind.
    Jedenfalls nicht mechanisch, wie mit der Wahrheitstafel; es ist also tatsächlich etwas schwieriger. Man muss etwas herumprobieren. Nützlich ist es auf jeden Fall, im Hinterkopf zu haben, dass Modelle einer FO-Formel nicht nur aus "wahr" und "falsch" für die einzelnen Variablen bestehen, sondern aus einer kompletten Trägermenge und Interpretationen für alle Konstanten, Funktionen und Relationen. Man hat da also einen sehr großen Spielraum. Ich finde es immer nützlich, sich die Bedeutung von Formeln in bekannten Standardinterpretationen wie den natürlichen oder ganzen Zahlen oder Graphen vorzustellen.

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 25. Aug 2011 17:28
    von bafnai
    Hallo,
    zuerst möchte ich für die bisherigen Erklärungen danken.


    Wollen wir doch einmal sehen, ob ich es halbwegs verstanden habe.

    Als Beispiel Aufgabe 2 (a) aus der Klausur vom WS 06/07.
    \(\forall x \forall y [Rxx \wedge \neg Rxfx \wedge (Rxfy \rightarrow Rxy)]\)

    Ich gehe davon aus, dass R standardmäßig wahr ist und f die Teilformel negiert.
    - \(Rxx\) wahr
    - \(\neg Rxfx\) zuerst wahr, durch f falsch, durch \(\neg\) wieder wahr
    - \(Rxfy\) zuerst wahr, durch f falsch
    - \(Rxy\) wahr
    - \(R^H = T_0 (S)\) ?


    Und noch zwei weitere Fragen zur Skolemisierung:
    Wenn in einer Formel für verschiedene Variablen (z. B.) einstellige Funktionssymbole benötigt werden, kann man dann dasselbe Funktionssymbol verwenden, oder muss man noch ein zweites einführen.
    Und dieselbe Frage noch einmal, nur mit Konstantensymbolen anstatt Funktionssymbolen.

    MfG bafnai

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 25. Aug 2011 19:17
    von dschneid
    bafnai hat geschrieben:Als Beispiel Aufgabe 2 (a) aus der Klausur vom WS 06/07.
    \(\forall x \forall y [Rxx \wedge \neg Rxfx \wedge (Rxfy \rightarrow Rxy)]\)

    Ich gehe davon aus, dass R standardmäßig wahr ist und f die Teilformel negiert.
    - \(Rxx\) wahr
    - \(\neg Rxfx\) zuerst wahr, durch f falsch, durch \(\neg\) wieder wahr
    - \(Rxfy\) zuerst wahr, durch f falsch
    - \(Rxy\) wahr
    - \(R^H = T_0 (S)\) ?
    Also ich geh mal davon aus, dass du ein Herbrand-Modell für die Formel suchst. Zuerst einmal gibt es da noch ein Missverständnis: wahr oder falsch können nur Formelatome sein (also Gleichheiten oder Relationen, z.B. von der Form \(Rxy\)). Ein Term dagegen ist sozusagen nur eine Adresse auf ein Element der Trägermenge. Deswegen macht es keinen Sinn, davon zu sprechen, dass eine Anwendung von \(f\) irgendeinen Wahrheitswert verändern würde. Außerdem funktioniert deine Wahl für \(R^\mathcal{H}\) nicht so wirklich, weil \(R\) ja eine binäre Relation ist.

    Mein Gedankengang wäre der folgende: Wir müssen alle drei Teile der Konjunktion in der Formel wahr machen. Als erstes testen wir die Brachialtaktik, einfach \(R^\mathcal{H}\) auf alle Paare von Termen zu setzen. Das geht offenbar nicht, weil im zweiten Teil eine Negation ist, der würde dann also immer falsch sein. Genauso funktioniert es auch nicht, einfach \(R^\mathcal{H}\) auf die leere Menge (also immer falsch) zu setzen, weil dann der erste Teil immer falsch wäre. Hier muss man also tatsächlich etwas feinfühliger arbeiten.
    Wir machen die Beobachtung, dass der zweite Teil und die Prämisse des dritten Teils quasi dieselbe Struktur haben. Deswegen können wir die Implikation im dritten Teil nur dadurch erfüllen, dass wir die Prämisse auf "falsch" setzen. Der andere Weg, sowohl die Prämisse als auch die Konklusion erfüllen zu wollen, kann nicht funktionieren, weil die Prämisse zu erfüllen automatisch den zweiten Teil der Konjunktion nicht mehr erfüllen würde (denn die beiden sind ja gleich). Also darf kein Paar der Form \((t, ft)\) für irgendeinen Term \(t\) in \(R^\mathcal{H}\) sein. Damit erfüllen wir den dritten Teil, und außerdem gleichzeitig noch den zweiten Teil. Jetzt müssen wir nur noch alle Paare der Form \((t, t)\) mit einem beliebigen Term \(t\) in unsere Interpretation von \(R\) aufnehmen, um auch noch den ersten Teil zu erfüllen.

    Also ist \(R^\mathcal{H} = \{(t, t) \, | \, t \in T_0(S)\}\) beispielsweise eine günstige Wahl.
    bafnai hat geschrieben:Wenn in einer Formel für verschiedene Variablen (z. B.) einstellige Funktionssymbole benötigt werden, kann man dann dasselbe Funktionssymbol verwenden, oder muss man noch ein zweites einführen.
    Und dieselbe Frage noch einmal, nur mit Konstantensymbolen anstatt Funktionssymbolen.
    Nein, man braucht verschiedene. Die quantifizierten Variablen, die man durch Ersetzung eliminiert, sind ja in der Wahl der Elemente, die man dafür einsetzen kann, unabhängig voneinander. Z.B. kann man in der Formel \(\exists x \, \exists y \, x + 1 = y\) die Werte von \(x\) und \(y\) verschieden wählen. Wenn man für zwei Variablen dieselbe Funktion oder Konstante benutzt, dann impliziert man damit aber, dass die Variablen immer den gleichen Wert haben müssen, was ja falsch ist.

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 26. Aug 2011 19:36
    von bafnai
    Hallo,
    gut, ich versuche deine Ausführungen anzuwenden.

    Klausur WS 07/08, Aufgabe 5 (b)

    Sei \(R\) ein zweistelliges Relationssymbol und \(f\) ein einstelliges Funktionssymbol. Geben Sie zu dem Satz
    \(\varphi := \forall x Rfxx \wedge \forall x \forall y (Rfxfy \rightarrow Rxy) \wedge \forall x \forall y (Rxy \rightarrow \neg Ryx)\)
    ein Herbrand-Modell an.

    \(S(c, f, R)\)
    \(H=(T_0(S), c^H, f^H, R^H)\)
    \(T_0(S) = \{c, fc, ffc, …\}\)
    Interpretation der Konstanten- und Funktionssymbole wie üblich über die Trägermenge, d.h. \(c^H=c\) und \(f(f^nc) = \{ff^nc \mid n \in \mathbb{N} \}\).

    Gedanken: Die Konklusion im dritten Teil muss falsch sein (ohne das \(\neg\)), dann muss im zweiten Teil die Prämisse ebenso falsch sein. D.h. Terme der Form \((c, c)\) und \((fc, fc)\) dürfen nicht in \(R^H\) enthalten sein.

    \(R^H = \{(f^nc, f^mc) : n \not= m \}\) für \(f, c \in T_0(S)\) und \(n, m \in \mathbb{N}\)



    Klausur SS06, Aufgabe 2 (c)


    \(g\) einstelliges Funktionssymbol, \(E\) zweistelliges Relationssymbol.
    \(\forall x \forall y [\neg Exx \wedge Exgx \wedge (Exy \rightarrow (Exfxy \wedge Efxyy))]\)

    \(S(c, g, E)\)
    \(H=(T_0(S), c^H, g^H, E^H)\)
    \(T_0(S) = \{c, gc, ggc, …\}\)
    Interpretation der Konstanten- und Funktionssymbole wie üblich über die Trägermenge, d.h. \(c^H=c\) und \(g(g^nc) = \{gg^nc \mid n \in \mathbb{N} \}\).

    Gedanke: Der erste Teil muss falsch sein (wieder ohne das \(\neg\)).

    \(E^H = \{f^nc, f^mc : n > 0, m > 0 \}\) für \(f, c \in T_0(S)\) und \(n, m \in \mathbb{N}\)


    MfG bafnai

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 27. Aug 2011 14:26
    von fscheepy
    bafnai hat geschrieben: Klausur WS 07/08, Aufgabe 5 (b)

    Sei \(R\) ein zweistelliges Relationssymbol und \(f\) ein einstelliges Funktionssymbol. Geben Sie zu dem Satz
    \(\varphi := \forall x Rfxx \wedge \forall x \forall y (Rfxfy \rightarrow Rxy) \wedge \forall x \forall y (Rxy \rightarrow \neg Ryx)\)
    ein Herbrand-Modell an.

    \(S(c, f, R)\)
    \(H=(T_0(S), c^H, f^H, R^H)\)
    \(T_0(S) = \{c, fc, ffc, …\}\)
    Interpretation der Konstanten- und Funktionssymbole wie üblich über die Trägermenge, d.h. \(c^H=c\) und \(f(f^nc) = \{ff^nc \mid n \in \mathbb{N} \}\).

    Gedanken: Die Konklusion im dritten Teil muss falsch sein (ohne das \(\neg\)), dann muss im zweiten Teil die Prämisse ebenso falsch sein. D.h. Terme der Form \((c, c)\) und \((fc, fc)\) dürfen nicht in \(R^H\) enthalten sein.

    \(R^H = \{(f^nc, f^mc) : n \not= m \}\) für \(f, c \in T_0(S)\) und \(n, m \in \mathbb{N}\)
    Könnte man hier nicht \(R^H\) wählen als
    \(R^H = \{(f(t), t) : t \in T_0(S)\}\)
    ?
    bafnai hat geschrieben:
    Klausur SS06, Aufgabe 2 (c)


    \(g\) einstelliges Funktionssymbol, \(E\) zweistelliges Relationssymbol.
    \(\forall x \forall y [\neg Exx \wedge Exgx \wedge (Exy \rightarrow (Exfxy \wedge Efxyy))]\)

    \(S(c, g, E)\)
    \(H=(T_0(S), c^H, g^H, E^H)\)
    \(T_0(S) = \{c, gc, ggc, …\}\)
    Interpretation der Konstanten- und Funktionssymbole wie üblich über die Trägermenge, d.h. \(c^H=c\) und \(g(g^nc) = \{gg^nc \mid n \in \mathbb{N} \}\).

    Gedanke: Der erste Teil muss falsch sein (wieder ohne das \(\neg\)).

    \(E^H = \{f^nc, f^mc : n > 0, m > 0 \}\) für \(f, c \in T_0(S)\) und \(n, m \in \mathbb{N}\)
    Und hier analog:
    \(E^H = \{(t, g(t)) : t \in T_0(S)\}\)
    ?

    Und da meine andere Frage wohl untergegangen ist, würde ich sie gerne noch einmal stellen:
    fscheepy hat geschrieben:Was bedeutet bei der Übung 12, G1 in der Musterlösung der Hinweis "Wenn man einen Quantor aus der Prämisse einer Implikation herauszieht, muss man ihn dualisieren!"?
    Kann mir vielleicht jemand ein Beispiel dazu geben? Ich verstehe nicht so ganz, was hier mit dem dualisieren gemeint ist.

    Re: Herbrandmodell und Skolemisierung

    Verfasst: 27. Aug 2011 16:13
    von Ankou
    Dualisieren spielt hier auf die Dualität von \(\forall\) und \(\exists\) an und will nix weiter bedeuten, als, dass du den Quantor aus einer Negation herausziehst, da ja \(a\rightarrow b \equiv \neg a\vee n\) und \(\neg (\forall x \varphi) \equiv \exists x \neg \varphi\) und somit ersetzt
    sprich \((\forall x \varphi)\rightarrow \psi \equiv \neg (\forall x \varphi) \vee \psi \equiv \exists x \neg \varphi \vee \psi \equiv \exists x (\varphi \rightarrow \psi)\)