verificación de pruebas para la deducción natural

Question

¿Podría alguien decirme si la siguiente deducción natural es correcta para la siguiente fórmula?

(p  q)  r  p  (q r)
1       (p  q)  r    assump 0
2        p  (q r)    
2.1      p              assump 2.1
2.2      q  r         
2.2.1    q             assump 2.2
2.2.2    r             E 1,2.2
2.3      qr          I 2.2
3        p(qr)      I 2, 2.3

Answer 1

La notación me resulta un poco rara. ¿2. anuncia lo que vas a probar?

Y necesitas un paso explícito introduciendo $p \land q$ en el sistema que me enseñaron. El resto parece estar bien.

Así que en mi notación:

1. $(p \land q) \Rightarrow r$ (suposición/axioma)
2. $p$ (supuesto)
3. $q$ (supuesto)
4. $p \land q$ (de 2 y 3)
5. $r$ (del modus ponens, 4 y 1)
6. $q \Rightarrow r$ y el 3 se retira. (Introducción de $\Rightarrow$ )
7. $p \Rightarrow (q \Rightarrow r)$ y se suprime 2 (Introducción de $\Rightarrow$ de nuevo).

Prueba completa, ya que la única suposición no eliminada es el "axioma" a la izquierda de $\vdash$ .

Answer 2

Estoy de acuerdo con Henno Brandema sobre la necesidad de un paso que derive $p ∧ q$ .

Esta respuesta muestra principalmente que existen comprobadores de pruebas que se pueden utilizar para la deducción natural al estilo de Fitch. Así es como se vería la prueba en el comprobador de pruebas asociado con el programa forallx texto. A continuación figuran los enlaces correspondientes.

La razón por la que se necesita la línea 4 es para hacer referencia a ella en la línea 5 para la eliminación condicional (→E). Se necesita una línea para el condicional (línea 1) y el antecedente (línea 4) para derivar el consecuente (línea 5).

El software permite obtener comprobaciones de verificación con la frecuencia que se desee. El coste es utilizar los requisitos de entrada particulares del software, como el uso de mayúsculas para las variables de frase.

---

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

P. D. Magnus, Tim Button con adiciones de J. Robert Loftis remezclado y revisado por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: Una introducción a la lógica formal, otoño de 2019. http://forallx.openlogicproject.org/forallxyyc.pdf