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.
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 |