Kann mir jemand helfen, ~(AvB) |- ~(BvA) per natürlichem Abzug zu beweisen?

Tatsache 1. ¬(A ∨ B) |= ¬(B ∨ A)

Nachweisen. Die verneinte Form der Konklusion deutet auf eine naheliegende Vorgehensweise hin: Nimm (B ∨ A) an mit der Hoffnung auf einen Widerspruch. Die disjunktive Form dieser Annahme legt den zweiten Schritt nahe (Beweis-für-Fall-Analyse): Nehmen Sie B an, leiten Sie einen Satz Γ ab, nehmen Sie dann A an und leiten Sie dieses Γ erneut ab; dann unter Verwendung von (B ∨ A) und diese beiden Ableitungen schließen auf Γ. Hier ist eine Möglichkeit, diese Techniken anzuwenden:

1. ¬(A ∨ B) [ Gegeben ]
2. (B ∨ A) [ Annahme ]
3. B [ Annahme ]
4. (A ∨ B) [ ∨-Einleitung, 3 ]
5. ⊥ [ ⊥-Einleitung, 4, 1 ]
6. A [ Annahme ]
7. (A ∨ B) [ ∨-Einleitung, 6 ]
8. ⊥ [ ⊥-Einleitung, 7, 1]
9. ⊥ [ ∨-Elimination, 2, 3-5, 6-8 ]
10. ¬(B ∨ A) [ ¬-Einleitung, 2-9 ].

Tatsache 2. ¬(A ∨ ¬(A ∧ B)) ≡ ⊥

Nachweisen. Der kombinatorische Raum ist hier größer, da Sie nicht festgelegt haben, welche Regeln Sie verwenden dürfen und ob Sie dies semantisch, beweistheoretisch usw. beweisen sollen. Ich skizziere hier eine algebraische Variante. Wir wollen zeigen, dass ¬(A ∨ ¬(A ∧ B)) ≡ ⊥. Wir können wie folgt vorgehen:

1. ¬(A ∨ ¬(A ∧ B)) ≡ ⊥ [ Ziel ]
2. (A ∨ ¬(A ∧ B)) ≡ ⊤
3. (A ∨ (¬A ∨ ¬B)) ≡ ⊤ [ De Morgan ]
4. (A ∨ ¬A ∨ ¬B) ≡ ⊤ [ Assoziativität ]
5. (⊤ ∨ ¬B) ≡ ⊤
6. ⊤ ≡ ⊤.

Eine andere Methode wäre die Verwendung von Bewertungen (Wahrheitstabellen). Wir wollen zeigen, dass v(¬(A ∨ ¬(A ∧ B))) = 0. Die nützliche Tatsache ist: v(¬φ) = 1 - v(φ). Wir gehen wie folgt vor.

1. v(¬(A ∨ ¬(A ∧ B))) = 0 [ Ziel ]
2. v(A ∨ ¬(A ∧ B)) = 1
3. v(A) = 1 oder v(¬(A ∧ B)) = 1
4. v(A) = 1 oder v(A ∧ B) = 0
5. v(A) = 1 oder (v(A) = 0 oder v(B) = 0)
6. (v(A) = 1 oder v(A) = 0) oder v(B) = 0
7. 1 oder v(B) = 0
8. 1

Das ist so ziemlich das Gleiche wie oben. Sie können mit demjenigen gehen, das dem von Ihnen verwendeten System am nächsten kommt. Ich habe die Schritte nicht begründet, weil wir, wie bereits erwähnt, nicht wissen, welche Regeln Sie anwenden können.

Der Beweis, dass eine Formel φ ein Widerspruch ist, läuft darauf hinaus, daraus ⊥ abzuleiten (dh : φ ⊢ ⊥ ).

Nachweisen :

(i) ~(Av~(A&B)) --- Prämisse

(ii) ~A --- angenommen [1]

(iii) A&B --- angenommen [2]

(iv) A --- von (iii) durch &-elim

(v) ⊥ --- aus (ii) und (iv) durch →-elim

(vi) ~(A&B) --- von (iii) und (v) durch →-Intro, Entladung [2]

(vii) Av~(A&B) --- aus (vi) von v-intro

(viii) ⊥ --- aus (i) und (vii) durch →-elim

(ix) A --- von (ii) und (viii) durch RAA (oder Double Negation ), Entladung [1]

(x) Av~(A&B) --- von (ix) von v-intro

(xi) ⊥ --- aus (i) und (x) durch →-elim

Fazit :

~(Av~(A&B)) ⊢ ⊥

Erstens, kann ich zuerst ~(AvB)nach ~A&~Bden De-Morgan-Regeln wechseln?

Sicher, Sie könnten abgeleitete Regeln verwenden , aber das überzeugendste natürliche Deduktionsargument für diese Kommutivität würde die grundlegenden Schlußregeln verwenden ; wodurch gezeigt wird, dass die Kommutivität direkt aus den Einführungsregeln folgt, die linke und rechte Seitenversionen haben.

Schließlich würden Sie, wenn Sie deMorgans verwenden, eine Konjunktion umwandeln, bevor Sie erneut deMorgans verwenden. Da Sie also die Kommutierung so oder so rechtfertigen müssen, können Sie dies auch tun, ohne abgeleitete Regeln zu verwenden.

  1|_ ~(A v B)         : Premise
  2|   |_ B v A         : Assumption
  3|   |   |_ B          : Assumption
  4|   |   |  A v B      : Disjunction Introduction (3, Left)
   |   |   +
  5|   |   |_ A          : Assumption
  6|   |   |  A v B      : Disjunction Introduction (5, Right)
  7|   |  A v B         : Disjunction Elimination (2,3-4,5-6)
  8|   |  #             : Negation Elimination (1,7)
  9|  ~(B v A)         : Negation Introduction (2-8)

Und das zweite ist:

~(Av~(A&B))

Ich muss daraus schließen, dass dies ein Widerspruch ist.

Es scheint schwierig, weil das gesamte Argument verneint wird. Ich bin mir nicht sicher, was ich zuerst annehmen soll.

Verwenden Sie das Gesetz der ausgeschlossenen Mitte, nehmen Sie an, dass A oder ~A der Fall sein muss. Um diese Disjunktion zu etwas Brauchbarem zu beseitigen, müssen Sie eine Disjunktion und eine Negation einer Konjunktion einführen.

  0|  A v ~A              : Axiom (L.E.M.)
  1|_ ~(A v ~(A & B))     : Premise
  2|   |_ A                : Assumption
  3|   |  A v ~(A & B)     : Disjunction Introduction (2, R)
   |   +
  4|   |_ ~A               : Assumption
  5|   |   |_ A & B         : Assumption
  6|   |   |  A             : Conjunction Elimination (5, R)
  7|   |   |  #             : Negation Elimination (4,6)
  8|   |  ~(A & B)         : Negation Introduction (5-7)
  9|   |  A v ~(A & B)     : Disjunction Introduction (8, L)
 10|  A v ~(A & B)        : Disjunction Elimination (0,2-3,4-9)
 11|  #                   : Negation Elimination (1,10)

Revision: Dies kann etwas gekürzt werden.

  1|_ ~(A v ~(A & B))     : Premise
  2|  |_ A & B             : Assumption
  3|  |  A                 : Conjunction Elimination (2)
  4|  |  A v ~(A & B)      : Disjunction Introduction (3)
  5|  |  #                 : Negation Elimination (4,1)
  6|  ~(A & B)            : Negation Introduction (2-5)
  7|  A v ~(A & B)        : Disjunction Introduction (6)
  8|  #                   : Negation Elimination (7,1)

Im Folgenden werden Möglichkeiten aufgezeigt, diese Argumente zu beweisen.

Die erste verwendet die De-Morgan-Regeln (DeM), die Eliminierung von Konjunktionen (E), die Einführung von Konjunktionen (∧I).

Das Ziel des ersten Arguments ist es zu zeigen, dass zwei Sätze über die Disjunktion verbindend mit einer Negation verbindend über die gesamte Disjunktion pendeln. Dies erfordert, den Satz in jedes Disjunkt zu zerlegen und die Sätze dann in der anderen Reihenfolge neu zu kombinieren.

Die zweite verwendet die De-Morgan-Regeln (DeM), Konjunktions-Eliminierung (∧E), Doppel-Negativ-Eliminierung (DNE) und Widerspruchseinführung (⊥I).

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/