Cómo probar P ∨ Q : ~ (~P & ~Q) con deducción natural

Aquí hay otro problema de Tomassi que no puedo resolver ( Lógica , Ejercicio 3.9.1.17, página 106):

P ∨ Q : ~ (~P & ~Q)

Tengo que usar la deducción natural y las únicas reglas que conozco son:

  • suposiciones,
  • modus ponendo ponens,
  • modus tollendo tollens,
  • doble negación,
  • reducción al absurdo,
  • prueba condicional,
  • v-introducción,
  • v-eliminación,
  • e introducción,
  • y eliminación.

La demostración de Tomassi consta de 11 pasos.

Hasta ahora esta es mi solución:

[1] (1) P ∨ Q Premisa

[2] (2) ~P & ~Q Suposición para RAA

[2] (3) ~P 2 &E

[4] (4) P Suposición y conclusión de la primera disyunción para vE

[5] (5) Q Suposición 2ª disyunción para vE

[2,5] (6) ~P-->Q 2,5 CP

[2] (7) ~P 2 &E

[2,5] (8) ~~P 6,7 MT

[2,5] (9) P 8 DNE

[1,2] (10) P 1,4,4,5,9 vE (descarga 4 y 5)

[1,2] (11) ~P&P 2,10 &I

[1] (12) ~(~P & ~Q) 2,11 RAA (descarga 2)

El de Tomassi no se da.

Hice una edición para formatear las reglas para facilitar la lectura. Supongo que tengo la lista correcta. Puede revertir esto o continuar editando. Me pregunto si tienes introducción de negación o introducción de contradicción.

Respuestas (3)

Esta respuesta proporcionará una prueba basada en la Lógica de Paul Tomassi . El problema es 1.17 en el Ejercicio 3.9 de la página 106.

P v Q : ~(~P & ~Q)

P v Q ⊦ ~(~P & ~Q)
{1} 1. Premisa P v Q
{2} 2. P Supuesto para vEliminación
{3} 3. Suposición de ~P y ~Q para RAA
{3} 4. ~P 3 &E
{2,3} 5. P & ~P 2,4 &I
{2} 6. ~(~P & ~Q) 3,5 RAA
{7} 7. Supuesto Q para VEliminación
{8} 8. ~P & ~Q Suposición para RAA
{8} 9. ~P 8 &E
{7,8} 10. P & ~P 7,9 &I
{7} 11. ~(~P & ~Q) 8,10 RAA
{1} 12. ~(~P & ~Q) 1,2,6,7,11 vE

La descripción de reductio ad absurdum (RAA) está en las páginas 101-5.

La descripción de vEliminación (vE) se encuentra en las páginas 86-9.

La descripción de &Eliminación (&E) e &Introducción (&I) se encuentra en las páginas 50-2.

Esta prueba usó 12 en lugar de 11 líneas.

Referencia

Tomassi, P. (1999). Logic (Londres y Nueva York.

Aquí está su prueba ligeramente modificada ...

[1] P ∨ Q --- Premisa

[2] ~P & ~Q --- Suposición para RAA

[3] ~P --- de 2 por &E

[4] ~Q --- de 2 por &E

[5] P --- Supuesto de [1] para vE (1º)

[6] ~P & P --- de [3] y [5] por &I

[7] ~(~P & ~Q) --- de [2] y contradicción [6] por RAA

[8] Q --- Suposición de [1] para vE (2º)

[9] ~Q & Q --- de [4] y [8] por &I

[10] ~(~P & ~Q) --- de [2] y contradicción [9] por RAA, suposición de descarga [2]

[11] ~(~P & ~Q) --- de [5]-[7] y [8]-[10] y [1] por vE, descargando los supuestos [5] y [8]

Aquí hay una forma de probar esto basada en el verificador de pruebas de Klement:

ingrese la descripción de la imagen aquí

En la línea 2 asumo la negación de lo que quiero mostrar. Este es un argumento de reducción al absurdo diseñado para permitirme introducir una negación en 10. Aunque no veo la regla de introducción de negación en su lista, esto puede darle una idea de cómo proceder.

En las líneas 3 y 4 utilicé la eliminación de conjunciones y en las líneas 5 a 8 establecí una eliminación de disyunción que completó en línea 9. Implicó introducir una contradicción en las líneas 6 y 8. No vi la introducción de contradicción en su lista de reglas, pero la reductio ad absurdum me sugirió que podría ser aceptable.

Aquí hay una prueba que usa el silogismo de disyunción (DS), una regla derivada para acortar la eliminación de la disyunción. Esto no está en tu lista. Lo proporciono solo para dar otra perspectiva sobre cómo esto podría probarse.

ingrese la descripción de la imagen aquí

Finalmente, aquí hay una prueba más corta (al menos en el verificador de pruebas que estoy usando) que usa la regla de De Morgan (DeM). Eso no está en la lista de reglas permitidas, pero lo ofrezco como otra perspectiva del problema cuando esa regla derivada esté disponible.

ingrese la descripción de la imagen aquí

El OP proporcionó un intento de prueba. Esto parece funcionar. Usando las reglas para el verificador de pruebas que estoy usando, obtengo lo siguiente:

ingrese la descripción de la imagen aquí

Hay dos diferencias. Para la línea 6 en la prueba del OP necesitaba tres líneas, mi 6, 7 y 8. Para que la línea 11 alcanzara la contracción, necesitaba usar una introducción de contradicción (⊥I) en mi línea 13. De lo contrario, las pruebas son similares.

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/

Según DeMorgan, esto es obvio ya que el algoritmo general es solo para eliminar la negación del exterior, negar cualquier elemento en el siguiente paso de la jerarquía y cambiar las conjunciones y disyunciones.
@ rus9384 Sí, es obvio. Esperaría hacerlo en dos líneas, premisa y conclusión, pero este verificador de pruebas, asumiendo que lo usé de manera eficiente, me hizo usar 5 líneas.
@FrankHubeny Muchas gracias por su pronta respuesta. Sin embargo, todavía no conozco la introducción de la contradicción. Entonces, ¿te importaría mostrarme cómo resolverlo sin ese, por favor?
@DiegoRuizHaro Tienes reductio ad absurdum (RAA) que es similar. No tengo esa regla en el verificador de prueba que estoy usando, pero me imagino que funciona de la misma manera, excepto que en lugar de introducir la contradicción y luego descartar la suposición con una prueba indirecta, es posible que tengas que llegar a algo como P & ~ P y luego cumplir con la suposición con una regla RAA de algún tipo.
@FrankHubeny Gracias de nuevo por la ayuda. Todavía estoy atascado en la eliminación de la disyunción. ¿Cuál es la conclusión que debo derivar de ambas disyuntivas para validar la eliminación de la disyunción?
@DiegoRuizHaro Como no tiene una introducción de contradicción, es posible que la eliminación de la disyunción tenga que ser diferente para usted. Si tiene silogismo disyuntivo o reglas de DeMorgan, las otras dos pruebas pueden ser posibles usando RAA.
@FrankHubeny Todavía no sé cómo proceder desde la línea 6. ¿Debería usar la eliminación de la disyunción para probar P de ambas disyunciones? ¿Cómo podría probar P a partir de Q?
@DiegoRuizHaro Usando la segunda prueba, reemplace la introducción de contradicción con la introducción de conjunción de Q & ~Q de las líneas 4 y 5. Esto debería permitirle usar RAA en la línea 7.
@FrankHubeny Hasta ahora, creo que he podido resolverlo en 12 pasos, mientras que la prueba de Tomassi consta de 11. Esto es lo que he hecho hasta ahora:
@DiegoRuizHaro Puede editar su pregunta y publicar su solución allí. Agregue las reglas que está usando y observe dónde difieren de la solución de Tomassi.
@FrankHubeny [1] (1) P ∨ Q Premisa [2] (2) ~P & ~Q Supuesto para RAA [2] (3) ~P 2 &E [4] (4) P Supuesto y conclusión de la primera disyunción para vE [5] (5) Q Suposición 2da disyunción para vE [2,5] (6) ~P-->Q 2,5 CP [2] (7) ~Q 2 &E [2,5] (8) ~ ~P 6,7 MT [2,5] (9) P 8 DNE [1,2] (10) P 1,4,4,5,9 vE (descarga 4 y 5) [1,2] (11) ~P&p 2,10 &I [1] (12) ~(~P & ~Q) 2,11 RAA (descarga 2)
@DiegoRuizHaro Creo que tu prueba funciona. Pude seguirlo en el comprobador de pruebas que estoy usando. Hubo dos lugares donde necesitaba usar enfoques ligeramente diferentes, pero su enfoque parece correcto. Puede ver los resultados del verificador de pruebas después de su prueba en mi respuesta.
Cómo probar P ∨ Q : ~ (~P & ~Q) con deducción natural
RespuestasAquíPolítica de privacidad1y, 0v