Ayuda de lógica formal de Fitch 6.26

6.26

1.A v (B ^C)

2.~B v ~C v D

3.-A

4.-AVD (V intro 3)

-5. B^C

--6. ~B

--7. B (conjunción elim. 5)

--8. contradicción (contradicción introductoria 6 y 7)

--9. AVD (introducción de contradicción)

--10. ~C

--11. C (conjunción elim. 5)

--12. contradicción (c intro 11 y 12)

--13. AVD (eliminación de contradicciones)

¡Tú haces el resto! Si puede obtener AVD en el segundo nivel de la subdemostración, puede llevarlo al primero mediante la disyunción elim. Una vez que hagas eso, ¡el resto debería ser fácil!

El OP quisiera una prueba formal de lo siguiente:

Premisa: A ∨ (B ∧ C)

Premisa: ¬B ∨ ¬C ∨ D

Meta: A ∨ D

Lo primero a tener en cuenta es que aunque parece que la segunda premisa es una simbolización de algo, no es una oración válida. Es solo una expresión. El alcance de los conectores, "∨", es ambiguo. Para hacer de esta una oración que podamos usar formalmente, debe reescribirse como

(¬B ∨ ¬C) ∨ D

o como

¬B ∨ (¬C ∨ D)

Para ver esto, intente poner la expresión ¬B ∨ ¬C ∨ D en un comprobador de pruebas. ¿Se puede incluso empezar? Esto es lo que sucedió cuando intenté usar la deducción natural y el verificador de prueba utilizado por forall x: Calgary Remix :

Basados ​​en nuestra comprensión humana del conectivo "∨" como "o" podríamos proceder informalmente a usar la expresión tal como es y pensar que estamos haciendo casos. Primero consideraríamos el caso "¬B", luego el caso "¬C" y luego el caso D y veríamos si podemos llegar a la meta "A ∨ D" en cada caso.

Sin embargo, dado que queremos una prueba formal , no podemos proceder de esa manera. Necesitamos usar oraciones, no expresiones arbitrarias, sin importar cuán obvias sean para nosotros, y necesitamos usar reglas formales para disyunciones (es decir, "∨") para justificar cada línea de la prueba formal. Un verificador de pruebas nos ayuda a verificar que estamos usando oraciones y siguiendo las reglas.

Si elegimos ~B v (~C v D) como oración, podemos obtener una prueba como la siguiente.

Esta prueba muestra una forma de manejar los casos en ambas premisas eliminando formalmente el conectivo "V" a través de subpruebas.

Considere los dos casos en la primera premisa. Asumo, es decir, comienzo una subdemostración con "A" como suposición en la línea 3 y alcanzo la meta deseada en la línea 4 y asumo "(B ∧ C)" en la línea 5 y alcanzo la meta deseada en la línea 18. Con ambos lados del conector "V" alcanzando la meta, puedo eliminar la "V" y completar la demostración. Esta eliminación descarga las dos suposiciones que hice representadas por las dos subpruebas, una para cada caso.

El segundo caso anterior requería más líneas. Consideremos esos detalles. Para alcanzar el objetivo del segundo caso, "(B ∧ C)", necesitaba usar la segunda premisa. Asumí el caso "¬B" al crear una subdemostración con "¬B" como suposición en la línea 7 y alcancé la meta en la línea 9 y asumí el caso "¬C ∨ D" en la línea 10 y llegué a la conclusión en la línea 17. Tenga en cuenta que "¬C ∨ D" también es una disyunción, una oración "∨", por lo que también necesito usar casos, es decir, subpruebas. Hice esto en las líneas 10 a 17.

Uno de los requisitos en el OP era:

Demuéstrelo formalmente sin usar la Ley de DeMorgan

Tenga en cuenta que no utilicé la Ley de DeMorgan en la prueba anterior. Para ver cómo se podría haber usado la Ley de DeMorgan, considere la siguiente prueba usando "(¬B ∨ ¬C) ∨ D".

Lo hice, pero la prueba es monstruosamente larga. Si alguien sabe como simplificarlo se lo agradecería. Hecho con el editor de prueba de Fitch de Stanford :

Lo hice, pero la prueba es monstruosamente larga. Si alguien sabe como simplificarlo se lo agradecería. Hecho con el editor de prueba de Fitch de Stanford:

La implementación de Fitch de Stanford notoriamente infla las pruebas, pero habías vagado bastante en círculos, ahí @Houshalter

 1.|  A v (B & C)             Premise
 2.|_ (~B v ~C) v D           Premise
 3.|  |_ A                    Assumption
 4.|  |  A v D                Or Introduction 3
 5.|  A => A v D              Implication introduction 3,4
 6.|  |_ B & C                Assumption
 7.|  |  B                    And Elimination 6
 8.|  |  C                    And Elimination 6
 9.|  |  |_ ~(A v D)          Assumption
10.|  |  |  B                 Reiteration 7
11.|  |  ~(A v D) => B        Implication Introduction 9,10
12.|  |  |_ ~(A v D)          Assumption
13.|  |  |  C                 Reiteration 8
14.|  |  ~(A v D) => C        Implication Introduction 12,13
15.|  |  |_ ~B v ~C           Assumption
16.|  |  |  |_ ~B             Assumption
17.|  |  |  |  |_ ~(A v D)    Assumption
18.|  |  |  |  |  ~B          Reiteration 16
19.|  |  |  |  ~(A v D) => ~B Implication Introduction 17,18
20.|  |  |  |  ~~(A v D)      Negation Introduction 11,19
21.|  |  |  ~B => ~~(A v D)   Implication Introduction 16,20
22.|  |  |  |_ ~C             Assumption
23.|  |  |  |  |_ ~(A v D)    Assumption
24.|  |  |  |  |  ~C          Reiteration 22
25.|  |  |  |  ~(A v D) => ~C Implication Introduction 23,24
26.|  |  |  |  ~~(A v D)      Negation Introduction 17,28
27.|  |  |  ~C => ~~(A v D)   Implication Introduction 22,29
28.|  |  |  ~~(A v D)         Or Elimination 15,21,27
29.|  |  |  A v D             Negation Elimination 28
30.|  |  ~B v ~C => A v D     Implication Introduction 15,29
31.|  |  |_ D                 Assumption
32.|  |  |  A v D             Or Introduction 31
33.|  |  D => A v D           Implication Introduction 31,32
34.|  |  A v D                Or Elimination 2,30,33
35.|  B & C => A v D          Implication Introduction 6,34
36.|  A v D                   Or Elimination 1,5,36