Wie man P ∨ Q : ~ (~P & ~Q) mit natürlichem Abzug beweist

Diese Antwort wird einen Beweis liefern, der auf der Logik von Paul Tomassi basiert . Das Problem ist 1.17 in Aufgabe 3.9 auf Seite 106.

P gegen Q : ~(~P & ~Q)

P v Q ⊦ ~(~P & ~Q)
{1} 1. P-v-Q-Prämisse
{2} 2. P Annahme für vEliminierung
{3} 3. ~P & ~Q Annahme für RAA
{3} 4. ~P 3 &E
{2,3} 5. P & ~P 2,4 &I
{2} 6. ~(~P & ~Q) 3,5 RAA
{7} 7. Q Annahme für VEliminierung
{8} 8. ~P & ~Q Annahme für RAA
{8} 9. ~F 8 &E
{7,8} 10. F & ~F 7,9 &I
{7} 11. ~(~P & ~Q) 8,10 RAA
{1} 12. ~(~P & ~Q) 1,2,6,7,11 vE

Die Beschreibung von reductio ad absurdum (RAA) befindet sich auf den Seiten 101-5.

Die Beschreibung von vElimination (vE) befindet sich auf den Seiten 86-9.

Die Beschreibung von &Elimiantion (&E) und &Introduction (&I) befindet sich auf den Seiten 50-2.

Dieser Beweis verwendete 12 statt 11 Zeilen.

Bezug

Tomassi, P. (1999). Logik (London und New York.

Hier ist Ihr leicht modifizierter Beweis ...

[1] P ∨ Q --- Prämisse

[2] ~P & ~Q --- Annahme für RAA

[3] ~P --- ab 2 von &E

[4] ~Q --- ab 2 von &E

[5] P --- Annahme aus [1] für vE (1.)

[6] ~P & P --- aus [3] und [5] von &I

[7] ~(~P & ~Q) --- aus [2] und Widerspruch [6] von RAA

[8] Q --- Annahme aus [1] für vE (2.)

[9] ~Q & Q --- aus [4] und [8] von &I

[10] ~(~P & ~Q) --- aus [2] und Widerspruch [9] von RAA, entladende Annahme [2]

[11] ~(~P & ~Q) --- aus [5]-[7] und [8]-[10] und [1] von vE, entladende Annahmen [5] und [8]

Hier ist eine Möglichkeit, dies basierend auf Klements Beweisprüfer zu beweisen:

In Zeile 2 übernehme ich die Negation dessen, was ich zeigen möchte. Dies ist ein ad absurdum geführtes Argument, das es mir ermöglichen soll, eine Negation auf 10 einzuführen. Obwohl ich die Negationseinführungsregel nicht in Ihrer Liste sehe, kann Ihnen dies eine Vorstellung davon geben, wie Sie vorgehen sollen.

In den Zeilen 3 und 4 habe ich die Eliminierung von Konjunktionen verwendet und in den Zeilen 5 bis 8 habe ich eine Eliminierung von Disjunktionen eingerichtet, die Online 9 abgeschlossen hat. Es beinhaltete die Einführung eines Widerspruchs in den Zeilen 6 und 8. Ich habe keine Widerspruchseinführung in Ihrer Regelliste gesehen, aber die reductio ad absurdum ließ mich vermuten, dass es akzeptabel sein könnte.

Hier ist ein Beweis, der Disjunktionssyllogismus (DS) verwendet, eine abgeleitete Regel, um die Disjunktionsbeseitigung abzukürzen. Das steht nicht auf Ihrer Liste. Ich biete es nur an, um eine andere Perspektive zu geben, wie dies bewiesen werden könnte.

Schließlich ist hier ein kürzerer Beweis (zumindest in dem von mir verwendeten Beweisprüfer), der die De-Morgan-Regel (DeM) verwendet. Das steht nicht auf der Liste der zulässigen Regeln, aber ich biete es als eine andere Perspektive auf das Problem an, wenn diese abgeleitete Regel verfügbar wird.

Das OP lieferte einen Beweisversuch. Das scheint zu funktionieren. Wenn ich die Regeln für den von mir verwendeten Beweisprüfer verwende, erhalte ich Folgendes:

Es gibt zwei Unterschiede. Für Zeile 6 im Beweis des OP brauchte ich drei Zeilen, meine 6, 7 und 8. Damit Zeile 11 die Kontraktion erreicht, musste ich in meiner Zeile 13 eine Widerspruchseinführung (⊥I) verwenden. Ansonsten sind die Beweise ähnlich.

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/