Esta es una pregunta repetida: Lenguaje Lógica y Prueba P. 6.26
Usando las reglas de deducción natural, dé una prueba formal de
A ∨ D
de las instalaciones
- A ∨ (B ∧ C)
- (¬ segundo ∨ ¬ do) ∨ re
El libro de texto de LPL aún no ha introducido implicaciones materiales o implica el símbolo "-->" y la respuesta dada en el enlace anterior NO satisface la pregunta en el libro y me sorprendió que el usuario aceptara la respuesta como apropiada.
La respuesta es válida hasta el paso 22, ya que el libro de texto no ha introducido esas formas de pasos. ¿Hay alguna manera de usar esta prueba y usar otras reglas para mostrar la implicación de que ~A --> D y A --> ~D por lo tanto AVD ?
¿Cómo haría para resolver esta prueba en Fitch sin -> o implicación material?
Reglas que puedes usar:
V intro, elim (disyunción)
^ introducción, elim (conjunción)
~ intro, elim (negación)
Introducción a la contradicción, elim
= introducción, eliminación
| 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/
billy bob
billy bob
Mauro ALLEGRANZA