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.
Problem 10.1.2
Hallo,
wollte mal fragen ob mein Beweis zum Lemma so passt.
Ich finde keinen Fehler, aber er ist viel kürzer als die Musterlösung, was mich überrascht…
Beweis mit ND. Aussage:
¬ ∀ Y.P(Y) => ∃ Y.¬P(Y)
- Ann ¬ ∀ Y.P(Y)
- [Z/Y] ¬ P(Z) (aus 1)
- ∃-Intr. ∃Z.¬P(Z)
- Z:=Y ∃Y.¬P(Y)
- =>-Intr. ¬Y.P(Y) => ∃Y.¬P(Y)
dein 2) funktioniert nicht.
für ¬ ∀ Y.P(Y) greift nicht die ∀Elim Regel, für ∀ Y.¬P(Y) würde sie z.B. aber gehen.
1 „Gefällt mir“
Außerdem ist für mich nich klar, welche Regeln von ND^1 denn deine Zeile 4) ist.
Das wichtige bei den Kalkülen der Vorlesung ist ja, dass sie sound + complete mit allen ihren Regeln sind. Sobald man nun eine Regel/ Abkürzung benutzt, die nicht zu den Regeln gehört, kann man sich nicht mehr sicher sein, ob denn der neue, erweiterte Kalkül mit der neuen Regel/Abkürzung immer noch sound + complete ist. Wenn nicht, kann man plötzlich Dinge beweisen, die nicht wahr sind oder halt nicht mehr alle wahren Dinge beweisen. Das ist die Theorie dahinter, warum man sich nur an die Regeln der Vorlesung halten muss. (oder für neue Regeln/Abkürzungen=Lemmas zeigen muss, dass sie im Kalkül her leitbar sind)
What tyr said.
Die Eliminationsregel für ¬ in natural deduction ist in der anwendung etwas unpraktisch und tritt eigentlich immer mit der false-introduction zusammen auf.
EDIT: Hab gerade gemerkt dass ich entsprechend auch die regeln durchgehend falsch benannt hab; ist jetzt korrigiert 
Also vielleicht um die Musterlösung zu erklären:
Wenn du ¬A hast kannst du damit nur (durch F-Introduction) was anfangen, wenn du A zeigst und einen widerspruch herleitest. Beweis per Widerspruch halt.
für ¬ ∀ Y.P(Y) => ∃ Y.¬P(Y) bedeutet das, du musst ¬∀Y.P(Y) annehmen und ∃Y.¬P(Y) herleiten. Die Annahme kannst du aber nur ausnutzen wenn du ∀Y.P(Y) zeigen kannst und einen Widerspruch erzeugst. Wenn du nen Widerspruchsbeweis führen willst musst du aber natürlich das Gegenteil von dem Annehmen was du eigentlich zeigen willst, du musst also ¬∃Y.¬P(Y) annehmen und daraus irgendwie ∀Y.P(Y) ableiten.
Und wir sind wieder in der selben Situation: Wir brauchen nen Widerspruch um Annahme 2 irgendwie auszunutzen.
Es gibt Grundsätzlich zwei Möglichkeiten in Natural Deduction ein Beweisziel zu erreichen:
- Indem ich sie aus einer “größeren Formel” per elimination ableite oder
- Indem ich sie mit ner Introduction-regel einführe
Eliminieren kann ich nichts (Meine Annahme hab ich ja alle soweit ausgenutzt wie es ging), also bleibt ∀-introduction - ich muss also P(Y) beweisen. Meine zweite Annahme ¬∃Y.¬P(Y) kann ich eben nur per Widerspruch ausnutzen, also nehme ich ¬P(Y) an, beweise damit sofort ∃Y.¬P(Y) und hab nen widerspruch (F-Introduction). Also war die Annahme ¬P(Y) falsch, also gilt (¬-Introduction) ¬¬P(Y) = P(Y). Ich kann die ∀-introduction machen, hab meinen widerspruch zu annahme 1 und bin fertig 