https://www.glc.us.es/~jalonso/DAO2012/index.php?action=history&feed=atom&title=Rel_3
Rel 3 - Historial de revisiones
2026-07-17T13:11:08Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_3&diff=122&oldid=prev
Jalonso en 18:55 15 jul 2018
2018-07-15T18:55:12Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 18:55 15 jul 2018</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td>
<td colspan="2" class="diff-lineno">Línea 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><source lang="<del class="diffchange diffchange-inline">isar</del>"></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><source lang="<ins class="diffchange diffchange-inline">isabelle</ins>"></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Relación 3: Deducción natural proposicional *}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Relación 3: Deducción natural proposicional *}</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
</table>
Jalonso
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_3&diff=59&oldid=prev
Jalonso: Protegió «Rel 3» ([edit=sysop] (indefinido) [move=sysop] (indefinido))
2012-12-18T17:48:20Z
<p>Protegió «<a href="/~jalonso/DAO2012/index.php/Rel_3" title="Rel 3">Rel 3</a>» ([edit=sysop] (indefinido) [move=sysop] (indefinido))</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 17:48 18 dic 2012</td>
</tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div>
</td></tr></table>
Jalonso
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Rel_3&diff=57&oldid=prev
Jalonso: Página creada con '<source lang="isar"> header {* Relación 3: Deducción natural proposicional *} theory DNLP imports Main begin text {* -----------------------------------------------------...'
2012-12-18T17:47:16Z
<p>Página creada con '<source lang="isar"> header {* Relación 3: Deducción natural proposicional *} theory DNLP imports Main begin text {* -----------------------------------------------------...'</p>
<p><b>Página nueva</b></p><div><source lang="isar"><br />
header {* Relación 3: Deducción natural proposicional *}<br />
<br />
theory DNLP<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<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 />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación.<br />
*}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_1:<br />
assumes "p ⟶ q" and<br />
"p"<br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_2:<br />
assumes "p ⟶ q" and <br />
"q ⟶ r" and <br />
"p" <br />
shows "r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_3:<br />
assumes "p ⟶ (q ⟶ r)" and <br />
"p ⟶ q" and <br />
"p"<br />
shows "r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_4:<br />
assumes "p ⟶ q" and <br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_5:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_6:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_7:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_8:<br />
"p ⟶ (q ⟶ p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_9:<br />
assumes "p ⟶ q" <br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_11:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_13:<br />
assumes "p" and <br />
"q" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q) ∧ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_17:<br />
assumes "(p ∧ q) ∧ r" <br />
shows "p ∧ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_19:<br />
assumes "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ q ∧ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_21:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_22:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_23:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_24:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
oops<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q" and <br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q" and "¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Jalonso