https://www.glc.us.es/~jalonso/LMF2019/index.php?action=history&feed=atom&title=Sol_7 Sol 7 - Historial de revisiones 2026-07-20T11:16:35Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/LMF2019/index.php?title=Sol_7&diff=577&oldid=prev Jalonso en 12:03 20 abr 2019 2019-04-20T12:03:22Z <p></p> <a href="https://www.glc.us.es/~jalonso/LMF2019/index.php?title=Sol_7&amp;diff=577&amp;oldid=566">Mostrar los cambios</a> Jalonso https://www.glc.us.es/~jalonso/LMF2019/index.php?title=Sol_7&diff=566&oldid=prev Mjoseh en 10:53 9 abr 2019 2019-04-09T10:53:11Z <p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <tr class="diff-title" lang="es"> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">Revisión del 10:53 9 abr 2019</td> </tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div> </td></tr></table> Mjoseh https://www.glc.us.es/~jalonso/LMF2019/index.php?title=Sol_7&diff=563&oldid=prev Mjoseh en 10:52 9 abr 2019 2019-04-09T10:52:00Z <p></p> <p><b>Página nueva</b></p><div>&lt;source lang = &quot;isabelle&quot;&gt;<br /> theory R7_sol<br /> imports Main <br /> begin<br /> <br /> text {*<br /> --------------------------------------------------------------------- <br /> El objetivo de esta relación es escribir demostraciones usando sólo<br /> las reglas básicas de deducción natural de la lógica proposicional y<br /> los métodos rule, erule, frule, drule y assumption.<br /> <br /> Las reglas básicas de la deducción natural son las siguientes:<br /> · conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br /> · conjunct1: P ∧ Q ⟹ P<br /> · conjunct2: P ∧ Q ⟹ Q<br /> · conjE: ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R<br /> · notE: ⟦¬P; P⟧ ⟹ R<br /> · notI: (P ⟹ False) ⟹ ¬P<br /> · mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br /> · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br /> · impI: (P ⟹ Q) ⟹ P ⟶ Q<br /> · impE: ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R<br /> · disjI1: P ⟹ P ∨ Q<br /> · disjI2: Q ⟹ P ∨ Q<br /> · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br /> · FalseE: False ⟹ P<br /> · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br /> · iffD1: ⟦Q = P; Q⟧ ⟹ P <br /> · iffD2: ⟦P = Q; Q⟧ ⟹ P<br /> · iffE: ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R<br /> · notnotD: ¬¬ P ⟹ P<br /> · not_not: P = ¬¬P<br /> · ccontr: (¬P ⟹ False) ⟹ P<br /> · excluded_midle: ¬P ∨ P<br /> · classical: (¬ P ⟹ P) ⟹ P<br /> · contrapos_nn ⟦¬Q; P ⟹ Q⟧ ⟹ ¬P<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> section {* Implicaciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 1. Demostrar<br /> p ⟶ q, p ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej1: &quot;⟦p ⟶ q; p⟧ ⟹ q&quot; <br /> apply (erule mp)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 2. Demostrar<br /> p ⟶ q, q ⟶ r, p ⊢ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej2: &quot;⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r&quot;<br /> apply (erule mp)+<br /> apply assumption<br /> done <br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 3. Demostrar<br /> p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej3a: &quot;⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r&quot;<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule impE)<br /> apply assumption+<br /> done<br /> <br /> lemma ej3b: &quot;⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r&quot;<br /> apply (erule impE, assumption+)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 4. Demostrar<br /> p ⟶ q, q ⟶ r ⊢ p ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> -- &quot;La demostración detallada es&quot;<br /> lemma ej4: &quot;⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r&quot;<br /> apply (rule impI)<br /> apply (erule mp)<br /> apply (erule mp)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 5. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej5: &quot;p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)&quot;<br /> apply (rule impI)<br /> apply (rule impI)<br /> apply (erule impE, assumption)<br /> apply (erule impE, assumption+)<br /> done <br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 6. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej6: &quot;p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)&quot;<br /> apply (rule impI)<br /> apply (rule impI)<br /> apply (erule impE, assumption)<br /> apply (erule impE, assumption)<br /> apply (erule impE, assumption+)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 7. Demostrar<br /> p ⊢ q ⟶ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej7: &quot;p ⟹ q ⟶ p&quot;<br /> apply (rule impI)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 8. Demostrar<br /> ⊢ p ⟶ (q ⟶ p)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej8: &quot;p ⟶ (q ⟶ p)&quot;<br /> apply (rule impI)<br /> apply (rule impI)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 9. Demostrar<br /> p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej9: &quot;p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)&quot;<br /> apply (rule impI)<br /> apply (rule impI)<br /> apply (erule impE, assumption)<br /> apply (erule impE, assumption+)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 10. Demostrar<br /> p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej10: &quot;p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))&quot;<br /> apply (rule impI)+<br /> apply (erule impE, assumption+)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 11. Demostrar<br /> ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej11: &quot;(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))&quot;<br /> apply (rule impI)+<br /> apply (erule impE, assumption+)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 12. Demostrar<br /> (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej12: &quot;(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)&quot;<br /> apply (rule impI)+<br /> apply (rule_tac P=&quot;p ⟶ q&quot; in mp)<br /> apply assumption<br /> apply (rule impI)<br /> apply assumption<br /> done<br /> <br /> section {* Conjunciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 13. Demostrar<br /> p, q ⊢ p ∧ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej13: &quot;⟦p; q⟧ ⟹ p ∧ q&quot;<br /> apply (rule conjI)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 14. Demostrar<br /> p ∧ q ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej14: &quot;p ∧ q ⟹ p&quot;<br /> apply (erule conjunct1)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 15. Demostrar<br /> p ∧ q ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej15: &quot;p ∧ q ⟹ q&quot;<br /> apply (erule conjunct2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 16. Demostrar<br /> p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej16: &quot;p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r&quot;<br /> apply (rule conjI)<br /> apply (rule conjI)<br /> apply (erule conjunct1)<br /> apply (drule conjunct2)<br /> apply (erule conjunct1)<br /> apply (drule conjunct2)<br /> apply (erule conjunct2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 17. Demostrar<br /> (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej17: &quot;(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)&quot;<br /> apply (rule conjI)<br /> apply (drule conjunct1)<br /> apply (erule conjunct1)<br /> apply (rule conjI)<br /> apply (drule conjunct1)<br /> apply (erule conjunct2)<br /> apply (erule conjunct2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 18. Demostrar<br /> p ∧ q ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej18: &quot;p ∧ q ⟹ p ⟶ q&quot;<br /> apply (rule impI)<br /> apply (erule conjunct2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 19. Demostrar<br /> (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej19: &quot;(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r&quot;<br /> apply (rule impI)<br /> apply (rule conjI)<br /> apply (drule conjunct1)<br /> apply (erule impE)<br /> apply assumption<br /> apply assumption<br /> apply (drule conjunct2)<br /> apply (erule impE)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 20. Demostrar<br /> p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej20: &quot;p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)&quot;<br /> apply (rule conjI)<br /> apply (rule impI)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule conjunct1)<br /> apply (rule impI)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule conjunct2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 21. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej21_1: &quot;p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r&quot;<br /> apply (rule impI)<br /> apply (erule conjE)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule impE)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 22. Demostrar<br /> p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej22: &quot;p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)&quot;<br /> apply (rule impI)<br /> apply (rule impI)<br /> apply (erule impE)<br /> apply (rule conjI)<br /> apply assumption+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 23. Demostrar<br /> (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej23: &quot;(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r&quot;<br /> apply (rule impI)<br /> apply (erule impE)<br /> apply (rule impI)<br /> apply (erule conjunct2)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 24. Demostrar<br /> p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej24: &quot;p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r&quot;<br /> apply (rule impI)<br /> apply (erule conjE)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule impE)<br /> apply assumption+<br /> done<br /> <br /> section {* Disyunciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 25. Demostrar<br /> p ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej25: &quot;p ⟹ p ∨ q&quot;<br /> apply (erule disjI1)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 26. Demostrar<br /> q ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej26: &quot;q ⟹ p ∨ q&quot;<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 27. Demostrar<br /> p ∨ q ⊢ q ∨ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej27: &quot;p ∨ q ⟹ q ∨ p&quot;<br /> apply (erule disjE)<br /> apply (erule disjI2)<br /> apply (erule disjI1)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 28. Demostrar<br /> q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej28: &quot;q ⟶ r ⟹ p ∨ q ⟶ p ∨ r&quot;<br /> apply (rule impI)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 29. Demostrar<br /> p ∨ p ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej29: &quot;p ∨ p ⟹ p&quot;<br /> apply (erule disjE)<br /> apply assumption+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 30. Demostrar<br /> p ⊢ p ∨ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej30: &quot;p ⟹ p ∨ p&quot;<br /> apply (erule disjI1)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 31. Demostrar<br /> p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej31: &quot;p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r&quot;<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (erule disjI1)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (erule disjI2)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 32. Demostrar<br /> (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej32: &quot;(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)&quot;<br /> apply (erule disjE)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (rule disjI2)<br /> apply (erule disjI1)<br /> apply (rule disjI2)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 33. Demostrar<br /> p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej33: &quot;p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)&quot;<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (rule conjI)<br /> apply assumption<br /> apply assumption<br /> apply (rule disjI2)<br /> apply (rule conjI)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 34. Demostrar<br /> (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej34: &quot;(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)&quot;<br /> apply (rule conjI)<br /> apply (erule disjE)<br /> apply (erule conjunct1)<br /> apply (erule conjunct1)<br /> apply (erule disjE)<br /> apply (erule conjE)<br /> apply (rule disjI1)<br /> apply assumption<br /> apply (erule conjE)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 35. Demostrar<br /> p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej35: &quot;p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)&quot;<br /> apply (erule disjE)<br /> apply (rule conjI)<br /> apply (erule disjI1)<br /> apply (erule disjI1)<br /> apply (erule conjE)<br /> apply (rule conjI)<br /> apply (erule disjI2)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 36. Demostrar<br /> (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej36: &quot;(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)&quot;<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (rule disjI2)<br /> apply (rule conjI)<br /> apply assumption+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 37. Demostrar<br /> (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej37: &quot;(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r&quot;<br /> apply (rule impI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule impE, assumption+)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 38. Demostrar<br /> p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej38: &quot;p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)&quot;<br /> apply (rule conjI)<br /> apply (rule impI)<br /> apply (erule impE)<br /> apply (erule disjI1)<br /> apply assumption<br /> apply (rule impI)<br /> apply (erule impE)<br /> apply (erule disjI2)<br /> apply assumption<br /> done<br /> <br /> section {* Negación *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 39. Demostrar<br /> p ⊢ ¬¬p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej39: &quot;p ⟹ ¬¬p&quot;<br /> apply (rule notI)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 40. Demostrar<br /> ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej40: &quot;¬p ⟹ p ⟶ q&quot;<br /> apply (rule impI)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 41. Demostrar<br /> p ⟶ q ⊢ ¬q ⟶ ¬p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej41: &quot;p ⟶ q ⟹ ¬q ⟶ ¬p&quot;<br /> apply (rule impI)<br /> apply (rule notI)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 42. Demostrar<br /> p ∨ q, ¬q ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej42: &quot;⟦p ∨ q; ¬q⟧ ⟹ p&quot;<br /> apply (erule disjE)<br /> apply assumption<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 43. Demostrar<br /> p ∨ q, ¬p ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej43: &quot;⟦p ∨ q; ¬p⟧ ⟹ q&quot;<br /> apply (erule disjE)<br /> apply (erule notE)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 44. Demostrar<br /> p ∨ q ⊢ ¬(¬p ∧ ¬q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej44: &quot;p ∨ q ⟹ ¬(¬p ∧ ¬q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 45. Demostrar<br /> p ∧ q ⊢ ¬(¬p ∨ ¬q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej45: &quot;p ∧ q ⟹ ¬(¬p ∨ ¬q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 46. Demostrar<br /> ¬(p ∨ q) ⊢ ¬p ∧ ¬q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej46: &quot;¬(p ∨ q) ⟹ ¬p ∧ ¬q&quot;<br /> apply (rule conjI)<br /> apply (rule notI)<br /> apply (erule notE)<br /> apply (erule disjI1)<br /> apply (rule notI)<br /> apply (erule notE)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 47. Demostrar<br /> ¬p ∧ ¬q ⊢ ¬(p ∨ q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej47: &quot;¬p ∧ ¬q ⟹ ¬(p ∨ q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 48. Demostrar<br /> ¬p ∨ ¬q ⊢ ¬(p ∧ q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej48: &quot;¬p ∨ ¬q ⟹ ¬(p ∧ q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 49. Demostrar<br /> ⊢ ¬(p ∧ ¬p)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej49: &quot;¬(p ∧ ¬p)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 50. Demostrar<br /> p ∧ ¬p ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej50: &quot;p ∧ ¬p ⟹ q&quot;<br /> apply (erule conjE)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 51. Demostrar<br /> ¬¬p ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej51: &quot;¬¬p ⟹ p&quot;<br /> apply (erule notnotD)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 52. Demostrar<br /> ⊢ p ∨ ¬p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej52: &quot;p ∨ ¬p&quot;<br /> apply (cut_tac P=&quot;¬p&quot; in excluded_middle)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (erule notnotD)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 53. Demostrar<br /> ⊢ ((p ⟶ q) ⟶ p) ⟶ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej53: &quot;((p ⟶ q) ⟶ p) ⟶ p&quot;<br /> apply (rule impI)<br /> apply (rule ccontr)<br /> apply (cut_tac P=&quot;p ⟶ q&quot; in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule_tac P=&quot;p ⟶ q&quot; in notE)<br /> apply (rule impI)<br /> apply (erule notE)<br /> apply assumption<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 54. Demostrar<br /> ¬q ⟶ ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej54: &quot;¬q ⟶ ¬p ⟹ p ⟶ q&quot;<br /> apply (rule impI)<br /> apply (rule ccontr)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule notE)+<br /> apply assumption<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 55. Demostrar<br /> ¬(¬p ∧ ¬q) ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej55: &quot;¬(¬p ∧ ¬q) ⟹ p ∨ q&quot;<br /> apply (cut_tac P=p in excluded_middle)<br /> apply (erule disjE)<br /> apply (cut_tac P=q in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule notE)<br /> apply (rule conjI)<br /> apply assumption+<br /> apply (erule disjI2)<br /> apply (erule disjI1)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 56. Demostrar<br /> ¬(¬p ∨ ¬q) ⊢ p ∧ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej56: &quot;¬(¬p ∨ ¬q) ⟹ p ∧ q&quot;<br /> apply (rule conjI)<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (erule disjI1)<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (erule disjI2)<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 57. Demostrar<br /> ¬(p ∧ q) ⊢ ¬p ∨ ¬q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej57: &quot;¬(p ∧ q) ⟹ ¬p ∨ ¬q&quot;<br /> apply (cut_tac P=p in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (cut_tac P=q in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule disjI2)<br /> apply (erule notE)<br /> apply (rule conjI)<br /> apply assumption+<br /> done<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 58. Demostrar<br /> ⊢ (p ⟶ q) ∨ (q ⟶ p)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ej58: &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> apply (cut_tac P=p in excluded_middle)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (rule impI)<br /> apply (erule notE)<br /> apply assumption<br /> apply (rule disjI2)<br /> apply (rule impI)<br /> apply assumption<br /> done<br /> <br /> end<br /> <br /> &lt;/source&gt;</div> Mjoseh