Wir glauben das dieser Beweis Falsch ist. Kann uns jemand den Denkfehler aufzigen? (Oder sagen das wir doch richtig lagen):

!(Ax Ey Az Ew (R(w,z) -> R(x,y))) !Ey Az Ew (R(w,z) -> R(c,y)) !Az Ew (R(w,z) -> R(c,t1)) !Ew (R(w,d) -> R(c,t1)) !(R(t2,d) -> R(c,t1)) // jetzt setzten wir t2=c & t1=d R(c,d) !R(c,d) _|_ q.e.d.

Dass die oberste Formel keine Kontradiktion ist,
sieht man schon am Modell mit Universum {1,2}
und mit R als {(1,2)}.

Der Fehler ist, dass bei der Gamma-Expansion
ein bestimmter geschlossener Term eingesetzt
werden muss und keine Term-Variable, deren genauer
Inhalt erst später definiert wird (im Prinzip also dort,
wo ihr einen Kommentar machen musstet um euren
Schritt zu begründen [28]). Das liegt daran, dass bei
diesem Vorgehen ja die Belegung der durch Allquantoren
gebundenen Variablen in bestimmter Weise (in dem Fall
durch die Regel t2=c und t1=d) von der Belegung der
durch Existenzquantoren gebundenen abhängt. Ihr habt
also nur die Belegungen betrachtet, für die y=x und w=z
ist, womit die oberste Formel nicht erfüllbar ist. Da aber
eine Formel u.U. durch ganz andere Belegungen erfüllt
werden kann (wo eben diese Abhängigkeit nicht gegeben
ist), sind solche Schritte im Tableau nicht erlaubt.

Also: Statt Termvariablen immer konkrete geschlossene
Terme in der Gamma-Expansion verwenden.

[latex](\forall x)(\exists y)(\forall z)(\exists w)(R(w,z) \supset R(x,y))[/latex] gibt es keinen tableau-beweis, d.h.:

[latex]\not\vdash_{ft} (\forall x)(\exists y)(\forall z)(\exists w)(R(w,z) \supset R(x,y))[/latex]

das initiale tableau ist folgendes:
[latex]\neg (\forall x)(\exists y)(\forall z)(\exists w)(R(w,z) \supset R(x,y))[/latex]

wenn man nun berücksichtigt, dass:

• mit der [latex]\delta[/latex] regel sowohl neue terme eingeführt als auch schon vorhandene genutzt werden dürfen und
• mit der [latex]\gamma[/latex] regel ausschließlich noch nicht im tableau verwendete parameter eingeführt werden dürfen

kann man ziemlich schnell sehen, dass das tableau nicht abgeschlossen werden kann.

ups, zu spät…[2]

wenn man nun berücksichtigt, dass:

• mit der [latex]\delta[/latex] regel sowohl neue terme eingeführt als auch schon vorhandene genutzt werden dürfen und
• mit der [latex]\gamma[/latex] regel ausschließlich noch nicht im tableau verwendete parameter eingeführt werden dürfen

Umgekehrt [28]

Das mit den Variablen hatten wir gemacht aus der Überlegung, dass wir ja eigentlich die Quantorenreihenfolge ohne das es stört verändern können und so sozusagen die Universalexpansion nach den anderen zwei machen könnten. Heist das denn jetzt, wenn ich so ein Tableau Beweis hab (s.u.) müsste ich sozusagen begründen, warum ich die Gamma-Variable auf a beschränken kann?

!(Ax [(P(x) --> Q(x)) & P(a)] --> Q(a)) Ax[(P(x) --> Q(x)) & P(a)] !Q(a) P(a) | | !P(a) Q(a) //Hier müsste das Begründet werden? In der Art die // einzige Belegung von x die Ax[(P(x) --> Q(x)) & P(a)] in // diesem Fall wahr macht ist a?

Huch?! Nein, nein, Quantoren koennt ihr nicht einfach beliebig vertauschen!
Beispiel:

Fuer jede natuerliche Zahl n gibt es eine natuerliche Zahl m mit n < m
Formal:
A n E m <(n,m)

(z.B. m := n + 1)

Aber andersherum

E m A n <(n,m)

macht das keinen Sinn (es gibt eine natuerlich Zahl, die groesser ist als alle natuerlichen
Zahlen - das geht nicht).

Froehliche Gruesse

Das mit den Variablen hatten wir gemacht aus der Überlegung, dass wir ja eigentlich die Quantorenreihenfolge ohne das es stört verändern können und so sozusagen die Universalexpansion nach den anderen zwei machen könnten.

Das geht nicht (siehe anderes Posting).

Heist das denn jetzt, wenn ich so ein Tableau Beweis hab (s.u.) müsste ich sozusagen begründen, warum ich die Gamma-Variable auf a beschränken kann?

Nein, bei dem Tableau-Verfahren musst du eigentlich gar nichts
begründen. Deshalb ists ja ein Algorithmus (d.h. im Fall der PL nur ein
Semi-Entscheidungsverfahren), der schon korrekt ist, wenn man sich nur
an seine Regeln hält.

Nach der Regel der Gamma-Expansion darfst du (ganz ohne Begründung)
jeden geschlossenen Term für die betreffende gebundene Variable einsetzen.
In dem Beispiel also auch a.

Hallo, ist das jetzt als Lösung für die Aufgabe unter Zuhilfenahme von "Free-Variable Semanic Tableaux" (S. 166 . Fitting, First-Order and Automated Theorem Proving)?

!(Ax Ey Az Ew (R(w,z) -> R(x,y))) !Ey Az Ew (R(w,z) -> R(c,y)) !Az Ew (R(w,z) -> R(c,t1)) !Ew (R(w,f(t1)) -> R(c,t1)) !(R(t2,f(t1)) -> R(c,t1)) R(t2,f(t1)) !R(c,t1) sigma{t1/c,t2/c} R(c,f(c)) !R(c,c)
Es läst sich keine Substitution finden, die zu einem Abschluss führt und somit ist die Uhrsprüngliche Formel nicht gültig.

Hilfee, also ich hab bei Aufgabe 9.1
!(Ax Ey Az Ew (R(w,z) -> R(x,y)))
immer noch nicht verstanden woran man sieht das es kein Tableau Beweis für gibt.
Kann mir jemand den Unterschied zwischen gamma und delta Expansion erklären?
Bei der delta Expansion wird ein neuer Parameter eingeführt,der nicht in der Formelmenge
vorhanden ist (zB. a,b,c…?)
Die gamma Expansion fügt einen neuen geschlossenen Term in die Gleichung ein?
(zB. t1,t2..? wobei im Skript bei einigen gamma expansionen auch einfach nur (a,b,c,d..)
eingefügt wurden. Verwirrt. Hilfe!

Ist es richtig, das man erkennen kann das es kein tableau beweis für die obige formel gibt,
weil man2 delta und 2 gamma expansionen ausführen muss und somit bei
(R(w,z)->R(x,y))
zwei Terme entstehen, die nicht zum Abschluss führen können?