Disjunktiver Syllogismus in einem Fitch-Stilsystem

Ich versuche, ein Argument der Form zu beweisen:

  1. B
  2. ~(C & B)

Daher: ~C.

Ich kann ~(C & B) in ~C ODER ~B expandieren, und mit der Prämisse B ist klar, dass ~C der Fall ist.

Ich habe jedoch Probleme, dies mit einem Fitch-System zu beweisen. Ich habe die disjunktive Eliminierung versucht, aber ich kann nicht sehen, wie ich von einer Annahme von ~ B zu ~ C komme, also frage ich mich, ob dies der richtige Weg ist oder nicht.

Wenn jemand weiß, wie man das Äquivalent eines disjunktiven Syllogismus in Fitch zeigt, oder zumindest irgendwo herausfinden kann, wie, wäre eine Anleitung sehr dankbar.

Nehmen Sie C an. Verbinden Sie C und B, um (C & B) zu erhalten, was Prämisse 2 widerspricht. Schließen Sie ~C. [die einzigen hier verwendeten Regeln sind: &-Intro, Bottom/Absurd-Intro, ~-Elim].
In der Tat, danke. Das habe ich gerade herausgefunden. Ich machte es viel schwieriger, als es war, indem ich mich auf die disjunktive Eliminierung konzentrierte.
Hier ist eine mit De Morgan & v-Elim: Verschieben Sie die Negation in Prämisse (2), um (~C v ~B) zu erhalten. Angenommen ~C. Wiederholen Sie den Vorgang, um ~C zu erhalten. Nehmen Sie ~B an, um einen Widerspruch mit Prämisse (1) zu erhalten und schließen Sie ~C. Da aus beiden Fällen ~C folgt, folgt aus v-Elim, dass ~C.
+1 Zeigt Forschungsaufwand, ist klar und könnte sogar für andere nützlich sein. Nicht weniger wichtig, es hat die entsprechenden Tags.

Antworten (3)

Hier sind ein paar Optionen:

  • Wenn Sie eine doppelte Negationsregel haben, können Sie B in ~~B umwandeln. Dann können Sie eine disjunktive Syllogismusregel zusammen mit (~C v ~B) verwenden, um ~C zu erhalten.

  • Sie können einen indirekten Beweis versuchen, bei dem Sie C annehmen und es dann mit B verbinden, um (C & B) zu erhalten, was einen Widerspruch mit Zeile 2 ergibt, der ~C zur Folge hat.

Hey, danke für die Antwort! Das Problem, das ich habe, ist auf das Fehlen einer disjunktiven Syllogismusregel zurückzuführen. Die einzige Möglichkeit, eine v-Eliminierung in Fitch durchzuführen, ist über Proof by Cases (wobei die Fälle Unterbeweise sind). Wenn ich mit einem indirekten Beweis gehe und (C & B) bekomme, dann kann ich innerhalb von Fitch nur einen Widerspruch einführen, aus dem ich ~(C & D) ableiten kann, aber dann bin ich wieder da, wo ich angefangen habe. Ein Überblick über das System, in dem ich arbeite .
Und .... Ignorieren Sie das :). Ich habe es tatsächlich mit einem indirekten Beweis gelöst, nicht ganz sicher, wie ich diese Möglichkeit übersehen habe. Ich war so sehr darauf konzentriert, DeMorgans Gesetze in meinem Beweis zu verwenden, dass ich mich zwang, zu denken, dass die disjunktive Eliminierung der richtige Weg sein müsste. Danke schön!

Hier ist ein Ansatz, der die disjunktive Eliminierung verwendet. Angesichts des Folgenden gehe ich davon aus, dass die DeMorgan-Regeln verfügbar sind:

Ich kann ~(C & B) in ~C ODER ~B erweitern

Geben Sie hier die Bildbeschreibung ein

In Zeile 3 habe ich DeMorgan-Regeln (DeM) verwendet, um eine Disjunktion zu erhalten, die ich dann eliminieren muss, um das Ziel zu erreichen.

Um die Disjunktion zu beseitigen, muss ich beide Disjunktionen „¬C“ und „¬B“ berücksichtigen.

Das erste Disjunkt ist das einfachste, aber es kann verwirrend sein, weil es so einfach ist. Die Annahme „¬C“ für diesen Unterbeweis ist genau das, was ich zeigen möchte. Es gibt nichts mehr zu tun (zumindest für diesen Proof-Checker).

Der zweite Disjunkt verwendet die Explosion basierend auf der Beobachtung, dass die Zeilen 1 und 5 widersprüchlich sind. Dieser Beweisprüfer ermöglicht es mir, den Widerspruch (⊥) in Zeile 6 anzugeben und die Explosion (X) in Zeile 7 zu verwenden, um zu dem Schluss zu kommen, dass ich "¬C" möchte. Die von Ihnen verwendete erfordert möglicherweise etwas anderes.

Da ich für jede Disjunktion die gleiche Schlussfolgerung habe, kann ich die beiden Annahmen in den Zeilen 4 und 5 entkräften, indem ich die Regel der Disjunktionseliminierung (∨E) anführe. In diesem Beweisprüfer muss ich auf die Disjunktion selbst (3), den ersten Unterbeweis (der nur Zeile 4 ist, aber als Bereich 4-4 geschrieben wird) und den zweiten Unterbeweis (5-7) verweisen.

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/

Ihnen wurde B und ~(C ^ B) versprochen. Wenn Sie C annehmen, können Sie C ^ B aus der ersten Prämisse ableiten, was der zweiten Prämisse widerspricht, was es Ihnen ermöglicht, die Annahme durch Negationseinführung zu entkräften und somit ~C wie erforderlich abzuleiten. Das ist alles.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  |  #        Negation Elimination
|  ~C          Negation Introduction

Nun, die Version der Negationseinführungsregel, die Ihr System verwendet, kann variieren, aber das war es im Grunde.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  C->(C ^ B)  Conditional Introduction
|  |_ C        Assumption
|  |  ~(C ^ B) Reiteration
|  C->~(C ^ B) Conditional Introduction
|  ~C          Negation Introduction
Disjunktiver Syllogismus in einem Fitch-Stilsystem
AntwortenHierDatenschutz-Bestimmungen1y, 0v