{"id":7062,"date":"2020-02-27T10:02:47","date_gmt":"2020-02-27T09:02:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7062"},"modified":"2020-03-01T10:04:05","modified_gmt":"2020-03-01T09:04:05","slug":"lmf2019-deduccion-natural-proposicional-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-deduccion-natural-proposicional-2\/","title":{"rendered":"LMF2019: Deducci\u00f3n natural proposicional (2)"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">L\u00f3gica matem\u00e1tica y  fundamentos<\/a> se ha continuado el estudio de la deducci\u00f3n natural en la l\u00f3gica proposicional.<\/p>\n<p>Se han estudiado las siguientes reglas:<\/p>\n<ul>\n<li>Reglas de la disyunci\u00f3n<\/li>\n<li>Regla de copia<\/li>\n<li>Reglas de la negaci\u00f3n<\/li>\n<li>Reglas del bicondicional<\/li>\n<li>Regla del modus tollens<\/li>\n<li>Regla de introducci\u00f3n de doble negaci\u00f3n<\/li>\n<li>Regla de reducci\u00f3n al absurdo<\/li>\n<li>Ley del tercio excluido<\/li>\n<\/ul>\n<p>Las transparencias correspondientes son las 11-28 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\/temas\/tema-2.pdf\">tema 2<\/a>.<br \/>\n<iframe src=\"\/\/docs.google.com\/viewer?url=http%3A%2F%2Fwww.cs.us.es%2F%7Ejalonso%2Fcursos%2Flmf-19%2Ftemas%2Ftema-2.pdf&hl=es&embedded=true\" class=\"gde-frame\" style=\"width:100%; height:500px; border: none;\" scrolling=\"no\"><\/iframe>\n<p class=\"gde-text\"><a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\/temas\/tema-2.pdf\" class=\"gde-link\">Descargar (PDF, 142KB)<\/a><\/p><\/p>\n<p>Simult\u00e1neamente se ha explicado c\u00f3mo formalizar demostraciones en<br \/>\nIsabelle\/HOL. Los ejemplos correspondientes son los 12-24 de la<br \/>\nsiguiente teor\u00eda<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 2a: Deducci\u00f3n natural proposicional con Isabelle\/HOL\u203a\n\ntheory T2a_Deduccion_natural_en_logica_proposicional_con_Isabelle\nimports Main \nbegin\n\ntext \u2039En este tema se presentan los ejemplos del tema de deducci\u00f3n \n  natural proposicional siguiendo la presentaci\u00f3n de Huth y Ryan en su \n  libro \"Logic in Computer Science\" http:\/\/goo.gl\/qsVpY y, m\u00e1s \n  concretamente, a la forma como se explica en la asignatura de \n  \"L\u00f3gica inform\u00e1tica\" (LI) http:\/\/goo.gl\/AwDiv\n \n  La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las \n  transparencias de LI donde se encuentra la demostraci\u00f3n.\u203a\n\nsection \u2039Reglas de la conjunci\u00f3n\u203a\n\ntext \u2039  Notas sobre la l\u00f3gica: Las reglas de la conjunci\u00f3n son\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \u203a\n\nthm conjI\nthm conjunct1\nthm conjunct2\n\nsubsection \u2039Ejemplo 1\u203a\n\ntext \u2039Ejemplo 1 (p. 4). Demostrar que\n     p \u2227 q, r \u22a2 q \u2227 r. \u203a     \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_1: \n  \"\u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\"\n  apply (rule conjI)\n   apply (erule conjunct2)\n  apply assumption  \n  done \n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"\u27e6 ... \u27e7\" para representar las hip\u00f3tesis,\n  \u00b7 \";\" para separar las hip\u00f3tesis y\n  \u00b7 \"\u27f9\" para separar las hip\u00f3tesis de la conclusi\u00f3n.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_1_1:\n  assumes 1: \"p \u2227 q\" and\n          2: \"r\" \n  shows \"q \u2227 r\"     \nproof -\n  have 3: \"q\" using 1 by (rule conjunct2)\n  show 4: \"q \u2227 r\" using 3 2 by (rule conjI)\nqed\n\ntext \u2039Notas sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"assumes\" para indicar las hip\u00f3tesis,\n  \u00b7 \"and\" para separar las hip\u00f3tesis,\n  \u00b7 \"shows\" para indicar la conclusi\u00f3n,\n  \u00b7 \"proof\" para iniciar la prueba,\n  \u00b7 \"qed\" para terminar la pruebas,\n  \u00b7 \"-\" (despu\u00e9s de \"proof\") para no usar el m\u00e9todo por defecto,\n  \u00b7 \"have\" para establecer un paso,\n  \u00b7 \"using\" para usar hechos en un paso,\n  \u00b7 \"by (rule ..)\" para indicar la regla con la que se peueba un hecho,\n  \u00b7 \"show\" para establecer la conclusi\u00f3n.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\ntext \u2039Se pueden dejar impl\u00edcitas las reglas como sigue\u203a\n\nlemma ejemplo_1_2:\n  assumes 1: \"p \u2227 q\" and \n          2: \"r\" \n  shows \"q \u2227 r\"     \nproof -\n  have 3: \"q\" using 1 .. \n  show 4: \"q \u2227 r\" using 3 2 ..\nqed\n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"..\" para indicar que se prueba por la regla correspondiente.\u203a\n\ntext \u2039Se pueden eliminar las etiquetas como sigue\u203a\n\nlemma ejemplo_1_3:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \nproof -\n  have \"q\" using assms(1) ..\n  then show \"q \u2227 r\" using assms(2) ..\nqed\n\ntext \u2039\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"assms(n)\" para indicar la hip\u00f3tesis n y\n  \u00b7 \"then show\" para demostrar la conclusi\u00f3n usando el hecho anterior.\n  Adem\u00e1s, no es necesario usar and entre las hip\u00f3tesis.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_1_4:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \n  using assms\n  by auto\n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"assms\" para indicar las hip\u00f3tesis y\n  \u00b7 \"by auto\" para demostrar la conclusi\u00f3n autom\u00e1ticamente.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada hacia atr\u00e1s\u203a\n\ntext \u2039Se puede hacer la demostraci\u00f3n por razonamiento hacia atr\u00e1s,\n  como sigue\u203a\n\nlemma ejemplo_1_5:\n  assumes \"p \u2227 q\" \n      and \"r\" \n  shows   \"q \u2227 r\"     \nproof (rule conjI)\n  show \"q\" using assms(1) by (rule conjunct2)\nnext\n  show \"r\" using assms(2) by this\nqed\n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"proof (rule r)\" para indicar que se har\u00e1 la demostraci\u00f3n con la\n    regla r,\n  \u00b7 \"next\" para indicar el comienzo de la prueba del siguiente\n    subobjetivo,\n  \u00b7 \"this\" para indicar el hecho actual.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada hacia atr\u00e1s\u203a\n\ntext \u2039Se pueden dejar impl\u00edcitas las reglas como sigue\u203a\n\nlemma ejemplo_1_6:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \nproof \n  show \"q\" using assms(1) ..\nnext\n  show \"r\" using assms(2) . \nqed\n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \".\" para indicar por el hecho actual.\u203a\n\nsubsubsection \u2039Demostraciones autom\u00e1ticas\u203a\n\nlemma ejemplo_1_7:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \n  using assms by simp\n\n\u2015 \u2039Se puede acortar como sigue\u203a\nlemma ejemplo_1_8_:\n  \"\u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\"\n  by simp\n\nsection \u2039Reglas de la doble negaci\u00f3n\u203a\n\nsubsection \u2039Reglas de la doble negaci\u00f3n\u203a\n\ntext \u2039La regla de eliminaci\u00f3n de la doble negaci\u00f3n es\n  \u00b7 notnotD: \u00ac\u00ac P \u27f9 P\n\n  Para ajustarnos al tema de LI vamos a introducir la siguiente regla de\n  introducci\u00f3n de la doble negaci\u00f3n\n  \u00b7 notnotI: P \u27f9 \u00ac\u00ac P\n  aunque, de momento, no detallamos su demostraci\u00f3n.\u203a\n\nlemma notnotI [intro!]: \"P \u27f9 \u00ac\u00ac P\"\n  by auto\n\nsubsection \u2039Ejemplo 2\u203a\n\ntext \u2039Ejemplo 2. (p. 5)\n       p, \u00ac\u00ac(q \u2227 r) \u22a2 \u00ac\u00acp \u2227 r \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_2: \n  \"\u27e6p; \u00ac\u00ac(q \u2227 r)\u27e7 \u27f9 \u00ac\u00acp \u2227 r\"\n  apply (rule conjI)\n   apply (rule notnotI)\n   apply assumption\n  apply (drule notnotD)\n  apply (erule conjunct2)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_2_1:\n  assumes 1: \"p\" and\n          2: \"\u00ac\u00ac(q \u2227 r)\" \n  shows      \"\u00ac\u00acp \u2227 r\"\nproof -\n  have 3: \"\u00ac\u00acp\" using 1 by (rule notnotI)\n  have 4: \"q \u2227 r\" using 2 by (rule notnotD)\n  have 5: \"r\" using 4 by (rule conjunct2)\n  show 6: \"\u00ac\u00acp \u2227 r\" using 3 5 by (rule conjI)\nqed        \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039Se puede eliminar etiquetas y reglas\u203a\nlemma ejemplo_2_2:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nproof -\n  have \"\u00ac\u00acp\" using assms(1) ..\n  have \"q \u2227 r\" using assms(2) by (rule notnotD)\n  then have \"r\" ..\n  with \u2039\u00ac\u00acp\u203a show  \"\u00ac\u00acp \u2227 r\" ..\nqed        \n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \u2039...\u203a para referenciar un hecho y\n  \u00b7 \"with P show Q\" para indicar que con el hecho anterior junto con el\n    hecho P se demuestra Q.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada hacia atr\u00e1s\u203a\n\nlemma ejemplo_2_3:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nproof  (rule conjI)\n  show \"\u00ac\u00acp\" using assms(1) by (rule notnotI)\nnext\n  have \"q \u2227 r\" using assms(2) by (rule notnotD) \n  then show \"r\" by (rule conjunct2)\nqed \n\nsubsubsection \u2039Demostraci\u00f3n estructurada hacia atr\u00e1s\u203a\n\ntext \u2039Se puede eliminar las reglas en la demostraci\u00f3n anterior, como\n  sigue:\u203a\n\nlemma ejemplo_2_4:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nproof \n  show \"\u00ac\u00acp\" using assms(1) ..\nnext\n  have \"q \u2227 r\" using assms(2) by (rule notnotD) \n  then show \"r\" .. \nqed\n\nsubsubsection \u2039Demostraciones autom\u00e1ticas\u203a\n\nlemma ejemplo_2_5:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\n  using assms\n  by simp\n\n\u2015 \u2039Se puede simplificar\u203a\nlemma ejemplo_2_6: \n  \"\u27e6p; \u00ac\u00ac(q \u2227 r)\u27e7 \u27f9 \u00ac\u00acp \u2227 r\"\n  by simp\n\nsection \u2039Regla de eliminaci\u00f3n del condicional\u203a\n\ntext \u2039La regla de eliminaci\u00f3n del condicional es la regla del modus \n  ponens\n  \u00b7 mp: \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \u203a\n\nsubsection \u2039Ejemplo 3\u203a\n\ntext \u2039Ejemplo 3. (p. 6) Demostrar que\n     \u00acp \u2227 q, \u00acp \u2227 q \u27f6 r \u2228 \u00acp \u22a2 r \u2228 \u00acp \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_3: \n  \"\u27e6\u00acp \u2227 q; \u00acp \u2227 q \u27f6 r \u2228 \u00acp\u27e7 \u27f9 r \u2228 \u00acp\"\n  apply (erule mp)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_3_1:\n  assumes 1: \"\u00acp \u2227 q\" and \n          2: \"\u00acp \u2227 q \u27f6 r \u2228 \u00acp\" \n  shows      \"r \u2228 \u00acp\"\nproof -\n  show \"r \u2228 \u00acp\" using 2 1 by (rule mp)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_3_2:\n  assumes \"\u00acp \u2227 q\"\n          \"\u00acp \u2227 q \u27f6 r \u2228 \u00acp\" \n  shows   \"r \u2228 \u00acp\"\nproof -\n  show \"r \u2228 \u00acp\" using assms(2,1) ..\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_3_3:\n  \"\u27e6\u00acp \u2227 q; \u00acp \u2227 q \u27f6 r \u2228 \u00acp\u27e7 \u27f9 r \u2228 \u00acp\"\n  by simp\n\nsubsection \u2039Ejemplo 4\u203a\n\ntext \u2039Ejemplo 4 (p. 6) Demostrar que\n     p, p \u27f6 q, p \u27f6 (q \u27f6 r) \u22a2 r \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_4:\n  \"\u27e6p; p \u27f6 q; p \u27f6 (q \u27f6 r)\u27e7 \u27f9 r\"\n  apply (drule mp)\n   apply assumption\n  apply (drule mp)\n   apply assumption\n  apply (drule mp)\n   apply assumption+\n  done    \n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_4_1:\n  assumes 1: \"p\" and \n          2: \"p \u27f6 q\" and \n          3: \"p \u27f6 (q \u27f6 r)\" \n  shows \"r\"\nproof -\n  have 4: \"q\" using 2 1 by (rule mp)\n  have 5: \"q \u27f6 r\" using 3 1 by (rule mp)\n  show 6: \"r\" using 5 4 by (rule mp)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_4_2:\n  assumes \"p\"\n          \"p \u27f6 q\"\n          \"p \u27f6 (q \u27f6 r)\" \n  shows \"r\"\nproof -\n  have \"q\" using assms(2,1) .. \n  have \"q \u27f6 r\" using assms(3,1) ..\n  then show \"r\" using \u2039q\u203a ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_4_3:\n  \"\u27e6p; p \u27f6 q; p \u27f6 (q \u27f6 r)\u27e7 \u27f9 r\"\n  by simp\n\nsection \u2039Regla derivada del modus tollens\u203a\n\ntext \u2039Para ajustarnos al tema de LI vamos a introducir la regla del \n  modus tollens\n  \u00b7 mt: \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \n  aunque, de momento, sin detallar su demostraci\u00f3n.\u203a\n\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\n  by simp\n\nsubsection \u2039Ejemplo 5\u203a\n\ntext \u2039Ejemplo 5 (p. 7). Demostrar\n     p \u27f6 (q \u27f6 r), p, \u00acr \u22a2 \u00acq \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_5: \n  \"\u27e6p \u27f6 (q \u27f6 r); p; \u00acr \u27e7 \u27f9 \u00acq\"\n  apply (drule mp)\n   apply assumption\n  apply (erule mt)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_5_1:\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" and \n          2: \"p\" and \n          3: \"\u00acr\" \n  shows \"\u00acq\"\nproof -\n  have 4: \"q \u27f6 r\" using 1 2 by (rule mp)\n  show \"\u00acq\" using 4 3 by (rule mt)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_5_2:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p\"\n          \"\u00acr\" \n  shows   \"\u00acq\"\nproof -\n  have \"q \u27f6 r\" using assms(1,2) ..\n  then show \"\u00acq\" using assms(3) by (rule mt)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_5_3:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p\"\n          \"\u00acr\" \n  shows   \"\u00acq\"\n  using assms\n  by simp\n\nlemma ejemplo_5_4: \n  \"\u27e6p \u27f6 (q \u27f6 r); p; \u00acr \u27e7 \u27f9 \u00acq\"\n  by simp\n\nsubsection \u2039Ejemplo 6\u203a\n\ntext \u2039Ejemplo 6. (p. 7) Demostrar \n     \u00acp \u27f6 q, \u00acq \u22a2 p \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_6: \n  \"\u27e6\u00acp \u27f6 q; \u00acq\u27e7 \u27f9 p\"\n  apply (drule mt)\n   apply assumption\n  apply (erule notnotD)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_6_1:\n  assumes 1: \"\u00acp \u27f6 q\" and \n          2: \"\u00acq\" \n  shows \"p\"\nproof -\n  have 3: \"\u00ac\u00acp\" using 1 2 by (rule mt)\n  show \"p\" using 3 by (rule notnotD)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_6_2:\n  assumes \"\u00acp \u27f6 q\"\n          \"\u00acq\" \n  shows   \"p\"\nproof -\n  have \"\u00ac\u00acp\" using assms(1,2) by (rule mt)\n  then show \"p\" by (rule notnotD)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_6_3:\n  \"\u27e6\u00acp \u27f6 q; \u00acq\u27e7 \u27f9 p\"\n  by simp\n\nsubsection \u2039Ejemplo 7\u203a\n\ntext \u2039Ejemplo 7. (p. 7) Demostrar\n     p \u27f6 \u00acq, q \u22a2 \u00acp \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_7: \n  \"\u27e6p \u27f6 \u00acq; q\u27e7 \u27f9 \u00acp\"  \n  apply (erule mt)\n  apply (erule notnotI)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_7_1:\n  assumes 1: \"p \u27f6 \u00acq\" and \n          2: \"q\" \n  shows \"\u00acp\"\nproof -\n  have 3: \"\u00ac\u00acq\" using 2 by (rule notnotI)\n  show \"\u00acp\" using 1 3 by (rule mt)\nqed\n\nlemma ejemplo_7_2:\n  assumes \"p \u27f6 \u00acq\"\n          \"q\" \n  shows   \"\u00acp\"\nproof -\n  have \"\u00ac\u00acq\" using assms(2) by (rule notnotI)\n  with assms(1) show \"\u00acp\" by (rule mt)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_7_3:\n  \"\u27e6p \u27f6 \u00acq; q\u27e7 \u27f9 \u00acp\"\n  by simp\n\nsection \u2039Regla de introducci\u00f3n del condicional\u203a\n\ntext \u2039La regla de introducci\u00f3n del condicional es\n  \u00b7 impI: (P \u27f9 Q) \u27f9 P \u27f6 Q \u203a\n\nsubsection \u2039Ejemplo 8\u203a\n\ntext \u2039Ejemplo 8. (p. 8) Demostrar\n     p \u27f6 q \u22a2 \u00acq \u27f6 \u00acp \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_8: \n  \"p \u27f6 q \u27f9 \u00acq \u27f6 \u00acp\"\n  apply (rule impI)\n  apply (erule mt)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_8_1:\n  assumes 1: \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\nproof -\n  { assume 2: \"\u00acq\"\n    have \"\u00acp\" using 1 2 by (rule mt) } \n  then show \"\u00acq \u27f6 \u00acp\" by (rule impI)\nqed    \n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"{ ... }\" para representar una caja.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_8_2:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\nproof \n  assume \"\u00acq\"\n  with assms show \"\u00acp\" by (rule mt)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_8_3:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\n  using assms\n  by auto\n\nsubsection \u2039Ejemplo 9\u203a\n\ntext \u2039Ejemplo 9. (p. 9) Demostrar\n     \u00acq \u27f6 \u00acp \u22a2 p \u27f6 \u00ac\u00acq \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_9: \n  \"\u00acq \u27f6 \u00acp \u27f9 p \u27f6 \u00ac\u00acq\"  \n  apply (rule impI)\n  apply (erule mt)\n  apply (erule notnotI)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_9_1: \n  assumes 1: \"\u00acq \u27f6 \u00acp\" \n  shows \"p \u27f6 \u00ac\u00acq\"   \nproof -\n  { assume 2: \"p\"\n    have 3: \"\u00ac\u00acp\" using 2 by (rule notnotI)\n    have \"\u00ac\u00acq\" using 1 3 by (rule mt) } \n  then show \"p \u27f6 \u00ac\u00acq\" by (rule impI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_9_2:\n  assumes \"\u00acq \u27f6 \u00acp\" \n  shows    \"p \u27f6 \u00ac\u00acq\"   \nproof \n  assume \"p\"\n  then have \"\u00ac\u00acp\" by (rule notnotI)\n  with assms show \"\u00ac\u00acq\" by (rule mt)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_9_3:\n  assumes \"\u00acq \u27f6 \u00acp\" \n  shows \"p \u27f6 \u00ac\u00acq\"   \n  using assms\n  by auto \n\nsubsection \u2039Ejemplo 10\u203a\n\ntext \u2039Ejemplo 10 (p. 9). Demostrar\n     \u22a2 p \u27f6 p \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_10: \n  \"p \u27f6 p\"\n  apply (rule impI)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_10_1:\n  \"p \u27f6 p\"\nproof -\n  { assume 1: \"p\"\n    have \"p\" using 1 by this }\n  then show \"p \u27f6 p\" by (rule impI) \nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_10_2:\n  \"p \u27f6 p\"\nproof (rule impI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_10_3:\n  \"p \u27f6 p\"\n  by simp \n\nsubsection \u2039Ejemplo 11\u203a\n\ntext \u2039Ejemplo 11 (p. 10) Demostrar\n     \u22a2 (q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_11:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"  \n  apply (rule impI)+  \n  apply (erule mp)\n  apply (drule mt)\n   apply (erule notnotI)\n  apply (erule notnotD)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_11_1:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof -\n  { assume 1: \"q \u27f6 r\"\n    { assume 2: \"\u00acq \u27f6 \u00acp\"\n      { assume 3: \"p\"\n        have 4: \"\u00ac\u00acp\" using 3 by (rule notnotI)\n        have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\n        have 6: \"q\" using 5 by (rule notnotD)\n        have \"r\" using 1 6 by (rule mp) } \n      then have \"p \u27f6 r\" by (rule impI) } \n    then have \"(\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r\" by (rule impI) } \n  then show \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r)\" by (rule impI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n hacia atr\u00e1s es\u203a\nlemma ejemplo_11_2:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof (rule impI)\n  assume 1: \"q \u27f6 r\"\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\n  proof (rule impI)\n    assume 2: \"\u00acq \u27f6 \u00acp\"\n    show \"p \u27f6 r\"\n    proof (rule impI)\n      assume 3: \"p\"\n      have 4: \"\u00ac\u00acp\" using 3 by (rule notnotI)\n      have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\n      have 6: \"q\" using 5 by (rule notnotD)\n      show \"r\" using 1 6 by (rule mp)\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_11_3:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof\n  assume 1: \"q \u27f6 r\"\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\n  proof\n    assume 2: \"\u00acq \u27f6 \u00acp\"\n    show \"p \u27f6 r\"\n    proof\n      assume 3: \"p\"\n      have 4: \"\u00ac\u00acp\" using 3 ..\n      have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\n      have 6: \"q\" using 5 by (rule notnotD)\n      show \"r\" using 1 6 ..\n    qed\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n sin etiquetas es\u203a \nlemma ejemplo_11_4:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof\n  assume \"q \u27f6 r\"\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\n  proof\n    assume \"\u00acq \u27f6 \u00acp\"\n    show \"p \u27f6 r\"\n    proof\n      assume \"p\"\n      then have \"\u00ac\u00acp\" ..\n      with \u2039\u00acq \u27f6 \u00acp\u203a have \"\u00ac\u00acq\" by (rule mt)\n      then have \"q\" by (rule notnotD)\n      with \u2039q \u27f6 r\u203a show \"r\" ..\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_11_5:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\n  by auto\n\nsection \u2039Reglas de la disyunci\u00f3n\u203a\n\ntext \u2039Las reglas de la introducci\u00f3n de la disyunci\u00f3n son\n  \u00b7 disjI1: P \u27f9 P \u2228 Q\n  \u00b7 disjI2: Q \u27f9 P \u2228 Q\n  La regla de elimaci\u00f3n de la disyunci\u00f3n es\n  \u00b7 disjE:  \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R  \u203a\n\nsubsection \u2039Ejemplo 12\u203a\n\ntext \u2039Ejemplo 12 (p. 11). Demostrar\n     p \u2228 q \u22a2 q \u2228 p \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_12: \n  \"p \u2228 q \u27f9 q \u2228 p\"  \n  apply (erule disjE)\n   apply (erule disjI2)\n   apply (erule disjI1)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_12_1:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nproof -\n  have \"p \u2228 q\" using assms by this\n  moreover\n  { assume 2: \"p\"\n    have \"q \u2228 p\" using 2 by (rule disjI2) }\n  moreover\n  { assume 3: \"q\"\n    have \"q \u2228 p\" using 3 by (rule disjI1) }\n  ultimately show \"q \u2228 p\" by (rule disjE) \nqed    \n\ntext \u2039\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"moreover\" para separar los bloques y\n  \u00b7 \"ultimately\" para unir los resultados de los bloques.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada con reglas impl\u00edcitas es\u203a\nlemma ejemplo_12_2:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nproof -\n  note \u2039p \u2228 q\u203a\n  moreover\n  { assume \"p\"\n    then have \"q \u2228 p\" .. }\n  moreover\n  { assume \"q\"\n    then have \"q \u2228 p\" .. }\n  ultimately show \"q \u2228 p\" ..\nqed    \n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"note\" para copiar un hecho.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada hacia atr\u00e1s\u203a\n\nlemma ejemplo_12_3:\n  assumes 1: \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing 1\nproof (rule disjE)\n  { assume 2: \"p\"\n    show \"q \u2228 p\" using 2 by (rule disjI2) }\nnext\n  { assume 3: \"q\"\n    show \"q \u2228 p\" using 3 by (rule disjI1) }\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada hacia atr\u00e1s\u203a\n\nlemma ejemplo_12_4:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing assms\nproof \n  { assume  \"p\"\n    then show \"q \u2228 p\" .. }\nnext\n  { assume \"q\"\n    then show \"q \u2228 p\" .. }\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_12_5:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\n  using assms\n  by auto\n\nsubsection \u2039Ejemplo 13\u203a\n\ntext \u2039Ejemplo 13. (p. 12) Demostrar\n     q \u27f6 r \u22a2 p \u2228 q \u27f6 p \u2228 r \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_13: \n  \"q \u27f6 r \u27f9 p \u2228 q \u27f6 p \u2228 r\"  \n  apply (rule impI)\n  apply (erule disjE)\n   apply (erule disjI1)\n  apply (drule mp)\n   apply assumption\n  apply (erule disjI2)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_13_1:\n  assumes 1: \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nproof (rule impI)\n  assume 2: \"p \u2228 q\"\n  then show \"p \u2228 r\"\n  proof (rule disjE)\n    { assume 3: \"p\"\n      show \"p \u2228 r\" using 3 by (rule disjI1) }\n  next\n    { assume 4: \"q\"\n      have 5: \"r\" using 1 4 by (rule mp)\n      show \"p \u2228 r\" using 5 by (rule disjI2) }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_13_2:\n  assumes \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nproof \n  assume \"p \u2228 q\"\n  then show \"p \u2228 r\"\n  proof \n    { assume \"p\"\n      then show \"p \u2228 r\" .. }\n  next\n    { assume \"q\"\n      have \"r\" using assms \u2039q\u203a ..\n      then show \"p \u2228 r\" .. }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_13_3:\n  assumes \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\n  using assms\n  by auto\n\nsection \u2039Regla de copia\u203a\n\nsubsection \u2039Ejemplo 14\u203a\n\ntext \u2039Ejemplo 14 (p. 13). Demostrar\n     \u22a2 p \u27f6 (q \u27f6 p) \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_14: \n  \"p \u27f6 (q \u27f6 p)\"  \n  apply (rule impI)+\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_14_1:\n  \"p \u27f6 (q \u27f6 p)\"\nproof (rule impI)\n  assume 1: \"p\"\n  show \"q \u27f6 p\" \n  proof (rule impI)\n    assume \"q\"\n    show \"p\" using 1 by this\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_14_2:\n  \"p \u27f6 (q \u27f6 p)\"\nproof \n  assume \"p\"\n  then show \"q \u27f6 p\" ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_14_3:\n  \"p \u27f6 (q \u27f6 p)\"\n  by simp \n\nsection \u2039Reglas de la negaci\u00f3n\u203a\n\ntext \u2039La regla de eliminaci\u00f3n de lo falso es\n  \u00b7 FalseE: False \u27f9 P\n  La regla de eliminaci\u00f3n de la negaci\u00f3n es\n  \u00b7 notE: \u27e6\u00acP; P\u27e7 \u27f9 R\n  La regla de introducci\u00f3n de la negaci\u00f3n es\n  \u00b7 notI: (P \u27f9 False) \u27f9 \u00acP \u203a\n\nsubsection \u2039Ejemplo 15\u203a\n\ntext \u2039Ejemplo 15 (p. 15). Demostrar\n     \u00acp \u2228 q \u22a2 p \u27f6 q \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_15: \n  \"\u00acp \u2228 q \u27f9 p \u27f6 q\"  \n  apply (rule impI)\n  apply (erule disjE)\n   apply (erule notE)\n   apply assumption+\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_15_1:\n  assumes 1: \"\u00acp \u2228 q\" \n  shows \"p \u27f6 q\"\nproof (rule impI)\n  assume 2: \"p\"\n  note 1\n  then show \"q\"\n  proof (rule disjE)\n    { assume 3: \"\u00acp\"\n      show \"q\" using 3 2 by (rule notE) }\n  next\n    { assume 4: \"q\"\n      show \"q\" using 4 by this}\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_15_2:\n  assumes \"\u00acp \u2228 q\" \n  shows \"p \u27f6 q\"\nproof \n  assume \"p\"\n  note \u2039\u00acp \u2228 q\u203a\n  then show \"q\"\n  proof\n    assume \"\u00acp\"\n    then show \"q\" using \u2039p\u203a .. \n  next\n    assume \"q\"\n      then show \"q\" .\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_15_3:\n  assumes \"\u00acp \u2228 q\" \n  shows \"p \u27f6 q\"\n  using assms\n  by auto\n\nsubsection \u2039Ejemplo 16\u203a\n\ntext \u2039Ejemplo 16 (p. 16). Demostrar\n     p \u27f6 q, p \u27f6 \u00acq \u22a2 \u00acp \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_16: \n  \"\u27e6p \u27f6 q; p \u27f6 \u00acq\u27e7 \u27f9 \u00acp\"  \n  apply (rule notI)\n  apply (drule mp)+\n    apply assumption+\n  apply (drule mp)\n   apply assumption\n  apply (erule notE)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_16_1:\n  assumes 1: \"p \u27f6 q\" and \n          2: \"p \u27f6 \u00acq\" \n  shows \"\u00acp\"    \nproof (rule notI)\n  assume 3: \"p\"\n  have 4: \"q\" using 1 3 by (rule mp)\n  have 5: \"\u00acq\" using 2 3 by (rule mp)\n  show False using 5 4 by (rule notE)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_16_2:\n  assumes \"p \u27f6 q\"\n          \"p \u27f6 \u00acq\" \n  shows \"\u00acp\"    \nproof \n  assume \"p\"\n  have \"q\" using assms(1) \u2039p\u203a ..\n  have \"\u00acq\" using assms(2) \u2039p\u203a ..\n  then show False using \u2039q\u203a ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_16_3:\n  assumes \"p \u27f6 q\"\n          \"p \u27f6 \u00acq\" \n  shows \"\u00acp\"    \n  using assms\n  by simp \n\nsection \u2039Reglas del bicondicional\u203a\n\ntext \u2039La regla de introducci\u00f3n del bicondicional es\n  \u00b7 iffI: \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P \u27f7 Q\n  Las reglas de eliminaci\u00f3n del bicondicional son\n  \u00b7 iffD1: \u27e6Q \u27f7 P; Q\u27e7 \u27f9 P \n  \u00b7 iffD2: \u27e6P \u27f7 Q; Q\u27e7 \u27f9 P \u203a\n\nsubsection \u2039Ejemplo 17\u203a\n\ntext \u2039Ejemplo 17 (p. 17) Demostrar\n     (p \u2227 q) \u27f7 (q \u2227 p) \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_17_4: \n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"  \n  apply (rule iffI)\n   apply (rule conjI)\n    apply (erule conjunct2)\n   apply (erule conjunct1)\n    apply (rule conjI)\n    apply (erule conjunct2)\n  apply (erule conjunct1)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_17_1:\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\" \nproof (rule iffI)\n  { assume 1: \"p \u2227 q\"\n    have 2: \"p\" using 1 by (rule conjunct1)\n    have 3: \"q\" using 1 by (rule conjunct2)\n    show \"q \u2227 p\" using 3 2 by (rule conjI) }\nnext\n  { assume 4: \"q \u2227 p\"\n    have 5: \"q\" using 4 by (rule conjunct1)\n    have 6: \"p\" using 4 by (rule conjunct2)\n    show \"p \u2227 q\" using 6 5 by (rule conjI) }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_17_2:\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\nproof \n  { assume 1: \"p \u2227 q\"\n    have \"p\" using 1 ..\n    have \"q\" using 1 ..\n    show \"q \u2227 p\" using \u2039q\u203a \u2039p\u203a .. }\nnext\n  { assume 2: \"q \u2227 p\"\n    have \"q\" using 2 ..\n    have \"p\" using 2 ..\n    show \"p \u2227 q\" using \u2039p\u203a \u2039q\u203a  .. }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_17_3:\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\n  by auto\n\nsubsection \u2039Ejemplo 18\u203a\n\ntext \u2039Ejemplo 18 (p. 18). Demostrar\n     p \u27f7 q, p \u2228 q \u22a2 p \u2227 q \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_18_4: \n  \"\u27e6p \u27f7 q; p \u2228 q\u27e7 \u27f9 p \u2227 q\"  \n  apply (erule disjE)\n   apply (rule conjI)\n    apply assumption\n   apply (erule iffD1)\n   apply assumption\n  apply (rule conjI)\n   apply (erule iffD2)\n   apply assumption+\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_18_1:\n  assumes 1: \"p \u27f7 q\" and \n          2: \"p \u2228 q\"  \n  shows \"p \u2227 q\"\nusing 2\nproof (rule disjE)\n  { assume 3: \"p\"\n    have 4: \"q\" using 1 3 by (rule iffD1)\n    show \"p \u2227 q\" using 3 4 by (rule conjI) }\nnext\n  { assume 5: \"q\"\n    have 6: \"p\" using 1 5 by (rule iffD2)\n    show \"p \u2227 q\" using 6 5 by (rule conjI) }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_18_2:\n  assumes \"p \u27f7 q\"\n          \"p \u2228 q\"  \n  shows  \"p \u2227 q\"\nusing assms(2)\nproof\n  { assume \"p\"\n    with assms(1) have \"q\" ..\n    with \u2039p\u203a show \"p \u2227 q\" .. }\nnext\n  { assume \"q\"\n    with assms(1) have \"p\" ..\n    then show \"p \u2227 q\" using \u2039q\u203a .. }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_18_3:\n  assumes \"p \u27f7 q\"\n          \"p \u2228 q\"  \n  shows \"p \u2227 q\"\n  using assms\n  by simp \n\nsection \u2039Reglas derivadas\u203a\n\nsubsection \u2039Regla del modus tollens\u203a\n\ntext \u2039Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir \n  de las reglas b\u00e1sicas.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_20: \n  \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"  \n  apply (rule notI)\n  apply (drule mp)\n   apply assumption\n  apply (erule notE)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_20_1:\n  assumes 1: \"F \u27f6 G\" and \n          2: \"\u00acG\" \n  shows \"\u00acF\"\nproof (rule notI)\n  assume 3: \"F\"\n  have 4: \"G\" using 1 3 by (rule mp)\n  show False using 2 4 by (rule notE)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_20_2:\n  assumes \"F \u27f6 G\"\n          \"\u00acG\" \n  shows   \"\u00acF\"\nproof \n  assume \"F\"\n  with assms(1) have \"G\" ..\n  with assms(2) show False ..\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_20_3:\n  assumes \"F \u27f6 G\"\n          \"\u00acG\" \n  shows \"\u00acF\"\n  using assms\n  by simp \n\nsubsection \u2039Regla de la introducci\u00f3n de la doble negaci\u00f3n\u203a\n\ntext \u2039Ejemplo 21 (p. 21) Demostrar la regla de introducci\u00f3n de la doble\n  negaci\u00f3n a partir de las reglas b\u00e1sicas.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_21: \n  \"F \u27f9 \u00ac\u00acF\"  \n  apply (rule notI)\n  apply (erule notE)\n  apply assumption\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_21_1:\n  assumes 1: \"F\" \n  shows \"\u00ac\u00acF\"\nproof (rule notI)\n  assume 2: \"\u00acF\"\n  show False using 2 1 by (rule notE)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_21_2:\n  assumes \"F\" \n  shows \"\u00ac\u00acF\"\nproof \n  assume \"\u00acF\"\n  then show False using assms ..\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_21_3:\n  assumes \"F\" \n  shows \"\u00ac\u00acF\"\n  using assms\n  by simp \n\nsubsection \u2039Regla de reducci\u00f3n al absurdo\u203a\n\ntext \u2039La regla de reducci\u00f3n al absurdo en Isabelle se correponde con la\n  regla cl\u00e1sica de contradicci\u00f3n \n  \u00b7 ccontr: (\u00acP \u27f9 False) \u27f9 P \u203a\n\nsubsection \u2039Ley del tercio excluso\u203a\n\ntext \u2039La ley del tercio excluso es \n  \u00b7 excluded_middle: \u00acP \u2228 P \u203a\n\ntext \u2039Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de\n  las reglas b\u00e1sicas.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_22:\n  \"F \u2228 \u00acF\"\n  apply (rule ccontr)\n  apply (rule_tac P=\"F\" in notE)\n   apply (rule notI)\n   apply (erule notE)\n   apply (erule disjI1)\n  apply (rule notnotD)\n  apply (rule notI)\n  apply (erule notE)\n  apply (erule disjI2)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_22_1:\n  \"F \u2228 \u00acF\"\nproof (rule ccontr)\n  assume 1: \"\u00ac(F \u2228 \u00acF)\"\n  then show False\n  proof (rule notE)\n    show \"F \u2228 \u00acF\"\n    proof (rule disjI2)\n      show \"\u00acF\"\n      proof (rule notI)\n        assume 2: \"F\"\n        then have 3: \"F \u2228 \u00acF\" by (rule disjI1)\n        show False using 1 3 by (rule notE)\n      qed\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_22_2:\n  \"F \u2228 \u00acF\"\nproof (rule ccontr)\n  assume \"\u00ac(F \u2228 \u00acF)\"\n  then show False\n  proof (rule notE)\n    show \"F \u2228 \u00acF\"\n    proof (rule disjI2)\n      show \"\u00acF\"\n      proof (rule notI)\n        assume \"F\"\n        then have \"F \u2228 \u00acF\" ..\n        with \u2039\u00ac(F \u2228 \u00acF)\u203a show False ..\n      qed\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_22_3:\n  \"F \u2228 \u00acF\"\n  by simp \n\nsubsection \u2039Ejemplo 23\u203a\n\ntext \u2039Ejemplo 23 (p. 24). Demostrar\n     p \u27f6 q \u22a2 \u00acp \u2228 q \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_23: \n  \"p \u27f6 q \u27f9 \u00acp \u2228 q\"\n  apply (cut_tac P=\"p\" in excluded_middle)\n  apply (erule disjE)\n   apply (erule disjI1)\n  apply (drule mp)\n   apply assumption\n  apply (erule disjI2)\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_23_1:\n  assumes 1: \"p \u27f6 q\" \n  shows \"\u00acp \u2228 q\"\nproof -\n  have \"\u00acp \u2228 p\" by (rule excluded_middle)\n  then show \"\u00acp \u2228 q\"\n  proof (rule disjE)\n    { assume \"\u00acp\"\n      then show \"\u00acp \u2228 q\" by (rule disjI1) }\n  next\n    { assume 2: \"p\"\n      have \"q\" using 1 2 by (rule mp)\n      then show \"\u00acp \u2228 q\" by (rule disjI2) }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_23_2:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acp \u2228 q\"\nproof -\n  have \"\u00acp \u2228 p\" ..\n  then show \"\u00acp \u2228 q\"\n  proof \n    { assume \"\u00acp\"\n      then show \"\u00acp \u2228 q\" .. }\n  next\n    { assume \"p\"\n      with assms have \"q\" ..\n      then show \"\u00acp \u2228 q\" .. }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_23_3:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acp \u2228 q\"\n  using assms\n  by simp \n\nsection \u2039Demostraciones por contradicci\u00f3n\u203a\n\nsubsection \u2039Ejemplo 24\u203a\n\ntext \u2039Ejemplo 24. Demostrar que \n     \u00acp, p \u2228 q \u22a2 q \u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_24_4: \n  \"\u27e6\u00acp ; p \u2228 q\u27e7 \u27f9 q\"  \n  apply (erule disjE)\n   apply (erule notE)\n   apply assumption+\n  done\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\nlemma ejemplo_24_1:\n  assumes \"\u00acp\"\n          \"p \u2228 q\"\n  shows   \"q\"\nusing \u2039p \u2228 q\u203a\nproof (rule disjE)\n  assume \"p\"\n  with assms(1) show \"q\" by contradiction \nnext\n  assume \"q\"\n  then show \"q\" by assumption\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\nlemma ejemplo_24_2:\n  assumes \"\u00acp\"\n          \"p \u2228 q\"\n  shows \"q\"\nusing \u2039p \u2228 q\u203a\nproof \n  assume \"p\"\n  with assms(1) show \"q\" ..\nnext\n  assume \"q\"\n  then show \"q\" .\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_24_3:\n  assumes \"\u00acp\"\n          \"p \u2228 q\"\n  shows \"q\"\n  using assms\n  by simp \n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha continuado el estudio de la deducci\u00f3n natural en la l\u00f3gica proposicional. Se han estudiado las siguientes reglas: Reglas de la disyunci\u00f3n Regla de copia Reglas de la negaci\u00f3n Reglas del bicondicional Regla del modus tollens Regla de introducci\u00f3n de doble negaci\u00f3n Regla&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[334],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7062"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7062"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7062\/revisions"}],"predecessor-version":[{"id":7064,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7062\/revisions\/7064"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7062"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7062"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7062"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}