Wie beweist man '(B→C)→¬A' aus '(A→B)∨C' und '(A→¬C)' in Fitch?

Ich versuche, mich durch diesen Fitch-Beweis durchzuarbeiten, und bin mir nicht sicher, was ich falsch mache, aber ich bleibe hängen, egal was ich versuche.

Erster Versuch:

Zweiter Versuch:

Antworten (2)

Dies als Beweis für den Fitch-Stil zu tun, ist sehr mühsam, aber ich bekomme:

Geben Sie hier die Bildbeschreibung ein

Es wäre tatsächlich schneller, dies mit der Kurzschlussmethode oder einer Wahrheitstabelle zu beweisen.

Mit der Kurzschlussmethode

  1. die Schlussfolgerung ist falsch, wenn die linke Seite von (B -> C) -> ~A WAHR ist, aber die rechte Seite FALSCH ist
  2. Das bedeutet also, dass A wahr, WAHR sein müsste, damit die Schlussfolgerung falsch endet.
  3. Wenn A wahr ist, dann kann die erste Prämisse nur wahr sein, wenn C FALSCH ist.
  4. Wenn C falsch ist, muss B FALSCH sein, damit die linke Seite der Schlussfolgerung WAHR ist.
  5. Wenn B FALSCH ist, dann verwandelt sich Prämisse zwei in: (WAHR -> FALSCH) v FALSCH --> FALSCH oder FALSCH, also können wir nicht beide Prämissen wahr und die Schlussfolgerung falsch machen.

Verweise

Kevin Klements JavaScript/PHP-Beweiseditor und -prüfer im Fitch-Stil für natürliche Deduktion http://proofs.openlogicproject.org/

Die von Ihnen angegebene „Kurzschlussmethode“ ist sehr hilfreich, um zu verstehen, warum ich in Zeile 4 mit der Annahme von A beginnen muss, bevor ich B. usw. annehme, um zu meiner Schlussfolgerung zu gelangen. Danke dir

Dein erster Versuch ist der Beste.

Sie haben richtigerweise einen bedingten Beweis verwendet und mit der Annahme B->C begonnen. Es sollte jedoch beachtet werden, dass Sie zur Ableitung der Konsequenz eine Negation einführen müssen. In der Tat sehe ich, dass Sie das erkannt haben, aber warum haben Sie nicht gesehen, dass das nächste, was Sie annehmen mussten, A war, um einen Widerspruch abzuleiten?

|  (A -> B) v C         premise I
|_ A -> ~C              premise II
|  |_ B -> C            assumed (for conditional proof)
|  |  |_ A              assumed (for negational proof)
:  :  :  :
|  |  |  #              negation eliminated (hopefully)
|  |  ~A                negation introduced 
|  (B -> C) -> ~A       conditional introduced

Nun ist eine Ihrer Prämissen A->~C, also können wir sofort ~C im Kontext ableiten und haben unseren Widerspruch, wenn die andere Prämisse C unter beiden Annahmen beinhaltet.

Nun, diese andere Prämisse ist eine Disjunktion, die durch einen Fallbeweis eliminiert wird. Dadurch wird tatsächlich C in jedem Fall abgeleitet (in einem Fall ist es sogar trivial).

Sie müssen also einen Fallbeweis in einen Negationsbeweis in einen bedingten Beweis einbetten. Und du wirst fertig sein.

|  (A -> B) v C         premise I
|_ A -> ~C              premise II
|  |_ B -> C            assumed (for conditional proof)
|  |  |_ A              assumed (for negational proof)
|  |  |  ~C             conditional eliminated
|  |  |  |_ A -> B      left case assumed
:  :  :  :  :           ... (It should be clear, what you need to do here.)
|  |  |  |  C           derived (hopefully)
|  |  |  (A -> B) -> C  conditional introduced
|  |  |  |_ C           right case assumed
|  |  |  C -> C         conditional introduced
|  |  |  C              disjunction eliminated
|  |  |  #              negation eliminated
|  |  ~A                negation introduced
|  (B -> C) -> ~A       conditional introduced

TL;DR Wann immer Sie voraussehen, dass Sie eine Disjunktion eliminieren müssen, verschieben Sie dies um so viele erhöhte Annahmen wie möglich. Versuchen Sie, einen Berg mit zwei Gipfeln zu bauen, anstatt zwei ganze Berge.