Not logged in. · Lost password · Register

The_Tricker
Member since Feb 2013
24 posts
Subject: 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)

1) Ann        ¬ ∀ Y.P(Y)
2) [Z/Y]      ¬ P(Z)   (aus 1)
3) ∃-Intr.    ∃Z.¬P(Z)
4) Z:=Y      ∃Y.¬P(Y)
5) =>-Intr. ¬Y.P(Y) => ∃Y.¬P(Y)
tyr
Avatar
Member since Oct 2014
93 posts
+1 Jazzpirate
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.
"Debugging is like doing surgery by randomly squeezing stuff in a patient's body and going like 'lmao tell me when this guy stops breathing'." -- Orteil, Creator of Cookie-Clicker
tyr
Avatar
Member since Oct 2014
93 posts
In reply to post #1
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)
"Debugging is like doing surgery by randomly squeezing stuff in a patient's body and going like 'lmao tell me when this guy stops breathing'." -- Orteil, Creator of Cookie-Clicker
Jazzpirate
Member since Oct 2016
803 posts
In reply to post #1
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 :D

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 :)
This post was edited on 2018-02-11, 14:24 by Jazzpirate.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen