Demostrar A ∨ D a partir de A ∨ (B ∧ C) y (¬ B ∨ ¬ C) ∨ D ( LPL Q6.26) sin usar --> o implicación material

|  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

Ahora, con un tercer ∨-elim derivamos ⊥ (la contradicción) tanto de 8), 9) como de 8), 10); de este modo :

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

Habiendo derivado A ∨ D tanto de 6) D como de 8) (¬ B ∨ ¬ C), tenemos:

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

Habiendo derivado A ∨ D de 3) A y 5) (B ∧ C), tenemos:

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

Conclusión :

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

La prueba va a ser un gran v-elim en A v (B ^ C). Sin embargo, podría haber hecho fácilmente el v-elim en (~B v ~C) v D. He tratado de hacer que la notación coincida con lo que está en el libro de texto, aunque admito que es bastante atroz. Podría valer la pena copiarlo a mano para que pueda ver cómo funciona el alcance para las subpruebas.

 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

Esta es una prueba similar a la proporcionada por possibleWorld, excepto que comienza con la segunda premisa en lugar de la primera y la ilustra con un verificador de prueba diferente al estilo de Fitch.

La prueba utiliza la introducción de disyunción (∨I), la eliminación de conjunción (∧E), la introducción de contradicción (⊥I), la explosión (X) y la eliminación de conjunción (∨E). Para obtener detalles sobre estas reglas, consulte forall x: Calgary Remix .

El uso de explosión puede hacer que esto no sea una respuesta, pero el OP dice que se permite "Contradiction intro, elim". Por eso, asumo que la explosión también está permitida. Si no, proporciona otra ilustración de cómo se podría proceder con la adición de la regla de explosión.

Referencias

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

PD Magnus, Tim Button con adiciones de J. Robert Loftis remezcladas y revisadas por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, invierno de 2018. http://forallx.openlogicproject.org/