Prueba de deducción natural para los nuevos var

Question

Demostrar por deducción natural,

$$(x \vee y) \vdash ((x \wedge z) \vee (z \implies y))$$

He intentado utilizar $$(z \implies y)$$ como mi suposición, pero eso no funcionó demasiado bien.

¿Dónde puedo ir?

Answer 1

He aquí una forma de demostrarlo usando puramente las reglas de la deducción natural:

\begin{array}{l} & \{1\} & 1. & x \lor y & \text{ $Prem.$ }\\ & \{2\} & 2. & x & \text{ Assum. (1st Disj.) }\\ & \{3\} & 3. & z & \text{ Assum. }\\ & \{2,3\} & 4. & x \land z & \text{ 2,3 $\land$I }\\ & \{2,3\} & 5. & (x \land z) \lor (z \implies y) & \text{ 4 $\lor$I }\\ & \{2\} & 6. & z \implies ((x \land z) \lor (z \implies y)) & \text{ 3,5 CP }\\ & \{7\} & 7. & \neg z & \text{ Assum. }\\ & \{8\} & 8. & \neg y & \text{ Assum. }\\ & \{3,8\} & 9. & \neg y \land z & \text{ 3,8 $\land$I }\\ & \{3,8\} & 10. & z & \text{ 9 $\land$E }\\ & \{3\} & 11. & \neg y \implies z & \text{ 8,10 CP }\\ & \{3,7\} & 12. & \neg \neg y & \text{ 7,11 MT }\\ & \{3,7\} & 13. & y & \text{ 12 DNE }\\ & \{7\} & 14. & z \implies y & \text{ 3,13 CP }\\ & \{7\} & 15. & (x \land z) \lor (z \implies y) & \text{ 14 $\lor$I }\\ & - & 16. & \neg z \implies ((x \land z) \lor (z \implies y)) & \text{ 7,15 CP }\\ & \{17\} & 17. & \neg ((x \land z) \lor (z \implies y)) & \text{ Assum. }\\ & \{17\} & 18. & z & \text{ 16,17 MT, DNE }\\ & \{2,17\} & 19. & \neg z & \text{ 6,17 MT }\\ & \{2,17\} & 20. & z \land \neg z & \text{ 18,19 $\land$I }\\ & \{2\} & 21. & (x \land z) \lor (z \implies y) & \text{ 17,20 RAA (1st Concl.)}\\ & \{22\} & 22. & y & \text{ Assum. (2nd Disj.) }\\ & \{3,22\} & 23. & y \land z & \text{ 3,22 $\land$I }\\ & \{3,22\} & 24. & y & \text{ 23 $\land$E }\\ & \{22\} & 25. & z \implies y & \text{ 3,24 CP }\\ & \{22\} & 26. & (x \land z) \lor (z \implies y) & \text{ 26 $\lor$I (2nd Concl.)}\\ & \{1\} & 27. & (x \land z) \lor (z \implies y)& \text{ 1,2,21,22,26 $\lor$E }\\ \end{array}

Answer 2

En la fórmula que hay que derivar tenemos una disyunción lógica como conectivo lógico principal y sabemos que $p\to q \leftrightarrow \neg p\lor q$ . Tener en cuenta estas dos cosas nos ayuda a elegir la hipótesis adecuada $z\land\neg y$ . $$ \begin{array}{l} & \{1\} & (1) & x\lor y & \text {Premise}\\ & \{2\} & (2) & z \land\neg y & \text {Assumption}\\ & \{2\} & (3) & \neg y & \text {2 Simplification}\\ & \{1,2\} & (4) & x & \text {1,3 Modus tollendo ponens}\\ & \{2\} & (5) & z & \text {2 Simplification}\\ & \{1,2\} & (6) & x\land z & \text {4,5 Adjunction}\\ & \{1\} & (7) & (z\land\neg y)\to(x\land z) & \text {2,6 Conditional Proof}\\ & \{1\} & (8) & \neg(z\land\neg y)\lor(x\land z) & \text {7 Equivalence for Implication and Disjunction}\\ & \{1\} & (9) & (\neg z\lor y)\lor(x\land z) & \text {8 De Morgan's Law}\\ & \{1\} & (10) & (x\land z)\lor(z\to y) & \text {9 Equivalence for Implication and Disjunction and Commutative Law}\\ \end{array}$$

Answer 3

Una pista: Primeras 4 líneas de una prueba utilizando una forma simplificada de deducción natural:

1. $X\lor Y\space$ (Premisa, dos casos a considerar)

2. $Z\lor \neg Z\space$ (Ley del medio excluido, dos subcasos a considerar)

3. $X\space$ (Premisa, caso 1)

4. $Z\space$ (Premisa, subcaso 1)

En todos los casos y subcasos, debería poder obtener $[X\land Y] \lor [Z\implies Y].$

Answer 4

Aquí hay una prueba utilizando la deducción natural con un Comprobador de pruebas estilo Fitch .

La estrategia general fue utilizar la ley del medio excluido (LEM) en $Z \lor \lnot Z$ .

---

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

Answer 5

$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}$ He aquí una prueba por contradicción. $${\fitch{1.~x\vee y\qquad\textsf{Premise}}{\fitch{2.~\neg((x\wedge z)\vee(z\to y))\qquad\textsf{Assumption}}{\fitch{3.~z\qquad\textsf{Assumption}}{\fitch{4.~x\qquad\textsf{Assumption}}{5.~x\wedge z\qquad\textsf{Conjunction Introduction (3,4)}\\6.~(x\wedge z)\vee(z\to y)\qquad\textsf{Disjunction Introduction (5)}\\7.~\bot\qquad\textsf{Negation Elimination (2,6)}\\8.~y\qquad\textsf{Ex Falso Quodlibet (7)}}\\~~9.~x\to y\qquad\textsf{Conditional Introduction (4-8)}\\\fitch{10.~y\qquad\textsf{Assumption}}{}\\11.~y\to y\qquad\textsf{Conditional Introduction (10-10)}\\12.~y\qquad\textsf{Disjunction Elimination (1,9,11)}}\\13.~z\to y\qquad\textsf{Conditional Introduction (3-12)}\\14.~(x\wedge z)\vee(z\to y)\qquad\textsf{Disjunction Introduction (13)}\\15.~\bot\qquad\textsf{Negation Elimination (2,14)}}\\16.~\neg\neg((x\wedge z)\vee(z\to y))\qquad\textsf{Negation Introduction (2-15)}\\17.~(x\wedge z)\vee(z\to y)\qquad\textsf{Double Negation Elimination (16)}}\\\therefore \quad x\vee y\vdash (x\wedge z)\vee(z\to y)}$$