Cómo mostrar que (P & Q) v (~P v ~ Q) es un teorema en SD

Estoy trabajando en una pregunta de práctica en mi libro de texto de lógica. Y estoy atascado en esta pregunta.

Esto es lo que tengo hasta ahora:

1. ~(P & Q)   Assumption/ Negated Eelimination 
2.     P          Assumption/Negated Introduction 
3.       Q          Assumption/Negated Introduction 
4.       P&Q        2,3 conjunction Introduction
5.     ~(P&Q)       1 Reteration 
6.    ~Q            2-5 Negated Introduction 

Ahora, siempre que pueda derivar una Q, entonces podré Derivar (P&Q) Me pregunto si alguien puede darme una idea.

Gracias de antemano

¿No es esto solo lógica, no filosofía de la lógica o lógica con alguna dimensión filosófica?
¿No puedes usar a De Morgan? Simplemente abra los soportes de la parte NAND.
¿Entonces esto es filosofía de la lógica o lógica con una dimensión filosófica? Interesante.
¿Cuál es la pregunta en la que está atascado y cuál es el nombre del libro de lógica que está usando? ¿Utiliza algún software para la verificación de pruebas?
Como puede ver en las respuestas a continuación, los detalles dependen de los sistemas de prueba que puede usar: si, por ejemplo, SD es Deducción natural, no tiene una "regla primitiva" para De Morgan. Tienes que usar en su lugar Doble Negación. Por lo tanto, especifique qué significa sistema SD.

Respuestas (6)

No podrás probar ninguna disyunción, ya que ninguna es una verdad lógica. En cambio, asume la negación de lo que quieres probar y luego deriva una contradicción. Estoy seguro de que otros pueden formatear esto mucho mejor que yo, pero aquí hay una prueba. Utilizo 'F' para indicar falso/contradicción y confío en una equivalencia de DeMorgan, pero esto, por supuesto, debe eliminarse.

|1. ~((P&Q)∨(~P∨~Q))........ Suponga
||2. P&Q..................................Asumir
||3. (P&Q)∨(~P∨~Q)..........2, ∨Intro
||4. F .................................... 1,3
|5. ~(P&Q).......................... 2-4, ~Introducción
|6. ~P ∨ ~Q........................ 5,DeMorgan
|7. (P&Q)∨(~P∨~Q).......... 6, ∨Intro
|8. F.................................. 1,7
9. (P&Q)∨(~P∨ ~Q).......... 1-8, ~Elim

otro enfoque que da el número mínimo de pasos (aunque no es una prueba formal):

1. (P & Q) v ~(P & Q)              law of excluded middle
2. (P & Q) v (~P v ~Q)             DeM 1

Usando la deducción natural y el comprobador de pruebas asociado con forall x: Calgary Remix , obtengo la siguiente prueba:

ingrese la descripción de la imagen aquí

En la línea 1 comienza una subdemostración asumiendo la negación de lo que quieres probar.

En la línea 2 aplique la regla de DeMorgan a la línea 1.

En la línea 3 elimine la primera parte de la conjunción en la línea 2.

En la línea 4 aplique la regla de DeMorgan a la línea 3.

En la línea 5 elimine la segunda parte de la conjunción en la línea 2.

En la línea 6 introduce una contradicción basada en las líneas 4 y 5.

En la línea 7, descarte la suposición de la línea 1 y salga de la subdemostración usando la prueba indirecta (IP) para llegar a la conclusión deseada.

Me gustaría ofrecer la siguiente "prueba".

1 - Si (A) V ~(A) es un teorema SD,
2 - A = (P & Q) : definición
3 - (P & Q) V (~PV ~Q) : dado
4 - (P & Q) V ~(P & Q) : DeMorgan (en la 2da parte)
5 - (A) V ~(A) : sustitución
6 - Por lo tanto (P & Q) V (~PV ~Q), es un teorema SD.

Estrategia: Demostrar que asumir que el objetivo es falso conduce a una contradicción sin importar lo que supongamos sobre los literales.

La prueba de estilo Fitch es la siguiente: asumir algunas cosas y, luego, negar todo. Básicamente.

   ._.
 1.|  |_ ~((p & q) v (~p v ~q))      : Assumption
 2.|  |  |_ p                        : Assumption
 3.|  |  |  |_ q                     : Assumption

 6.|  |  |  | #                      : Negation Elimination (1,5)
 7.|  |  | ~q                        : Negation Introduction (3-6)

10.|  |  | #                         : Negation Elimination (1,9)
11.|  | ~p                           : Negation Introduction(2-10)

14.|  | #                            : Negation Elimination (1,13)
15.| ~~((p & q) v (~p v ~q))         : Negation Introduction (1-14)
16.| ((p & q) v (~p v ~q))           : Double Negation Elimination (15)

Opps. Me perdí algunos pasos. :)

NB: El DNE al final sugiere que este no es un teorema constructivamente válido. De hecho, no lo es. Aún así ((p & q) v (~pv ~q)) es un teorema de la lógica clásica, como se muestra al usar solo las reglas básicas de inferencia para la deducción natural.

PD: usando # como la constante falsa

Ninguna respuesta hasta ahora ha sido puramente en SD.

  1. |~((P&Q)∨(~P∨~Q)) A/~E
  2. | ~PA/~E
  3. | (~Pv~Q) 2 vI
  4. | (~Pv~Q)v(P&Q) 3 vI
  5. | ~((P&Q)∨(~P∨~Q)) 1 R
  6. |P 2-5 ~S
  7. | ~QA/~E
  8. | (~Pv~Q) 7 vI
  9. | (~Pv~Q)v(P&Q) 8 vI
  10. | ~((P&Q)∨(~P∨~Q)) 1 R
  11. |P 7-10 ~S
  12. |(P y Q)
  13. |(P&Q)v(~P∨~Q) 12 vI
  14. |~((P&Q)∨(~P∨~Q)) 1 R
  15. (P&Q)∨(~P∨~Q) 1-14 ~E