LMF2019: Deducción natural proposicional (2)

PorJosé A. Alonso 27 febrero 20201 marzo 2020
En la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la deducción natural en la lógica proposicional.
Se han estudiado las siguientes reglas:
Reglas de la disyunción
Regla de copia
Reglas de la negación
Reglas del bicondicional
Regla del modus tollens
Regla de introducción de doble negación
Regla de reducción al absurdo
Ley del tercio excluido
Las transparencias correspondientes son las 11-28 del tema 2.
Descargar (PDF, 142KB)
Simultáneamente se ha explicado cómo formalizar demostraciones en
Isabelle/HOL. Los ejemplos correspondientes son los 12-24 de la
siguiente teoría
chapter ‹Tema 2a: Deducción natural proposicional con Isabelle/HOL›

theory T2a_Deduccion_natural_en_logica_proposicional_con_Isabelle
imports Main 
begin

text ‹En este tema se presentan los ejemplos del tema de deducción 
  natural proposicional siguiendo la presentación de Huth y Ryan en su 
  libro "Logic in Computer Science" http://goo.gl/qsVpY y, más 
  concretamente, a la forma como se explica en la asignatura de 
  "Lógica informática" (LI) http://goo.gl/AwDiv
 
  La página al lado de cada ejemplo indica la página de las 
  transparencias de LI donde se encuentra la demostración.›

section ‹Reglas de la conjunción›

text ‹  Notas sobre la lógica: Las reglas de la conjunción son
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  ›

thm conjI
thm conjunct1
thm conjunct2

subsection ‹Ejemplo 1›

text ‹Ejemplo 1 (p. 4). Demostrar que
     p ∧ q, r ⊢ q ∧ r. ›     

subsubsection ‹Demostración aplicativa›

lemma ejemplo_1: 
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  apply (rule conjI)
   apply (erule conjunct2)
  apply assumption  
  done 

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "⟦ ... ⟧" para representar las hipótesis,
  · ";" para separar las hipótesis y
  · "⟹" para separar las hipótesis de la conclusión.›

subsubsection ‹Demostración detallada›

lemma ejemplo_1_1:
  assumes 1: "p ∧ q" and
          2: "r" 
  shows "q ∧ r"     
proof -
  have 3: "q" using 1 by (rule conjunct2)
  show 4: "q ∧ r" using 3 2 by (rule conjI)
qed

text ‹Notas sobre el lenguaje: En la demostración anterior se ha usado
  · "assumes" para indicar las hipótesis,
  · "and" para separar las hipótesis,
  · "shows" para indicar la conclusión,
  · "proof" para iniciar la prueba,
  · "qed" para terminar la pruebas,
  · "-" (después de "proof") para no usar el método por defecto,
  · "have" para establecer un paso,
  · "using" para usar hechos en un paso,
  · "by (rule ..)" para indicar la regla con la que se peueba un hecho,
  · "show" para establecer la conclusión.›

subsubsection ‹Demostración estructurada›

text ‹Se pueden dejar implícitas las reglas como sigue›

lemma ejemplo_1_2:
  assumes 1: "p ∧ q" and 
          2: "r" 
  shows "q ∧ r"     
proof -
  have 3: "q" using 1 .. 
  show 4: "q ∧ r" using 3 2 ..
qed

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · ".." para indicar que se prueba por la regla correspondiente.›

text ‹Se pueden eliminar las etiquetas como sigue›

lemma ejemplo_1_3:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
proof -
  have "q" using assms(1) ..
  then show "q ∧ r" using assms(2) ..
qed

text ‹
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "assms(n)" para indicar la hipótesis n y
  · "then show" para demostrar la conclusión usando el hecho anterior.
  Además, no es necesario usar and entre las hipótesis.›

subsubsection ‹Demostración automática›

lemma ejemplo_1_4:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
  using assms
  by auto

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "assms" para indicar las hipótesis y
  · "by auto" para demostrar la conclusión automáticamente.›

subsubsection ‹Demostración detallada hacia atrás›

text ‹Se puede hacer la demostración por razonamiento hacia atrás,
  como sigue›

lemma ejemplo_1_5:
  assumes "p ∧ q" 
      and "r" 
  shows   "q ∧ r"     
proof (rule conjI)
  show "q" using assms(1) by (rule conjunct2)
next
  show "r" using assms(2) by this
qed

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "proof (rule r)" para indicar que se hará la demostración con la
    regla r,
  · "next" para indicar el comienzo de la prueba del siguiente
    subobjetivo,
  · "this" para indicar el hecho actual.›

subsubsection ‹Demostración estructurada hacia atrás›

text ‹Se pueden dejar implícitas las reglas como sigue›

lemma ejemplo_1_6:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
proof 
  show "q" using assms(1) ..
next
  show "r" using assms(2) . 
qed

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "." para indicar por el hecho actual.›

subsubsection ‹Demostraciones automáticas›

lemma ejemplo_1_7:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
  using assms by simp

― ‹Se puede acortar como sigue›
lemma ejemplo_1_8_:
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  by simp

section ‹Reglas de la doble negación›

subsection ‹Reglas de la doble negación›

text ‹La regla de eliminación de la doble negación es
  · notnotD: ¬¬ P ⟹ P

  Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
  introducción de la doble negación
  · notnotI: P ⟹ ¬¬ P
  aunque, de momento, no detallamos su demostración.›

lemma notnotI [intro!]: "P ⟹ ¬¬ P"
  by auto

subsection ‹Ejemplo 2›

text ‹Ejemplo 2. (p. 5)
       p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_2: 
  "⟦p; ¬¬(q ∧ r)⟧ ⟹ ¬¬p ∧ r"
  apply (rule conjI)
   apply (rule notnotI)
   apply assumption
  apply (drule notnotD)
  apply (erule conjunct2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_2_1:
  assumes 1: "p" and
          2: "¬¬(q ∧ r)" 
  shows      "¬¬p ∧ r"
proof -
  have 3: "¬¬p" using 1 by (rule notnotI)
  have 4: "q ∧ r" using 2 by (rule notnotD)
  have 5: "r" using 4 by (rule conjunct2)
  show 6: "¬¬p ∧ r" using 3 5 by (rule conjI)
qed        

subsubsection ‹Demostración estructurada›

― ‹Se puede eliminar etiquetas y reglas›
lemma ejemplo_2_2:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
proof -
  have "¬¬p" using assms(1) ..
  have "q ∧ r" using assms(2) by (rule notnotD)
  then have "r" ..
  with ‹¬¬p› show  "¬¬p ∧ r" ..
qed        

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · ‹...› para referenciar un hecho y
  · "with P show Q" para indicar que con el hecho anterior junto con el
    hecho P se demuestra Q.›

subsubsection ‹Demostración detallada hacia atrás›

lemma ejemplo_2_3:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
proof  (rule conjI)
  show "¬¬p" using assms(1) by (rule notnotI)
next
  have "q ∧ r" using assms(2) by (rule notnotD) 
  then show "r" by (rule conjunct2)
qed 

subsubsection ‹Demostración estructurada hacia atrás›

text ‹Se puede eliminar las reglas en la demostración anterior, como
  sigue:›

lemma ejemplo_2_4:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
proof 
  show "¬¬p" using assms(1) ..
next
  have "q ∧ r" using assms(2) by (rule notnotD) 
  then show "r" .. 
qed

subsubsection ‹Demostraciones automáticas›

lemma ejemplo_2_5:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
  using assms
  by simp

― ‹Se puede simplificar›
lemma ejemplo_2_6: 
  "⟦p; ¬¬(q ∧ r)⟧ ⟹ ¬¬p ∧ r"
  by simp

section ‹Regla de eliminación del condicional›

text ‹La regla de eliminación del condicional es la regla del modus 
  ponens
  · mp: ⟦P ⟶ Q; P⟧ ⟹ Q ›

subsection ‹Ejemplo 3›

text ‹Ejemplo 3. (p. 6) Demostrar que
     ¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_3: 
  "⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p"
  apply (erule mp)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_3_1:
  assumes 1: "¬p ∧ q" and 
          2: "¬p ∧ q ⟶ r ∨ ¬p" 
  shows      "r ∨ ¬p"
proof -
  show "r ∨ ¬p" using 2 1 by (rule mp)
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_3_2:
  assumes "¬p ∧ q"
          "¬p ∧ q ⟶ r ∨ ¬p" 
  shows   "r ∨ ¬p"
proof -
  show "r ∨ ¬p" using assms(2,1) ..
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_3_3:
  "⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p"
  by simp

subsection ‹Ejemplo 4›

text ‹Ejemplo 4 (p. 6) Demostrar que
     p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_4:
  "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
  apply (drule mp)
   apply assumption
  apply (drule mp)
   apply assumption
  apply (drule mp)
   apply assumption+
  done    

subsubsection ‹Demostración detallada›

lemma ejemplo_4_1:
  assumes 1: "p" and 
          2: "p ⟶ q" and 
          3: "p ⟶ (q ⟶ r)" 
  shows "r"
proof -
  have 4: "q" using 2 1 by (rule mp)
  have 5: "q ⟶ r" using 3 1 by (rule mp)
  show 6: "r" using 5 4 by (rule mp)
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_4_2:
  assumes "p"
          "p ⟶ q"
          "p ⟶ (q ⟶ r)" 
  shows "r"
proof -
  have "q" using assms(2,1) .. 
  have "q ⟶ r" using assms(3,1) ..
  then show "r" using ‹q› ..
qed

subsubsection ‹Demostración automática›

lemma ejemplo_4_3:
  "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
  by simp

section ‹Regla derivada del modus tollens›

text ‹Para ajustarnos al tema de LI vamos a introducir la regla del 
  modus tollens
  · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  aunque, de momento, sin detallar su demostración.›

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

subsection ‹Ejemplo 5›

text ‹Ejemplo 5 (p. 7). Demostrar
     p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_5: 
  "⟦p ⟶ (q ⟶ r); p; ¬r ⟧ ⟹ ¬q"
  apply (drule mp)
   apply assumption
  apply (erule mt)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_5_1:
  assumes 1: "p ⟶ (q ⟶ r)" and 
          2: "p" and 
          3: "¬r" 
  shows "¬q"
proof -
  have 4: "q ⟶ r" using 1 2 by (rule mp)
  show "¬q" using 4 3 by (rule mt)
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_5_2:
  assumes "p ⟶ (q ⟶ r)"
          "p"
          "¬r" 
  shows   "¬q"
proof -
  have "q ⟶ r" using assms(1,2) ..
  then show "¬q" using assms(3) by (rule mt)
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_5_3:
  assumes "p ⟶ (q ⟶ r)"
          "p"
          "¬r" 
  shows   "¬q"
  using assms
  by simp

lemma ejemplo_5_4: 
  "⟦p ⟶ (q ⟶ r); p; ¬r ⟧ ⟹ ¬q"
  by simp

subsection ‹Ejemplo 6›

text ‹Ejemplo 6. (p. 7) Demostrar 
     ¬p ⟶ q, ¬q ⊢ p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_6: 
  "⟦¬p ⟶ q; ¬q⟧ ⟹ p"
  apply (drule mt)
   apply assumption
  apply (erule notnotD)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_6_1:
  assumes 1: "¬p ⟶ q" and 
          2: "¬q" 
  shows "p"
proof -
  have 3: "¬¬p" using 1 2 by (rule mt)
  show "p" using 3 by (rule notnotD)
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_6_2:
  assumes "¬p ⟶ q"
          "¬q" 
  shows   "p"
proof -
  have "¬¬p" using assms(1,2) by (rule mt)
  then show "p" by (rule notnotD)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_6_3:
  "⟦¬p ⟶ q; ¬q⟧ ⟹ p"
  by simp

subsection ‹Ejemplo 7›

text ‹Ejemplo 7. (p. 7) Demostrar
     p ⟶ ¬q, q ⊢ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_7: 
  "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"  
  apply (erule mt)
  apply (erule notnotI)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_7_1:
  assumes 1: "p ⟶ ¬q" and 
          2: "q" 
  shows "¬p"
proof -
  have 3: "¬¬q" using 2 by (rule notnotI)
  show "¬p" using 1 3 by (rule mt)
qed

lemma ejemplo_7_2:
  assumes "p ⟶ ¬q"
          "q" 
  shows   "¬p"
proof -
  have "¬¬q" using assms(2) by (rule notnotI)
  with assms(1) show "¬p" by (rule mt)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_7_3:
  "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"
  by simp

section ‹Regla de introducción del condicional›

text ‹La regla de introducción del condicional es
  · impI: (P ⟹ Q) ⟹ P ⟶ Q ›

subsection ‹Ejemplo 8›

text ‹Ejemplo 8. (p. 8) Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_8: 
  "p ⟶ q ⟹ ¬q ⟶ ¬p"
  apply (rule impI)
  apply (erule mt)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_8_1:
  assumes 1: "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof -
  { assume 2: "¬q"
    have "¬p" using 1 2 by (rule mt) } 
  then show "¬q ⟶ ¬p" by (rule impI)
qed    

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "{ ... }" para representar una caja.›

subsubsection ‹Demostración estructurada›

lemma ejemplo_8_2:
  assumes "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof 
  assume "¬q"
  with assms show "¬p" by (rule mt)
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_8_3:
  assumes "p ⟶ q" 
  shows "¬q ⟶ ¬p"
  using assms
  by auto

subsection ‹Ejemplo 9›

text ‹Ejemplo 9. (p. 9) Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ ¬¬q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_9: 
  "¬q ⟶ ¬p ⟹ p ⟶ ¬¬q"  
  apply (rule impI)
  apply (erule mt)
  apply (erule notnotI)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_9_1: 
  assumes 1: "¬q ⟶ ¬p" 
  shows "p ⟶ ¬¬q"   
proof -
  { assume 2: "p"
    have 3: "¬¬p" using 2 by (rule notnotI)
    have "¬¬q" using 1 3 by (rule mt) } 
  then show "p ⟶ ¬¬q" by (rule impI)
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_9_2:
  assumes "¬q ⟶ ¬p" 
  shows    "p ⟶ ¬¬q"   
proof 
  assume "p"
  then have "¬¬p" by (rule notnotI)
  with assms show "¬¬q" by (rule mt)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_9_3:
  assumes "¬q ⟶ ¬p" 
  shows "p ⟶ ¬¬q"   
  using assms
  by auto 

subsection ‹Ejemplo 10›

text ‹Ejemplo 10 (p. 9). Demostrar
     ⊢ p ⟶ p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_10: 
  "p ⟶ p"
  apply (rule impI)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_10_1:
  "p ⟶ p"
proof -
  { assume 1: "p"
    have "p" using 1 by this }
  then show "p ⟶ p" by (rule impI) 
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_10_2:
  "p ⟶ p"
proof (rule impI)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_10_3:
  "p ⟶ p"
  by simp 

subsection ‹Ejemplo 11›

text ‹Ejemplo 11 (p. 10) Demostrar
     ⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_11:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"  
  apply (rule impI)+  
  apply (erule mp)
  apply (drule mt)
   apply (erule notnotI)
  apply (erule notnotD)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_11_1:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
  { assume 1: "q ⟶ r"
    { assume 2: "¬q ⟶ ¬p"
      { assume 3: "p"
        have 4: "¬¬p" using 3 by (rule notnotI)
        have 5: "¬¬q" using 2 4 by (rule mt)
        have 6: "q" using 5 by (rule notnotD)
        have "r" using 1 6 by (rule mp) } 
      then have "p ⟶ r" by (rule impI) } 
    then have "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI) } 
  then show "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

― ‹La demostración hacia atrás es›
lemma ejemplo_11_2:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
  assume 1: "q ⟶ r"
  show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
  proof (rule impI)
    assume 2: "¬q ⟶ ¬p"
    show "p ⟶ r"
    proof (rule impI)
      assume 3: "p"
      have 4: "¬¬p" using 3 by (rule notnotI)
      have 5: "¬¬q" using 2 4 by (rule mt)
      have 6: "q" using 5 by (rule notnotD)
      show "r" using 1 6 by (rule mp)
    qed
  qed
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_11_3:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
  assume 1: "q ⟶ r"
  show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
  proof
    assume 2: "¬q ⟶ ¬p"
    show "p ⟶ r"
    proof
      assume 3: "p"
      have 4: "¬¬p" using 3 ..
      have 5: "¬¬q" using 2 4 by (rule mt)
      have 6: "q" using 5 by (rule notnotD)
      show "r" using 1 6 ..
    qed
  qed
qed

― ‹La demostración sin etiquetas es› 
lemma ejemplo_11_4:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
  assume "q ⟶ r"
  show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
  proof
    assume "¬q ⟶ ¬p"
    show "p ⟶ r"
    proof
      assume "p"
      then have "¬¬p" ..
      with ‹¬q ⟶ ¬p› have "¬¬q" by (rule mt)
      then have "q" by (rule notnotD)
      with ‹q ⟶ r› show "r" ..
    qed
  qed
qed

subsubsection ‹Demostración automática›

lemma ejemplo_11_5:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
  by auto

section ‹Reglas de la disyunción›

text ‹Las reglas de la introducción de la disyunción son
  · disjI1: P ⟹ P ∨ Q
  · disjI2: Q ⟹ P ∨ Q
  La regla de elimación de la disyunción es
  · disjE:  ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R  ›

subsection ‹Ejemplo 12›

text ‹Ejemplo 12 (p. 11). Demostrar
     p ∨ q ⊢ q ∨ p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_12: 
  "p ∨ q ⟹ q ∨ p"  
  apply (erule disjE)
   apply (erule disjI2)
   apply (erule disjI1)
  done

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_12_1:
  assumes "p ∨ q" 
  shows "q ∨ p"
proof -
  have "p ∨ q" using assms by this
  moreover
  { assume 2: "p"
    have "q ∨ p" using 2 by (rule disjI2) }
  moreover
  { assume 3: "q"
    have "q ∨ p" using 3 by (rule disjI1) }
  ultimately show "q ∨ p" by (rule disjE) 
qed    

text ‹
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "moreover" para separar los bloques y
  · "ultimately" para unir los resultados de los bloques.›

subsubsection ‹Demostración estructurada›

― ‹La demostración detallada con reglas implícitas es›
lemma ejemplo_12_2:
  assumes "p ∨ q" 
  shows "q ∨ p"
proof -
  note ‹p ∨ q›
  moreover
  { assume "p"
    then have "q ∨ p" .. }
  moreover
  { assume "q"
    then have "q ∨ p" .. }
  ultimately show "q ∨ p" ..
qed    

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "note" para copiar un hecho.›

subsubsection ‹Demostración detallada hacia atrás›

lemma ejemplo_12_3:
  assumes 1: "p ∨ q" 
  shows "q ∨ p"
using 1
proof (rule disjE)
  { assume 2: "p"
    show "q ∨ p" using 2 by (rule disjI2) }
next
  { assume 3: "q"
    show "q ∨ p" using 3 by (rule disjI1) }
qed    

subsubsection ‹Demostración estructurada hacia atrás›

lemma ejemplo_12_4:
  assumes "p ∨ q" 
  shows "q ∨ p"
using assms
proof 
  { assume  "p"
    then show "q ∨ p" .. }
next
  { assume "q"
    then show "q ∨ p" .. }
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_12_5:
  assumes "p ∨ q" 
  shows "q ∨ p"
  using assms
  by auto

subsection ‹Ejemplo 13›

text ‹Ejemplo 13. (p. 12) Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_13: 
  "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"  
  apply (rule impI)
  apply (erule disjE)
   apply (erule disjI1)
  apply (drule mp)
   apply assumption
  apply (erule disjI2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_13_1:
  assumes 1: "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume 2: "p ∨ q"
  then show "p ∨ r"
  proof (rule disjE)
    { assume 3: "p"
      show "p ∨ r" using 3 by (rule disjI1) }
  next
    { assume 4: "q"
      have 5: "r" using 1 4 by (rule mp)
      show "p ∨ r" using 5 by (rule disjI2) }
  qed
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_13_2:
  assumes "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
proof 
  assume "p ∨ q"
  then show "p ∨ r"
  proof 
    { assume "p"
      then show "p ∨ r" .. }
  next
    { assume "q"
      have "r" using assms ‹q› ..
      then show "p ∨ r" .. }
  qed
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_13_3:
  assumes "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
  using assms
  by auto

section ‹Regla de copia›

subsection ‹Ejemplo 14›

text ‹Ejemplo 14 (p. 13). Demostrar
     ⊢ p ⟶ (q ⟶ p) ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_14: 
  "p ⟶ (q ⟶ p)"  
  apply (rule impI)+
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_14_1:
  "p ⟶ (q ⟶ p)"
proof (rule impI)
  assume 1: "p"
  show "q ⟶ p" 
  proof (rule impI)
    assume "q"
    show "p" using 1 by this
  qed
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_14_2:
  "p ⟶ (q ⟶ p)"
proof 
  assume "p"
  then show "q ⟶ p" ..
qed

subsubsection ‹Demostración automática›

lemma ejemplo_14_3:
  "p ⟶ (q ⟶ p)"
  by simp 

section ‹Reglas de la negación›

text ‹La regla de eliminación de lo falso es
  · FalseE: False ⟹ P
  La regla de eliminación de la negación es
  · notE: ⟦¬P; P⟧ ⟹ R
  La regla de introducción de la negación es
  · notI: (P ⟹ False) ⟹ ¬P ›

subsection ‹Ejemplo 15›

text ‹Ejemplo 15 (p. 15). Demostrar
     ¬p ∨ q ⊢ p ⟶ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_15: 
  "¬p ∨ q ⟹ p ⟶ q"  
  apply (rule impI)
  apply (erule disjE)
   apply (erule notE)
   apply assumption+
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_15_1:
  assumes 1: "¬p ∨ q" 
  shows "p ⟶ q"
proof (rule impI)
  assume 2: "p"
  note 1
  then show "q"
  proof (rule disjE)
    { assume 3: "¬p"
      show "q" using 3 2 by (rule notE) }
  next
    { assume 4: "q"
      show "q" using 4 by this}
  qed
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_15_2:
  assumes "¬p ∨ q" 
  shows "p ⟶ q"
proof 
  assume "p"
  note ‹¬p ∨ q›
  then show "q"
  proof
    assume "¬p"
    then show "q" using ‹p› .. 
  next
    assume "q"
      then show "q" .
  qed
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_15_3:
  assumes "¬p ∨ q" 
  shows "p ⟶ q"
  using assms
  by auto

subsection ‹Ejemplo 16›

text ‹Ejemplo 16 (p. 16). Demostrar
     p ⟶ q, p ⟶ ¬q ⊢ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_16: 
  "⟦p ⟶ q; p ⟶ ¬q⟧ ⟹ ¬p"  
  apply (rule notI)
  apply (drule mp)+
    apply assumption+
  apply (drule mp)
   apply assumption
  apply (erule notE)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_16_1:
  assumes 1: "p ⟶ q" and 
          2: "p ⟶ ¬q" 
  shows "¬p"    
proof (rule notI)
  assume 3: "p"
  have 4: "q" using 1 3 by (rule mp)
  have 5: "¬q" using 2 3 by (rule mp)
  show False using 5 4 by (rule notE)
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_16_2:
  assumes "p ⟶ q"
          "p ⟶ ¬q" 
  shows "¬p"    
proof 
  assume "p"
  have "q" using assms(1) ‹p› ..
  have "¬q" using assms(2) ‹p› ..
  then show False using ‹q› ..
qed

subsubsection ‹Demostración automática›

lemma ejemplo_16_3:
  assumes "p ⟶ q"
          "p ⟶ ¬q" 
  shows "¬p"    
  using assms
  by simp 

section ‹Reglas del bicondicional›

text ‹La regla de introducción del bicondicional es
  · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q
  Las reglas de eliminación del bicondicional son
  · iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P 
  · iffD2: ⟦P ⟷ Q; Q⟧ ⟹ P ›

subsection ‹Ejemplo 17›

text ‹Ejemplo 17 (p. 17) Demostrar
     (p ∧ q) ⟷ (q ∧ p) ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_17_4: 
  "(p ∧ q) ⟷ (q ∧ p)"  
  apply (rule iffI)
   apply (rule conjI)
    apply (erule conjunct2)
   apply (erule conjunct1)
    apply (rule conjI)
    apply (erule conjunct2)
  apply (erule conjunct1)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_17_1:
  "(p ∧ q) ⟷ (q ∧ p)" 
proof (rule iffI)
  { assume 1: "p ∧ q"
    have 2: "p" using 1 by (rule conjunct1)
    have 3: "q" using 1 by (rule conjunct2)
    show "q ∧ p" using 3 2 by (rule conjI) }
next
  { assume 4: "q ∧ p"
    have 5: "q" using 4 by (rule conjunct1)
    have 6: "p" using 4 by (rule conjunct2)
    show "p ∧ q" using 6 5 by (rule conjI) }
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_17_2:
  "(p ∧ q) ⟷ (q ∧ p)"
proof 
  { assume 1: "p ∧ q"
    have "p" using 1 ..
    have "q" using 1 ..
    show "q ∧ p" using ‹q› ‹p› .. }
next
  { assume 2: "q ∧ p"
    have "q" using 2 ..
    have "p" using 2 ..
    show "p ∧ q" using ‹p› ‹q›  .. }
qed

subsubsection ‹Demostración automática›

lemma ejemplo_17_3:
  "(p ∧ q) ⟷ (q ∧ p)"
  by auto

subsection ‹Ejemplo 18›

text ‹Ejemplo 18 (p. 18). Demostrar
     p ⟷ q, p ∨ q ⊢ p ∧ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_18_4: 
  "⟦p ⟷ q; p ∨ q⟧ ⟹ p ∧ q"  
  apply (erule disjE)
   apply (rule conjI)
    apply assumption
   apply (erule iffD1)
   apply assumption
  apply (rule conjI)
   apply (erule iffD2)
   apply assumption+
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_18_1:
  assumes 1: "p ⟷ q" and 
          2: "p ∨ q"  
  shows "p ∧ q"
using 2
proof (rule disjE)
  { assume 3: "p"
    have 4: "q" using 1 3 by (rule iffD1)
    show "p ∧ q" using 3 4 by (rule conjI) }
next
  { assume 5: "q"
    have 6: "p" using 1 5 by (rule iffD2)
    show "p ∧ q" using 6 5 by (rule conjI) }
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_18_2:
  assumes "p ⟷ q"
          "p ∨ q"  
  shows  "p ∧ q"
using assms(2)
proof
  { assume "p"
    with assms(1) have "q" ..
    with ‹p› show "p ∧ q" .. }
next
  { assume "q"
    with assms(1) have "p" ..
    then show "p ∧ q" using ‹q› .. }
qed

subsubsection ‹Demostración automática›

lemma ejemplo_18_3:
  assumes "p ⟷ q"
          "p ∨ q"  
  shows "p ∧ q"
  using assms
  by simp 

section ‹Reglas derivadas›

subsection ‹Regla del modus tollens›

text ‹Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir 
  de las reglas básicas.›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_20: 
  "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"  
  apply (rule notI)
  apply (drule mp)
   apply assumption
  apply (erule notE)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_20_1:
  assumes 1: "F ⟶ G" and 
          2: "¬G" 
  shows "¬F"
proof (rule notI)
  assume 3: "F"
  have 4: "G" using 1 3 by (rule mp)
  show False using 2 4 by (rule notE)
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_20_2:
  assumes "F ⟶ G"
          "¬G" 
  shows   "¬F"
proof 
  assume "F"
  with assms(1) have "G" ..
  with assms(2) show False ..
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_20_3:
  assumes "F ⟶ G"
          "¬G" 
  shows "¬F"
  using assms
  by simp 

subsection ‹Regla de la introducción de la doble negación›

text ‹Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
  negación a partir de las reglas básicas.›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_21: 
  "F ⟹ ¬¬F"  
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_21_1:
  assumes 1: "F" 
  shows "¬¬F"
proof (rule notI)
  assume 2: "¬F"
  show False using 2 1 by (rule notE)
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_21_2:
  assumes "F" 
  shows "¬¬F"
proof 
  assume "¬F"
  then show False using assms ..
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_21_3:
  assumes "F" 
  shows "¬¬F"
  using assms
  by simp 

subsection ‹Regla de reducción al absurdo›

text ‹La regla de reducción al absurdo en Isabelle se correponde con la
  regla clásica de contradicción 
  · ccontr: (¬P ⟹ False) ⟹ P ›

subsection ‹Ley del tercio excluso›

text ‹La ley del tercio excluso es 
  · excluded_middle: ¬P ∨ P ›

text ‹Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
  las reglas básicas.›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_22:
  "F ∨ ¬F"
  apply (rule ccontr)
  apply (rule_tac P="F" in notE)
   apply (rule notI)
   apply (erule notE)
   apply (erule disjI1)
  apply (rule notnotD)
  apply (rule notI)
  apply (erule notE)
  apply (erule disjI2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_22_1:
  "F ∨ ¬F"
proof (rule ccontr)
  assume 1: "¬(F ∨ ¬F)"
  then show False
  proof (rule notE)
    show "F ∨ ¬F"
    proof (rule disjI2)
      show "¬F"
      proof (rule notI)
        assume 2: "F"
        then have 3: "F ∨ ¬F" by (rule disjI1)
        show False using 1 3 by (rule notE)
      qed
    qed
  qed
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_22_2:
  "F ∨ ¬F"
proof (rule ccontr)
  assume "¬(F ∨ ¬F)"
  then show False
  proof (rule notE)
    show "F ∨ ¬F"
    proof (rule disjI2)
      show "¬F"
      proof (rule notI)
        assume "F"
        then have "F ∨ ¬F" ..
        with ‹¬(F ∨ ¬F)› show False ..
      qed
    qed
  qed
qed

subsubsection ‹Demostración automática›

lemma ejemplo_22_3:
  "F ∨ ¬F"
  by simp 

subsection ‹Ejemplo 23›

text ‹Ejemplo 23 (p. 24). Demostrar
     p ⟶ q ⊢ ¬p ∨ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_23: 
  "p ⟶ q ⟹ ¬p ∨ q"
  apply (cut_tac P="p" in excluded_middle)
  apply (erule disjE)
   apply (erule disjI1)
  apply (drule mp)
   apply assumption
  apply (erule disjI2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_23_1:
  assumes 1: "p ⟶ q" 
  shows "¬p ∨ q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  then show "¬p ∨ q"
  proof (rule disjE)
    { assume "¬p"
      then show "¬p ∨ q" by (rule disjI1) }
  next
    { assume 2: "p"
      have "q" using 1 2 by (rule mp)
      then show "¬p ∨ q" by (rule disjI2) }
  qed
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_23_2:
  assumes "p ⟶ q" 
  shows "¬p ∨ q"
proof -
  have "¬p ∨ p" ..
  then show "¬p ∨ q"
  proof 
    { assume "¬p"
      then show "¬p ∨ q" .. }
  next
    { assume "p"
      with assms have "q" ..
      then show "¬p ∨ q" .. }
  qed
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_23_3:
  assumes "p ⟶ q" 
  shows "¬p ∨ q"
  using assms
  by simp 

section ‹Demostraciones por contradicción›

subsection ‹Ejemplo 24›

text ‹Ejemplo 24. Demostrar que 
     ¬p, p ∨ q ⊢ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_24_4: 
  "⟦¬p ; p ∨ q⟧ ⟹ q"  
  apply (erule disjE)
   apply (erule notE)
   apply assumption+
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_24_1:
  assumes "¬p"
          "p ∨ q"
  shows   "q"
using ‹p ∨ q›
proof (rule disjE)
  assume "p"
  with assms(1) show "q" by contradiction 
next
  assume "q"
  then show "q" by assumption
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_24_2:
  assumes "¬p"
          "p ∨ q"
  shows "q"
using ‹p ∨ q›
proof 
  assume "p"
  with assms(1) show "q" ..
next
  assume "q"
  then show "q" .
qed

subsubsection ‹Demostración automática›

lemma ejemplo_24_3:
  assumes "¬p"
          "p ∨ q"
  shows "q"
  using assms
  by simp 

end
1
2
3
4
5
6
7
8
9
10
11
Se puede imprimir o compartir con
