Beweisen Sie A ∨ D aus A ∨ (B ∧ C) und (¬ B ∨ ¬ C) ∨ D ( LPL Q6.26) ohne Verwendung von --> oder materieller Implikation

Dies ist eine wiederholte Frage: Sprachlogik und Beweis F. 6.26

Geben Sie unter Verwendung der natürlichen Abzugsregeln einen formalen Beweis von

A ∨ D

aus den Räumlichkeiten

  1. A ∨ (B ∧ C)
  2. (¬ B ∨ ¬ C) ∨ D

Das LPL-Lehrbuch hat noch keine materiellen Auswirkungen oder das implizierte Symbol "-->" eingeführt, und die im obigen Link gegebene Antwort erfüllt die Frage im Buch NICHT, und ich war überrascht, dass der Benutzer die Antwort als angemessen akzeptierte.

Die Antwort ist bis Schritt 22 gültig, da das Lehrbuch diese Schrittformen nicht eingeführt hat. Gibt es eine Möglichkeit, diesen Beweis und andere Regeln zu verwenden, um die Implikation zu zeigen, dass ~A --> D und A --> ~D daher AVD ?

Wie würde ich diesen Beweis in Fitch ohne --> oder materielle Implikation lösen?

Regeln, die Sie verwenden können:

  • V intro, elim (Disjunktion)

  • ^ Einleitung, elim (Konjunktion)

  • ~ Intro, elim (Verneinung)

  • Widerspruch Intro, elim

  • = Einleitung, elimin

Antworten (3)

|  1) A ∨ (B ∧ C) --- premise
|_ 2) (¬ B ∨ ¬ C) ∨ D --- premise
|  |_ 3) A --- assumed [a] from 1) for ∨-elim
|  |  4) A ∨ D --- from 3) by ∨-intro
|  /
|  |_ 5) (B ∧ C) --- assumed [b] [from 1) for ∨-elim
|  |  |_ 6) D --- assumed [c] from 2) for ∨-elim
|  |  |  7) A ∨ D --- from 6) by ∨-intro
|  |  /
|  |  |_ 8) (¬ B ∨ ¬ C) --- assumed [d] from 2) for ∨-elim
|  |  |  9) B --- from 5) by ∧-elim
|  |  | 10) C --- from 5) by ∧-elim

Nun leiten wir mit einem dritten ∨-elim ⊥ (den Widerspruch) sowohl aus 8), 9) als auch aus 8), 10); daher :

|  |  | 11) ⊥ --- from 8) by ∨-elim
|  |  | 12) A ∨ D --- from 11) by ⊥-elim

Nachdem wir A ∨ D aus 6) D und 8) (¬ B ∨ ¬ C) abgeleitet haben, haben wir:

|  | 13)  A ∨ D --- from 2) by ∨-elim discharging assumptions [c] and [d]

Nachdem wir A ∨ D sowohl aus 3) A als auch 5) (B ∧ C) abgeleitet haben, haben wir:

| >14)  A ∨ D --- from 1) by ∨-elim discharging assumptions [a] and [b].

Fazit :

A ∨ (B ∧ C), (¬ B ∨ ¬ C) ∨ D ⊢ A ∨ D --- aus 1), 2) und 14).

Ich verstehe nicht, wo die Unterbeweise beginnen und enden oder wie tief sie aus dieser Antwort verschachtelt sind. Wenn Sie sich die ursprüngliche Antwort von Philosophy.stackexchange.com/questions/15651/… ansehen und sie so formatieren könnten, wäre das sehr hilfreich
Wie, was bedeutet " A --- angenommen [a] von 1) für ∨-elim" bedeutet, klingt wie, Angenommen A, also A, weil v elim von Schritt 1. Dies wird nicht überprüft.
Der Unterbeweis beginnt mit den Annahmen [a] und [b] : benötigt für ∨-elim aus 1) und endet bei Schritt 14) mit der Erledigung der beiden Annahmen. Siehe hier für eine Erklärung.

Der Beweis wird ein großes v-elim auf A v (B ^ C) sein. Sie hätten das v-elim aber auch einfach auf (~B v ~C) v D machen können. Ich habe versucht, die Notation dem Lehrbuch anzupassen, obwohl ich zugeben muss, dass es ziemlich grausam ist. Es könnte sich lohnen, es von Hand zu kopieren, nur damit Sie sehen können, wie das Scoping für die Unterbeweise funktioniert.

 1. |A v (B ^ C)         Premise
 2. |(~B v ~C) v D       Premise
    ---------------
 3. ||A                  Assumption for v-elim
    ---------------
 4. ||A v D              3, v-intro
    |
 5. ||B ^ C              Assumption
    ---------------
 6. ||B                  5, ^-elim
 7. ||C                  6, ^-elim
 8. |||D                 Assumtion
    ---------------
 9. |||A v D             8, v-intro
    ||
10. |||~B v ~C           Assumption
    ---------------
11. ||||~B               Assumption
    ---------------
12. ||||| ~D             Assumption (for reductio)
    ---------------
13. ||||| falsum         falsum-intro, 6, 11
14. ||||~~D              ~-intro, 12 - 13
15. |||| D               ~-elim, 14
16. ||||~C               Assumption
    --------------
17. |||||~D              Assumption (for reductio)
    --------------
18. ||||| falsum         falsum-intro, 7, 16
19. ||||~~D              ~-intro, 17-18
20. |||| D               ~-elim, 19
21. |||D                 v-elim, 10, 11-15, 16-20
22. |||A v D             v-intro, 21
23. || A v D             v-elim, 2, 8-9, 10-22
24. |A v D               v-elim, 1, 3-4, 5 - 23

Dies ist ein ähnlicher Beweis wie der von possibleWorld , außer dass er mit der zweiten Prämisse und nicht mit der ersten beginnt und ihn mit einem anderen Beweisprüfer im Fitch-Stil veranschaulicht.

Der Beweis verwendet Disjunktionseinführung (∨I), Konjunktionsbeseitigung (∧E), Widerspruchseinführung (⊥I), Explosion (X) und Konjunktionsbeseitigung (∨E). Einzelheiten zu diesen Regeln finden Sie unter forall x: Calgary Remix .

Die Verwendung von Explosion macht dies möglicherweise zu keiner Antwort, aber das OP sagt, dass "Widerspruch intro, elim" zulässig sind. Aus diesem Grund gehe ich davon aus, dass auch eine Explosion zulässig ist. Wenn nicht, liefert es eine weitere Illustration, wie man mit der Hinzufügung der Explosionsregel verfahren könnte.

Geben Sie hier die Bildbeschreibung ein

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/

„Contradiction Elimination“ ist ein Alias ​​für „Explosion“ – siehe „Regeln für Cambridge“. Außerdem ... Tipp: Sie können sofort zu A v D explodieren, ohne durch A gehen zu müssen.
Gute Beobachtung, dass "Widerspruchsbeseitigung" ein Alias ​​für "Explosion" ist. Sie haben Recht, dass Sie die Zeilen 12 und 17 nicht benötigen. @GrahamKemp
Beweisen Sie A ∨ D aus A ∨ (B ∧ C) und (¬ B ∨ ¬ C) ∨ D ( LPL Q6.26) ohne Verwendung von --> oder materieller Implikation
AntwortenHierDatenschutz-Bestimmungen1y, 0v