In fitch, S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R)

Ein anderer Ansatz besteht darin, ~(Q ∨ R) anzunehmen, wie ich es in Zeile 9 unten getan habe. Dies führt zu einem Widerspruch in Zeile 17, sodass Sie die andere Hälfte der Disjunktion vervollständigen können.

1 | (S→(R ∨ P)) Prämisse
2 |_ (P→(~R→Q)) Prämisse
3 | |_ S Annahme
4 | | (R ∨ P) 1,3 →E
5 | | |_ R Annahme
6 | | | (Q ∨ R) 5 ∨I
7 | | |_ P Annahme
8 | | | (~R→Q) 2,7 →E
9 | | | |_ ~(Q ∨ R) Annahme
10 | | | | |_ ~R Annahme
11 | | | | | Q 8,10 →E
12 | | | | | (Q ∨ R) 11 ∨I
13 | | | | | ⊥ 9,12 ⊥I
14 | | | | ~~R 10-13 ~I
15 | | | | R 14 ~E
16 | | | | (Q ∨ R) 15 ∨I
17 | | | | ⊥ 9,16 ⊥I
18 | | | ~~(Q ∨ R) 9-17 ~I
19 | | | (Q ∨ R) 18 ~E
20 | | (Q ∨ R) 4,5-6,7-19 ∨E
21 | (S→(Q ∨ R)) 3-20 →I

Hinweis

Nehmen Sie S an und leiten Sie R ∨ P aus 1. Prämisse ab.

Nun zwei Unterbeweise, für ∨ -elim:

1) Nehme R an und leite Q ∨ R durch ∨ -intro ab, und fertig.

2) Nehmen Sie P an und leiten Sie ¬R → Q aus der 2. Prämisse ab.

Verwenden Sie nun R ∨ ¬R (Excluded Middle) für ein neues ∨ -elim:

2.1) Nehmen Sie R an und leiten Sie Q ∨ R ab .

2.2) Nimm ¬R an und leite Q aus ¬R → Q ab und leite dann Q ∨ R ab .

Nachdem wir jeweils Q ∨ R hergeleitet haben, können wir schließen mit:

S → (Q ∨ R)

von → -Einleitung.

Wie Pe habe ich einen Widerspruchsbeweis durchgeführt ... und indem ich die Annahme von ~ (Q v R) früher im Beweis gemacht habe (und Fitchs Abkürzung ausgenutzt habe, um zu erlauben, dass ~ Intro verwendet wird, während die Negation der Annahme beseitigt wird), Ein paar Zeilen konnte ich kürzen:

Was mich an diesem Beweis wirklich interessiert, ist, dass der mit R beginnende Unterbeweis zweimal verwendet wird: als Beweis durch Widerspruch, um auf ~R zu schließen, sowie als Beweis durch Fälle, um den Widerspruch zu erhalten. So etwas sieht man nicht allzu oft.

Hier ist ein Beweis mit einem Beweisprüfer im Fitch-Stil .

Die ersten beiden Zeilen enthalten die Prämissen.

Da das Ziel ein Konditional ist, habe ich den Vordersatz S in einem Unterbeweis ab Zeile 3 angenommen. Mein Ziel war es, den Konsequenten Q v R zu erreichen , was ich in Zeile 13 getan habe. Dadurch konnte ich die Annahme aufheben und schließen den Unterbeweis durch Einführung einer Bedingung zur Vervollständigung des Beweises.

Um zu Zeile 13 zu gelangen, habe ich die Negation dieser Konsequenz angenommen, die ich beweisen wollte, indem ich einen neuen Unterbeweis begonnen habe. Ich wollte einen Widerspruch erreichen, was ich in Zeile 12 tat. Die Verwendung des disjunktiven Syllogismus (DS) in Zeile 8 ermöglichte es mir, die beiden Fälle der Disjunktion in Zeile 6 kurz zu testen.

---

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/