Solución:
Quien sea que puso el ejercicio no fue muy amable; pero abordar esto es, de hecho, una comprobación de la realidad bastante útil para que piense en la estrategia de prueba.
Tiene una premisa disyuntiva, de la forma $ A lor B $, y la conclusión objetivo $ C $. Es una libra a un centavo que tendrá que usar la eliminación de disyunción. Así que la forma del argumento seguramente será
$ quad A lor B \ quad quad mid quad A \ quad quad mid quad vdots \ quad quad mid quad C \ quad quad – quad quad mid quad B \ quad quad mid quad vdots \ quad quad mid quad C \ quad C $
De modo que eso reduce el problema a encontrar dos pruebas, desde $ A $ a $ C $ y $ B $ a $ C $. Veremos el primero, el otro es similar.
Entonces ahora quieres completar los puntos
$ quad s to p \ quad vdots \ quad (s to q) lor (t to p) $
Desagradable de hacer desde los primeros principios. Pero tal vez parezca un poco más manejable si divides las cosas en dos etapas como esta.
$ quad s ap \ quad vdots \ quad neg s lor p \ quad vdots \ quad (s to q) lor (t to p) $
(No saqué eso de un sombrero: ¡piensa por qué ese es el camino obvio a tomar!) Y vas a necesitar otra eliminación de disyunción para la segunda parte que obviamente debería ir
$ quad s ap \ quad vdots \ quad neg s lor p \ quad quad mid neg s \ quad quad mid vdots \ quad quad mid (s to q) \ quad quad mid (s to q) lor (t to p) \ quad quad – \ quad quad mid p \ quad quad mid vdots \ quad quad mid (t to p) \ quad quad mid (s to q) lor (t to p) \ quad (s a q) lor (t a p) $
Así que al menos hemos reducido el problema al de llenar los tres vacíos. Pero cada uno de ellos debería ser una tarea familiar estándar que ya puede hacer en una prueba de Fitch. Así que te dejaré esos detalles adicionales completando la prueba $ A $ -to- $ C $; ¡y la prueba $ B $ -to- $ C $ funciona de manera similar!
Un intento de resolver este problema es asumir la negación de la meta, $ (s → q) ∨ (t → p) $y luego intentar derivar una contradicción. La negación con la regla de De Morgan convertiría la disyunción en una conjunción que debería simplificar las cosas, pero también antepone una negación a dos condicionales. El verificador de pruebas estilo Fitch que utilizo no tiene una regla que me permita derivar $ ¬s ∨ p $ de $ s → p $ así que tendré que encontrar una forma de evitarlo.
Una cosa que podría hacer es, en lugar de negar la meta directamente, negar algo equivalente a la meta. Por ejemplo, podría negar esto: $ (¬s ∨ q) ∨ (¬t ∨ p) $. Podría ser más fácil trabajar con esa forma de meta porque convierte los condicionales en disyunciones. Es cierto que si llego a una contradicción, todavía tendré trabajo por hacer: tendré que derivar el objetivo original de esa declaración que sé que es equivalente a ella. Ojalá sea más fácil hacerlo.
Aquí hay una prueba usando el corrector de pruebas asociado con el forallx texto. Tuve que poner en mayúscula las variables de la oración para ingresar el argumento en este corrector de pruebas:
Observe cómo en la línea 2 estoy negando una declaración diferente, pero equivalente, al objetivo real que quiero lograr. Esto me permite derivar una contradicción en la línea 20. Con esa contradicción, ahora puedo usar la declaración innecesaria en la línea 21 y derivar el objetivo real en la línea 38.
Esta puede ser una forma alternativa de abordar los objetivos con condicionales en las pruebas de verificación al estilo de Fitch si los métodos más directos no funcionan.
Para ver el corrector de pruebas y una descripción de las reglas de inferencia, consulte los enlaces a continuación.
Editor y verificador de pruebas de deducción natural estilo JavaScript / PHP Fitch de Kevin Klement http://proofs.openlogicproject.org/
PD Magnus, Tim Button con adiciones de J. Robert Loftis remezclado y revisado por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, otoño de 2019. http://forallx.openlogicproject.org/forallxyyc.pdf