Klausur ws2016 A5 Formale Deduktion

ich komme nicht weiter

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Klausur ws2016 A5 Formale Deduktion
meine Versuche ist hier, leider scheiterte ich , kann jemand kurz anschauen , wie ich weitermachen soll

https://www.dropbox.com/s/brl47mq61fwec7l/A5.jpg?dl=0,


Du solltest zuerst Allquantor-Elimination machen, dein nächstes Ziel ist dann R(c,c). R(c,c) bekommst du indem du die Implikations-Elim auf Zeile 10 anwendest.


Dropbox - 15.jpg - Simplify your life meinst du so?


Zeilen 4, 16 und 17 kannst du dir eigentlich sparen. Wenn du über c gehst, kannst du am Ende eine Allquantoreinführung machen und musst dann unter c nur R(c,c) zeigen, das Ergebenis steht bei dir ja schon in der Zeile 15.
Du hast in Zeile 2 noch einen Fehler, da die Annahme ->R(x,z) und nicht → R(z,z) ist.


warum soll ich die 16,17 sparen?? ich kann dich nicht verstanden, wenn du die Aufgabe schon gelöst? kannst du noch dein Denkweg kurz erklären?? :huh:


Ich hab es noch nicht vollständig gelöst. Aber die Allquantor-Einführung setzt voraus, dass du ein frisches c hast. Dh wenn du unter c R(c,c) herleiten kannst, dann hast du ∀R(x,x). Also musst du nicht erst -∀R(x,x) annehmen um dann anschließend --∀R(x,x) herzuleiten. Es ist per se nicht falsch, aber überflüssig, weil dir -∀R(x,x) ansonsten im ganzen Beweis nichts bringt.

Ich weiß noch nicht ganz, welche Regel ich nutzen soll, um auf R(c,c) zu kommen. Wenn ich x durch c und und y durch d ersetze, kann ich z nicht auch einfach durch c ersetzen. Irgendwie muss man die 2. Annahme zu R(c, d) ∧ R(d, c) → R(c, c) formen. Aber dafür muss ich ja erst R(c, c) herleiten, was den vorherigen Schritt schon wieder überflüssig macht :confused:


du hast Recht, was ich gemacht, die Schritte sind überflüssig! und eine Frage , ich weisse auch R(c, d) ∧ R(d, c) → R(c, c) so leiten, aber ich weisse nicht mehr warum kann z als c einzusetzen, warum darf man nicht mehr anderen Variable benennen,


Ich habe die Aufgabe jetzt wie folgt gelöst, bin mir aber nicht sicher ob das so passt. Im Skript wurde im Beweis der “Transitivität der Subsumption” (Seite 33), wurde sowohl x als auch z durch d ersetzt. Bin mir noch etwas unsicher was Zeile 13 & 14 anbelangt, sprich wie ich das R(c,c) aus dem Unterbeweis in den Hauptbeweis bekomme.

1 | ∀x∃y(R(x, y))
2 |∀x∀y∀z((R(x,y)∧R(y, z)) → R(x, z))
3 |∀x∀y(R(x, y) → R(y, x))
4 ||c
5 ||R(c, y) (∀E) 1 [c/x]
6 |||d R(c, d)
7 |||R(c, d) → R(d, c) (∀E) 3 [d/y]
8 |||(R(c, d) ∧ R(d, c)) → R(c, c)) (∀E) 2 [c/z]
9 |||R(d, c) (→E) 6, 7
10|||R(c, d) ∧ R(d, c) (∧I) 6, 9
12|||R(c, c) (→E) 10, 11
13|||∃x.(R(x,x) (∃I)
14||R(x, x) (∃E) 6- [x/x]
15|∀x(R(x, x)) (∀I) 4-14


ich wollte gerade auch meine Lösung posten . ich habe ähnliches bekommen, was ich nicht habe, ist genau die zeile 13, warum sollte ∃x.(R(x,x)
[color=crimson]
1 | ∀x∃y(R(x, y))
2 |∀x∀y∀z((R(x,y)∧R(y, z)) → R(x, z))
3 |∀x∀y(R(x, y) → R(y, x))
4 ||c
5 ||∃yR(c, y) (∀E) 1
6 |||d R(c, d)
7 |||R(c, d) → R(d, c) (∀E) 3 [d/y]
8 |||(R(c, d) ∧ R(d, c)) → R(c, c)) (∀E) 2 [c/z]
9 |||R(d, c) (→E) 6, 7
10|||R(c, d) ∧ R(d, c) (∧I) 6, 9
12|||R(c, c) (→E) 10, 11
13|∀x(R(x, x)) (∀I) 4-12

[/color]


Wenn Z12 wahr ist, dann ist Z13 trivialerweise doch auch wahr. In Z12 wird explizit eine Belegung angegeben wofür der allgemeine Ausdruck R(x,x) wahr ist, nämlich R(c,c). Daher existiert ein x, sodass R(x,x) wahr ist, nämlich x = c.