R6

chapter ‹R6: Deducción natural proposicional›

theory R6_Deduccion_natural_proposicional_1
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 ‹Implicaciones›

text ‹--------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       p ⟶ q, p ⊢ q
  ------------------------------------------------------------------›

lemma ejercicio_1:
  assumes "p ⟶ q"
          "p"
  shows "q"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ⟶ q, q ⟶ r, p ⊢ r
  ------------------------------------------------------------------›

lemma ejercicio_2:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
  ------------------------------------------------------------------›

lemma ejercicio_3:
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows "r"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     p ⟶ q, q ⟶ r ⊢ p ⟶ r
  ------------------------------------------------------------------›

lemma ejercicio_4:
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows "p ⟶ r"
oops

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

lemma ejercicio_5:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
oops

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

lemma ejercicio_6:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     p ⊢ q ⟶ p
  ------------------------------------------------------------------›

lemma ejercicio_7:
  assumes "p"  
  shows   "q ⟶ p"
oops

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

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

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

lemma ejercicio_9:
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------›

lemma ejercicio_10:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
oops

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

lemma ejercicio_11:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops

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

lemma ejercicio_12:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
oops

section ‹Conjunciones›

text ‹--------------------------------------------------------------- 
  Ejercicio 13. Demostrar
     p, q ⊢  p ∧ q
  ------------------------------------------------------------------›

lemma ejercicio_13:
  assumes "p"
          "q" 
  shows "p ∧ q"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------›

lemma ejercicio_14:
  assumes "p ∧ q"  
  shows   "p"
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------›

lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"
oops

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

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

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

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

text ‹--------------------------------------------------------------- 
  Ejercicio 18. Demostrar
     p ∧ q ⊢ p ⟶ q
  ------------------------------------------------------------------›

lemma ejercicio_18:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
oops

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

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

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

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

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

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

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

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

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

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

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

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


end