R3

chapter ‹ R3: Deducción natural proposicional(II)  ›

theory R3
imports Main 
begin

text ‹------------------------------------------------------------------ 
  El objetivo de esta relación es demostrar cada uno de los ejercicios
  usando sólo las reglas básicas de deducción natural de la lógica
  proposicional (sin usar los método simp ni auto).

  Para cada ejercicio dar una demostración estructurada y otra
  aplicativa.

  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  
  · notnotD:    ¬¬ P ⟹ P
  · notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
  ---------------------------------------------------------------------›

text ‹Se usarán las reglas notnotI y mt que demostramos a continuación.›

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

section ‹ Disyunciones ›

text ‹ --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------  ›

lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------  ›

lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------  ›

lemma ejercicio_27:
  assumes "p ∨ q"
  shows   "q ∨ p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------  ›

lemma ejercicio_28:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------  ›

lemma ejercicio_29:
  assumes "p ∨ p"
  shows   "p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------  ›

lemma ejercicio_30:
  assumes "p" 
  shows   "p ∨ p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------  ›

lemma ejercicio_31:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------  ›

lemma ejercicio_32:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------  ›

lemma ejercicio_33:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------  ›

lemma ejercicio_34:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------  ›

lemma ejercicio_35:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 36. Demostrar
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
  ------------------------------------------------------------------  ›

lemma ejercicio_36:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 37. Demostrar
     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
  ------------------------------------------------------------------  ›

lemma ejercicio_37:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------  ›

lemma ejercicio_38:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
oops

section ‹ Negaciones  ›

text ‹ --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------  ›

lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------  ›

lemma ejercicio_40:
  assumes "¬p" 
  shows   "p ⟶ q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------  ›

lemma ejercicio_41:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p∨q, ¬q ⊢ p
  ------------------------------------------------------------------  ›

lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------  ›

lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------  ›

lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------  ›

lemma ejercicio_45:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 46. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------  ›

lemma ejercicio_46:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 47. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------  ›

lemma ejercicio_47:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 48. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------  ›

lemma ejercicio_48:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------  ›

lemma ejercicio_49:
  "¬(p ∧ ¬p)"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------  ›

lemma ejercicio_50:
  assumes "p ∧ ¬p" 
  shows   "q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------  ›

lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------  ›

lemma ejercicio_52:
  "p ∨ ¬p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 53. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------  ›

lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 54. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------  ›

lemma ejercicio_54:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------  ›

lemma ejercicio_55:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------  ›

lemma ejercicio_56:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------  ›

lemma ejercicio_57:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
oops

text ‹ --------------------------------------------------------------- 
  Ejercicio 58. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ ›

lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
oops

end