Diferencia entre revisiones de «R7»
De Lógica matemática y fundamentos (2018-19)
| (No se muestra una edición intermedia del mismo usuario) | |||
| Línea 1: | Línea 1: | ||
<source lang = "isabelle"> | <source lang = "isabelle"> | ||
| − | |||
| − | |||
theory R7 | theory R7 | ||
imports Main | imports Main | ||
| Línea 8: | Línea 6: | ||
text {* | text {* | ||
--------------------------------------------------------------------- | --------------------------------------------------------------------- | ||
| − | + | El objetivo de esta relación es escribir demostraciones usando sólo | |
las reglas básicas de deducción natural de la lógica proposicional y | las reglas básicas de deducción natural de la lógica proposicional y | ||
los métodos rule, erule, frule, drule y assumption. | los métodos rule, erule, frule, drule y assumption. | ||
| − | |||
Las reglas básicas de la deducción natural son las siguientes: | Las reglas básicas de la deducción natural son las siguientes: | ||
| − | · conjI: | + | · conjI: ⟦P; Q⟧ ⟹ P ∧ Q |
| − | · conjunct1: | + | · conjunct1: P ∧ Q ⟹ P |
| − | · conjunct2: | + | · conjunct2: P ∧ Q ⟹ Q |
| − | · | + | · conjE: ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R |
| − | · | + | · notE: ⟦¬P; P⟧ ⟹ R |
| − | · mp: | + | · notI: (P ⟹ False) ⟹ ¬P |
| − | · mt: | + | · mp: ⟦P ⟶ Q; P⟧ ⟹ Q |
| − | · impI: | + | · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F |
| − | · disjI1: | + | · impI: (P ⟹ Q) ⟹ P ⟶ Q |
| − | · disjI2: | + | · impE: ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R |
| − | · disjE: | + | · disjI1: P ⟹ P ∨ Q |
| − | · FalseE: | + | · disjI2: Q ⟹ P ∨ Q |
| − | + | · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R | |
| − | + | · FalseE: False ⟹ P | |
| − | · iffI: | + | · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q |
| − | · iffD1: | + | · iffD1: ⟦Q = P; Q⟧ ⟹ P |
| − | · iffD2: | + | · iffD2: ⟦P = Q; Q⟧ ⟹ P |
| − | · ccontr: | + | · iffE: ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R |
| + | · notnotD: ¬¬ P ⟹ P | ||
| + | · not_not: P = ¬¬P | ||
| + | · ccontr: (¬P ⟹ False) ⟹ P | ||
| + | · excluded_midle: ¬P ∨ P | ||
| + | · classical: (¬ P ⟹ P) ⟹ P | ||
| + | · contrapos_nn ⟦¬Q; P ⟹ Q⟧ ⟹ ¬P | ||
--------------------------------------------------------------------- | --------------------------------------------------------------------- | ||
*} | *} | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
section {* Implicaciones *} | section {* Implicaciones *} | ||
| Línea 51: | Línea 45: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej1: "⟦p ⟶ q; p⟧ ⟹ q" |
| − | |||
| − | |||
| − | |||
oops | oops | ||
| Línea 62: | Línea 53: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej2: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r" |
| − | + | oops | |
| − | |||
| − | |||
| − | |||
| − | oops | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 74: | Línea 61: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej3a: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" |
| − | + | oops | |
| − | + | ||
| − | + | lemma ej3b: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" | |
| − | |||
oops | oops | ||
| Línea 86: | Línea 72: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | -- "La demostración detallada es" |
| − | + | lemma ej4: "⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r" | |
| − | + | oops | |
| − | |||
| − | oops | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 97: | Línea 81: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej5: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)" |
| − | |||
| − | |||
oops | oops | ||
| − | + | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 6. Demostrar | Ejercicio 6. Demostrar | ||
| Línea 107: | Línea 89: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej6: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)" |
| − | + | oops | |
| − | |||
| − | oops | ||
| + | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 7. Demostrar | Ejercicio 7. Demostrar | ||
| Línea 117: | Línea 98: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej7: "p ⟹ q ⟶ p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 8. Demostrar | Ejercicio 8. Demostrar | ||
| Línea 127: | Línea 106: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej8: "p ⟶ (q ⟶ p)" |
| − | + | oops | |
| − | oops | + | |
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 9. Demostrar | Ejercicio 9. Demostrar | ||
| Línea 136: | Línea 114: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej9: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)" |
| − | + | oops | |
| − | |||
| − | oops | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 146: | Línea 122: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej10: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 11. Demostrar | Ejercicio 11. Demostrar | ||
| Línea 156: | Línea 130: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej11: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" |
| − | + | oops | |
| − | oops | + | |
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 12. Demostrar | Ejercicio 12. Demostrar | ||
| Línea 165: | Línea 138: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej12: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
section {* Conjunciones *} | section {* Conjunciones *} | ||
| Línea 177: | Línea 148: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej13: "⟦p; q⟧ ⟹ p ∧ q" |
| − | + | oops | |
| − | + | ||
| − | |||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 14. Demostrar | Ejercicio 14. Demostrar | ||
| Línea 188: | Línea 156: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej14: "p ∧ q ⟹ p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 15. Demostrar | Ejercicio 15. Demostrar | ||
| Línea 198: | Línea 164: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej15: "p ∧ q ⟹ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 16. Demostrar | Ejercicio 16. Demostrar | ||
| Línea 208: | Línea 172: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej16: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 17. Demostrar | Ejercicio 17. Demostrar | ||
| Línea 218: | Línea 180: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej17: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 18. Demostrar | Ejercicio 18. Demostrar | ||
| Línea 228: | Línea 188: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej18: "p ∧ q ⟹ p ⟶ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 19. Demostrar | Ejercicio 19. Demostrar | ||
| Línea 238: | Línea 196: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej19: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 20. Demostrar | Ejercicio 20. Demostrar | ||
| Línea 248: | Línea 204: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej20: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 21. Demostrar | Ejercicio 21. Demostrar | ||
| Línea 258: | Línea 212: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej21_1: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 22. Demostrar | Ejercicio 22. Demostrar | ||
| Línea 268: | Línea 220: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej22: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 23. Demostrar | Ejercicio 23. Demostrar | ||
| Línea 278: | Línea 228: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej23: "(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 24. Demostrar | Ejercicio 24. Demostrar | ||
| Línea 288: | Línea 236: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej24: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
section {* Disyunciones *} | section {* Disyunciones *} | ||
| Línea 300: | Línea 246: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej25: "p ⟹ p ∨ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 26. Demostrar | Ejercicio 26. Demostrar | ||
| Línea 310: | Línea 254: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej26: "q ⟹ p ∨ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 27. Demostrar | Ejercicio 27. Demostrar | ||
| Línea 320: | Línea 262: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej27: "p ∨ q ⟹ q ∨ p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 28. Demostrar | Ejercicio 28. Demostrar | ||
| Línea 330: | Línea 270: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 29. Demostrar | Ejercicio 29. Demostrar | ||
| Línea 340: | Línea 278: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej29: "p ∨ p ⟹ p" |
| − | + | oops | |
| − | |||
| − | oops | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 350: | Línea 286: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej30: "p ⟹ p ∨ p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 31. Demostrar | Ejercicio 31. Demostrar | ||
| Línea 360: | Línea 294: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej31: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 32. Demostrar | Ejercicio 32. Demostrar | ||
| Línea 370: | Línea 302: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej32: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 33. Demostrar | Ejercicio 33. Demostrar | ||
| Línea 380: | Línea 310: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej33: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 34. Demostrar | Ejercicio 34. Demostrar | ||
| Línea 390: | Línea 318: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej34: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 35. Demostrar | Ejercicio 35. Demostrar | ||
| Línea 400: | Línea 326: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej35: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 36. Demostrar | Ejercicio 36. Demostrar | ||
| Línea 410: | Línea 334: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej36: "(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 37. Demostrar | Ejercicio 37. Demostrar | ||
| Línea 420: | Línea 342: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej37: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 38. Demostrar | Ejercicio 38. Demostrar | ||
| Línea 430: | Línea 350: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej38: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)" |
| − | + | oops | |
| − | + | ||
| − | oops | + | section {* Negación *} |
| − | |||
| − | section {* | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 442: | Línea 360: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej39: "p ⟹ ¬¬p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 40. Demostrar | Ejercicio 40. Demostrar | ||
| Línea 452: | Línea 368: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej40: "¬p ⟹ p ⟶ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 41. Demostrar | Ejercicio 41. Demostrar | ||
| Línea 462: | Línea 376: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 42. Demostrar | Ejercicio 42. Demostrar | ||
| − | + | p ∨ q, ¬q ⊢ p | |
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p" |
| − | + | oops | |
| − | + | ||
| − | |||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| − | Ejercicio | + | Ejercicio 43. Demostrar |
p ∨ q, ¬p ⊢ q | p ∨ q, ¬p ⊢ q | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q" |
| − | + | oops | |
| − | + | ||
| − | |||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| − | Ejercicio | + | Ejercicio 44. Demostrar |
p ∨ q ⊢ ¬(¬p ∧ ¬q) | p ∨ q ⊢ ¬(¬p ∧ ¬q) | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej44: "p ∨ q ⟹ ¬(¬p ∧ ¬q)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 45. Demostrar | Ejercicio 45. Demostrar | ||
| Línea 504: | Línea 408: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej45: "p ∧ q ⟹ ¬(¬p ∨ ¬q)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 46. Demostrar | Ejercicio 46. Demostrar | ||
| Línea 514: | Línea 416: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej46: "¬(p ∨ q) ⟹ ¬p ∧ ¬q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 47. Demostrar | Ejercicio 47. Demostrar | ||
| Línea 524: | Línea 424: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej47: "¬p ∧ ¬q ⟹ ¬(p ∨ q)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 48. Demostrar | Ejercicio 48. Demostrar | ||
| Línea 534: | Línea 432: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej48: "¬p ∨ ¬q ⟹ ¬(p ∧ q)" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 49. Demostrar | Ejercicio 49. Demostrar | ||
| Línea 544: | Línea 440: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej49: "¬(p ∧ ¬p)" |
| − | + | oops | |
| − | oops | + | |
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 50. Demostrar | Ejercicio 50. Demostrar | ||
| Línea 553: | Línea 448: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej50: "p ∧ ¬p ⟹ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 51. Demostrar | Ejercicio 51. Demostrar | ||
| Línea 563: | Línea 456: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej51: "¬¬p ⟹ p" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 52. Demostrar | Ejercicio 52. Demostrar | ||
| Línea 573: | Línea 464: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej52: "p ∨ ¬p" |
| − | + | oops | |
| − | oops | + | |
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 53. Demostrar | Ejercicio 53. Demostrar | ||
| Línea 582: | Línea 472: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p" |
| − | + | oops | |
| − | oops | + | |
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 54. Demostrar | Ejercicio 54. Demostrar | ||
| Línea 591: | Línea 480: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 55. Demostrar | Ejercicio 55. Demostrar | ||
| Línea 601: | Línea 488: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 56. Demostrar | Ejercicio 56. Demostrar | ||
| Línea 611: | Línea 496: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej56: "¬(¬p ∨ ¬q) ⟹ p ∧ q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 57. Demostrar | Ejercicio 57. Demostrar | ||
| Línea 621: | Línea 504: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q" |
| − | + | oops | |
| − | + | ||
| − | oops | ||
| − | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 58. Demostrar | Ejercicio 58. Demostrar | ||
| Línea 631: | Línea 512: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej58: "(p ⟶ q) ∨ (q ⟶ p)" |
| − | + | oops | |
| − | oops | ||
end | end | ||
| + | |||
</source> | </source> | ||
Revisión actual del 14:29 28 mar 2019
theory R7
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es escribir demostraciones usando sólo
las reglas básicas de deducción natural de la lógica proposicional y
los métodos rule, erule, frule, drule y assumption.
Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· conjE: ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· impE: ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· iffE: ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
· notnotD: ¬¬ P ⟹ P
· not_not: P = ¬¬P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_midle: ¬P ∨ P
· classical: (¬ P ⟹ P) ⟹ P
· contrapos_nn ⟦¬Q; P ⟹ Q⟧ ⟹ ¬P
---------------------------------------------------------------------
*}
section {* Implicaciones *}
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}
lemma ej1: "⟦p ⟶ q; p⟧ ⟹ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
lemma ej2: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
lemma ej3a: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
oops
lemma ej3b: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ej4: "⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej5: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej6: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
lemma ej7: "p ⟹ q ⟶ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ej8: "p ⟶ (q ⟶ p)"
oops
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej9: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
lemma ej10: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))"
oops
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
lemma ej11: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ej12: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)"
oops
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ej13: "⟦p; q⟧ ⟹ p ∧ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
lemma ej14: "p ∧ q ⟹ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
lemma ej15: "p ∧ q ⟹ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
lemma ej16: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
lemma ej17: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ej18: "p ∧ q ⟹ p ⟶ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
lemma ej19: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej20: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
lemma ej21_1: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ej22: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
lemma ej23: "(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
lemma ej24: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r"
oops
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ej25: "p ⟹ p ∨ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ej26: "q ⟹ p ∨ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
lemma ej27: "p ∨ q ⟹ q ∨ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
lemma ej29: "p ∨ p ⟹ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
lemma ej30: "p ⟹ p ∨ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
lemma ej31: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
lemma ej32: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
lemma ej33: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
lemma ej34: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
lemma ej35: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}
lemma ej36: "(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
lemma ej37: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ej38: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)"
oops
section {* Negación *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
lemma ej39: "p ⟹ ¬¬p"
oops
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ej40: "¬p ⟹ p ⟶ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p"
oops
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}
lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 43. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 44. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
lemma ej44: "p ∨ q ⟹ ¬(¬p ∧ ¬q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
lemma ej45: "p ∧ q ⟹ ¬(¬p ∨ ¬q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
lemma ej46: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
oops
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
lemma ej47: "¬p ∧ ¬q ⟹ ¬(p ∨ q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
lemma ej48: "¬p ∨ ¬q ⟹ ¬(p ∧ q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
lemma ej49: "¬(p ∧ ¬p)"
oops
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ej50: "p ∧ ¬p ⟹ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
lemma ej51: "¬¬p ⟹ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
lemma ej52: "p ∨ ¬p"
oops
text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ej56: "¬(¬p ∨ ¬q) ⟹ p ∧ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q"
oops
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ej58: "(p ⟶ q) ∨ (q ⟶ p)"
oops
end