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
