Hilfe zur formalen Fitch-Logik 6.26

6.26

1.A v (B^C)

2.~B gegen ~C gegen D

3.-A

4.-AVD (V-Einführung 3)

-5. B^C

--6. ~B

--7. B (Konjunktion el. 5)

--8. Widerspruch (Widerspruch Intro 6&7)

--9. AVD (Widerspruchseinführung)

--10. ~C

--11. C (Konjunktion el. 5)

--12. Widerspruch (c Intro 11&12)

--13. AVD (Widerspruch elim)

Den Rest machen Sie! Wenn Sie AVD auf der zweiten Ebene des Unterbeweises erhalten können, können Sie es mittels Disjunktion elim auf die erste bringen. Sobald Sie das getan haben, sollte der Rest einfach sein!

Das OP möchte einen formellen Nachweis für Folgendes:

Prämisse: A ∨ (B ∧ C)

Prämisse: ¬B ∨ ¬C ∨ D

Ziel: A ∨ D

Das erste, was zu beachten ist, ist, dass die zweite Prämisse zwar eine Symbolisierung von etwas zu sein scheint, aber kein gültiger Satz ist. Es ist nur ein Ausdruck. Der Umfang der Konnektoren "∨" ist mehrdeutig. Um dies zu einem Satz zu machen, den wir formell verwenden können, muss er als entweder umgeschrieben werden

(¬B ∨ ¬C) ∨ D

oder als

¬B ∨ (¬C ∨ D)

Um dies zu sehen, versuchen Sie, den Ausdruck ¬B ∨ ¬C ∨ D in einen Beweisprüfer einzugeben. Kann man überhaupt anfangen? Folgendes ist passiert, als ich versucht habe, den von forall x: Calgary Remix verwendeten natürlichen Abzug und Beweisprüfer zu verwenden :

Basierend auf unserem menschlichen Verständnis des Bindeworts „∨“ als „oder“ könnten wir informell fortfahren , den Ausdruck so zu verwenden, wie er ist, und denken, dass wir Fälle behandeln. Zuerst würden wir den Fall „¬B“, dann den Fall „¬C“ und dann den Fall D betrachten und schauen, ob wir jeweils zum Ziel „A ∨ D“ kommen.

Da wir aber einen formalen Beweis wollen, können wir so nicht vorgehen. Wir müssen Sätze verwenden, keine willkürlichen Ausdrücke, egal wie offensichtlich sie für uns sind, und wir müssen formale Regeln für Disjunktionen (dh "∨") verwenden, um jede Zeile des formalen Beweises zu rechtfertigen. Ein Proof Checker hilft uns zu überprüfen, ob wir Sätze verwenden und die Regeln befolgen.

Wenn wir als Satz ~B v (~C v D) wählen, können wir einen Beweis wie den folgenden erhalten.

Dieser Beweis zeigt eine Möglichkeit, die Fälle in beiden Prämissen zu handhaben, indem die Verbindung "V" durch Unterbeweise formal eliminiert wird.

Betrachten Sie die beiden Fälle in der ersten Prämisse. Ich nehme an, das heißt, beginne einen Unterbeweis mit "A" als Annahme in Zeile 3 und erreiche das gewünschte Ziel in Zeile 4 und ich nehme "(B ∧ C)" in Zeile 5 an und erreiche das gewünschte Ziel in Zeile 18. Mit Wenn beide Seiten der "V"-Verbindung das Ziel erreichen, kann ich das "V" eliminieren und den Beweis vervollständigen. Diese Eliminierung entlädt die beiden Annahmen, die ich gemacht habe und die durch die beiden Unterbeweise repräsentiert werden, einen für jeden Fall.

Der zweite Fall oben erforderte mehr Zeilen. Betrachten wir diese Details. Um das Ziel für den zweiten Fall "(B ∧ C)" zu erreichen, musste ich die zweite Prämisse verwenden. Ich habe den „¬B“-Fall angenommen, indem ich einen Unterbeweis mit „¬B“ als Annahme in Zeile 7 erstellt habe, und das Ziel in Zeile 9 erreicht, und ich habe den „¬C ∨ D“-Fall in Zeile 10 angenommen und die Schlussfolgerung in Zeile erreicht 17. Beachten Sie, dass "¬C ∨ D" auch eine Disjunktion ist, ein "∨"-Satz, und daher muss ich auch Fälle, dh Unterbeweise, darauf anwenden. Ich habe das in den Zeilen 10 bis 17 gemacht.

Eine der Anforderungen im OP war:

Beweisen Sie es formal, ohne DeMorgans Gesetz zu verwenden

Beachten Sie, dass ich das Gesetz von DeMorgan im obigen Beweis nicht verwendet habe. Um zu sehen, wie das Gesetz von DeMorgan hätte verwendet werden können, betrachten Sie den folgenden Beweis mit "(¬B ∨ ¬C) ∨ D".

Ich habe es getan, aber der Beweis ist ungeheuer lang. Wenn jemand weiß, wie man es vereinfacht, würde ich es schätzen. Fertig mit dem Fitch Proof Editor von Stanford :

Ich habe es getan, aber der Beweis ist ungeheuer lang. Wenn jemand weiß, wie man es vereinfacht, würde ich es schätzen. Fertig mit dem Fitch Proof Editor von Stanford:

Stanfords Fitch-Implementierung bläht Beweise notorisch auf, aber Sie sind ziemlich viel im Kreis herumgewandert, da @Houshalter

 1.|  A v (B & C)             Premise
 2.|_ (~B v ~C) v D           Premise
 3.|  |_ A                    Assumption
 4.|  |  A v D                Or Introduction 3
 5.|  A => A v D              Implication introduction 3,4
 6.|  |_ B & C                Assumption
 7.|  |  B                    And Elimination 6
 8.|  |  C                    And Elimination 6
 9.|  |  |_ ~(A v D)          Assumption
10.|  |  |  B                 Reiteration 7
11.|  |  ~(A v D) => B        Implication Introduction 9,10
12.|  |  |_ ~(A v D)          Assumption
13.|  |  |  C                 Reiteration 8
14.|  |  ~(A v D) => C        Implication Introduction 12,13
15.|  |  |_ ~B v ~C           Assumption
16.|  |  |  |_ ~B             Assumption
17.|  |  |  |  |_ ~(A v D)    Assumption
18.|  |  |  |  |  ~B          Reiteration 16
19.|  |  |  |  ~(A v D) => ~B Implication Introduction 17,18
20.|  |  |  |  ~~(A v D)      Negation Introduction 11,19
21.|  |  |  ~B => ~~(A v D)   Implication Introduction 16,20
22.|  |  |  |_ ~C             Assumption
23.|  |  |  |  |_ ~(A v D)    Assumption
24.|  |  |  |  |  ~C          Reiteration 22
25.|  |  |  |  ~(A v D) => ~C Implication Introduction 23,24
26.|  |  |  |  ~~(A v D)      Negation Introduction 17,28
27.|  |  |  ~C => ~~(A v D)   Implication Introduction 22,29
28.|  |  |  ~~(A v D)         Or Elimination 15,21,27
29.|  |  |  A v D             Negation Elimination 28
30.|  |  ~B v ~C => A v D     Implication Introduction 15,29
31.|  |  |_ D                 Assumption
32.|  |  |  A v D             Or Introduction 31
33.|  |  D => A v D           Implication Introduction 31,32
34.|  |  A v D                Or Elimination 2,30,33
35.|  B & C => A v D          Implication Introduction 6,34
36.|  A v D                   Or Elimination 1,5,36