Wie beweist man bei Fitch „P“ aus der Prämisse „(¬P ∨ Q)→P“?

Wie beweist man bei Fitch „P“ aus der Prämisse „(¬P ∨ Q)→P“?

Man nimmt Nicht-P an und verwendet einen Reduktion-auf-Absurditäts-Beweis.

|_ (~P v Q) -> P   Premise
|  |_ ~P           Assumption
|  |  :            :
|  |  :            :
|  |  :            :
|  ~~P             Negation Introduction
|  P               Double Negation Elimination

Hier ist eine Möglichkeit, dies zu beweisen, indem man die Regeln in Klements Fitch-Style Proof Checker verwendet. Die Regeln sind in forallx beschrieben . Beide sind über die unten stehenden Links verfügbar und eignen sich gut als Zusatzmaterial für den von Ihnen verwendeten Text.

Dieser Beweis verwendet das Gesetz des ausgeschlossenen Dritten (LEM). Um dies zu verwenden, nehme ich eine einfache Aussage und ihre Negation und versuche, aus beiden das gleiche Ergebnis abzuleiten. Wenn ich das gleiche Ergebnis erhalte, kann ich mich auf das Gesetz des ausgeschlossenen Dritten berufen. Hier habe ich „P“ und „¬P“ gewählt, weil eines davon, „P“, das Ziel selbst ist.

Für "P" brauche ich nichts weiter zu tun, als den Unterbeweis mit Annahme "P" hinzuzufügen. Für "¬P" verwende ich die Disjunktionseinführung, um Zeile 4 zu erhalten, und dann die bedingte Eliminierung in Zeile 5 (Modus Ponens), um "P" zu erhalten. Ich habe in beiden Fällen das Ziel „P“ erreicht und kann somit die beiden Annahmen auf Zeile 2 und 3 entladen und bin am Ende des Beweises angelangt.

Referenz

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/