Angenommen, A ist eine Menge von Prämissen eines Arguments und B die Schlussfolgerung dieses Arguments. Beweisen Sie, dass wenn AU {¬B} ⊢ ⊥, dann A ⊢ B

Angenommen, A ist eine Menge von Prämissen eines Arguments und B die Schlussfolgerung dieses Arguments. Beweisen Sie, dass wenn AU {¬B} ⊢ ⊥, dann A ⊢ B. (Verwenden Sie Fitch)

Ich habe keine Ahnung, wo ich anfangen soll, kann jemand helfen?

Das Operatorsymbol, das Sie für A (op) B verwenden, wird auf meinem Android-Handy nicht gerendert. Kannst du umschreiben? Zweitens ist $\cup$ kein logisches Symbol. Meinst du $A\land\nicht B$?
@mobileink - A ist eine Menge von Prämissen (aber eine andere Art von Symbolen - wie Γ - zu verwenden wäre besser ...); also ist Γ U {¬B} richtig: es bedeutet den "erweiterten" Satz von Prämissen, "aus" allen Formeln in Γ plus ¬B .
@ MauroALLEGRANZA: verstanden, mein pingeliger Punkt ist, dass FOL keine Mengenlehre ist. $ \Gamma, A\vdash B $ ist nicht unbedingt gleichbedeutend mit $\Gamma\cup A\vdash B$. (Tut mir leid, ich kann Latex-Markup nicht zum Laufen bringen.)
So steht es in vielen Lehrbüchern ... Siehe zB van Dalen , Lemma 2.4.3 (g), Seite 35.
OP: Ist Ihre Frage, wie Fitch Style Proofs funktionieren?

Antworten (2)

Angenommen AU {¬B} ⊢ ⊥

Nun müssen wir zeigen, dass A ⊢ B:

Nehmen Sie ¬B an, erhalten Sie einen Widerspruch von Prämisse A und von AU {¬B} ⊢ ⊥, und schließen Sie dann B. (Sie sollten hier die natürlichen Deduktionsschritte ausfüllen.) Das war's.

Ich stimme der Antwort von Eliran H zu .

Hier sind spezifische Schritte mit einem Proof Checker im Fitch-Stil, ohne "¬B" anzunehmen.

Der Beweis verwendet Disjunktionseinführung (∨I), bedingte Eliminierung (→E), Explosion (X) und bedingte Einführung (→I). Weitere Informationen zu diesen Regeln finden Sie in forall x: Calgary Remix .

Geben Sie hier die Bildbeschreibung ein


Verweise

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

PD Magnus, Tim Button mit Ergänzungen von J. Robert Loftis, remixt und überarbeitet von Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/