Natural Deduction 7.2

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.

Natural Deduction 7.2
Hallo,

ich hab ne Frage zur Aufgabe 7.2.
Aufgabenstellung war: Zeigen Sie mit ND
(A=>B=>C) => A /\ B => C

  1. Frage:
    Da sind doch zwei Aussagen zu zeigen, oder?
    ((A=>B=>C) => A /\ B) => C
    und
    (A=>B=>C) => (A /\ B => C)

  2. Frage:
    Beim Beweis der ersten Aussage hat ein Kumpel von mir mit folgender Argumentation angefangen und volle Punktzahl bekommen:

A /\ b

A
Schon damit bin ich nicht einverstanden. Wieso darf er A/\B annehmen?
Kurz gesagt weiss er doch nur
X => Y
Aber da er X nicht annehmen kann, kann er MP nicht anwenden, oder?


Das ist nur eine Aussage, die du richtig parsen musst.
[m](A => B => C) => (A /\ B) => C[/m] ist eine äquivalente Notation für [m](A => (B => C)) => ((A /\ B) => C)[/m] (Rechtsklammerung wie bei Funktionstypen).
Um dies zu zeigen, nimmst du [m](A => (B => C))[/m] () an. Dann musst du nur noch [m](A /\ B) => C[/m] zeigen. Um dies wiederum zu zeigen, nimmst du [m]A /\ B[/m] an und musst nur noch [m]C[/m] zeigen. Per MP bekommst du aus () [m]B => C[/m] und mit erneutem MP [m]C[/m].


EDIT: siehe die anderen Antworten

1 „Gefällt mir“

Nein. Implikationen sind rechts-assoziativ; die richtige Klammerung ist also
(A=>(B=>C)) => (A /\ B => C)
Nur die Variante ist also zu zeigen (Hinweise: In der Klausur wird immer eindeutig geklammert sein, damit derartige Ambiguitäten nicht auftreten können)

Also zuerst: In natural deduction darf man jederzeit alles annehmen. Anfangen sollte er allerdings an für sich mit (A=>(B=>C)) um damit (A /\ B => C) zu zeigen. Dann muss ich A/\B annehmen um daraus C abzuleiten.


Okay, danke schonmal für die vielen Antworten.
Ich habs etz nochmal mit der richtigen Klammerung probiert. Mein Beweis sieht so aus:

Aussage: (A => (B=>C)) => ((A /\ B) =>C)
Beweis durch Widerspruch.
Annahme1 A=> (B=>C)
Annahme2 ¬((A /\ B) =>C)

2 => zu / ¬( ¬(A/\B) / C) (Wie heißt diese Regel a)
2 oder zu und ( A/\B ) /\ ¬C) (Wie heißt diese Regel b)
2 Assoziativität A /\ B /\¬C (*)

1 => zu / ¬ A / (B=>C)
1 => zu / ¬ A / (¬ B / C)
1 Assoziativität ¬ A / ¬ B / C
1 oder zu und ¬ (A /\ B /\ ¬ C) (**)

Wegen (*) und (**), dh A und ¬A folgt der Widerspruch.

Ist das ein korrekter ND Beweis?


Du scheinst ja direkt x => y zu ¬x / y umzuformen. Wenn du die Slides zu ND0 liest steht da aber keine derartige Regel. Du musst dich schon an das Repertoire der dort aufgeführten Regeln halten, ansonsten ist es kein Natural Deduction Kalkül den du anwendest.
(s. notes.pdf, Kapitel 11.4, Seiten 187-189, Slide-Nummern 335+338)
EDIT: probier mal https://bentnib.org/docs/natural-deduction.html, dort wird deine Auswahl an Regeln auf die gerade zulässigen eingeschränkt, damit findest du die Lösung wahrscheinlich leichter. Tipp: (von unten nach oben) erst 2x Introduction, dann paar mal Elimination, zuletzt 3 Äste mit assumption abschließen.

1 „Gefällt mir“

What reptor said.

Da fällt mir gerade erst auf, dass da noch ne Musterlösung fehlt :open_mouth: Sorry. Hier ist eine:

ZZ: (A => (B => C)) => ((A /\ B) => C)
------------------------------------------------------------------------
1) A => (B => C)                        (Assumption 1)
2) A /\ B                               (Assumption 2)
3) A                                    (/\-E1 auf 2) )
4) B => C                               (=>E auf 1) und 3) )
5) B                                    (/\-E2 auf 2) )
6) C                                    (=>E auf 4) und 5) )
------------------------------------------------------------------------
7) (A /\ B) => C                        (=>I auf 6), schließt Assumption 2)
8) (A => (B => C)) => ((A /\ B) => C)   (=>I auf 7), schließt Assumption 1)

Ich hab auch noch eine rumliegen, falls noch wem dieses Format besser gefällt.


Vielen Dank für die schnellen und ausführlichen Antworten :slight_smile:
Habs ein Stück mehr verstanden.


In der Klausur werden dann die Regeln für ND angegeben oder? Man muss dieses Regelwerk jetzt nicht auswendig können?


„Regelwerk“? Wenn’s dir um die Namen geht: Es gibt halt für jeden Junktor und Quantor eine Introduction und eine Elimination rule. Die Introduction rule führt einen Junktor ein, die Elimination zerlegt ihn. Mit letzterem im Kopf sollte was die Regeln genau machen eigentlich hinreichend klar sein um sich an die Details zu erinnern.

Sorry wenn das etwas „anspruchsvoll“ klingt, aber mir geht’s ja bekanntlich grundsätzlich um Verständnis, nicht um auswendig lernen :wink:

Beispiel: für => gibt es also eine Introduction rule und eine elimination rule. Wann darf ich eine Implikation A=>B „einführen“ (=introduction rule)? Naja, wenn die Implikation halt wahr ist, also wenn aus der Annahme A tatsächlich die Formel B folgt. Dann muss ich mich nur erinnern dass das in natural deduction bedeutet „Ich darf A annehmen und muss B herleiten“, dann ist die Regel klar.
Die Elimination regel sagt mir, wie ich eine Formel A=>B „ausnutzen“ darf um den Junktor zu eliminieren. Das kann ich natürlich nur, wenn ich weiß dass A wahr ist, und dann darf ich damit eben B folgern, also ist die Elimination rule natürlich
A=>B ; A

  B

(Anmerkung: Mir ist natürlich klar dass das unter Zeitdruck nicht trivial ist und man manchmal halt einfach „auswendig lernen“ muss. Also erlaube ich mir als Antwort: Auswendig lernen musst du für ND nichts, aber verstehen wie er funktioniert solltest du)