{"id":7096,"date":"2020-03-12T17:05:16","date_gmt":"2020-03-12T16:05:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7096"},"modified":"2020-03-26T17:14:05","modified_gmt":"2020-03-26T16:14:05","slug":"lmf2019-deduccion-natural-en-logica-de-primer-orden-1-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-deduccion-natural-en-logica-de-primer-orden-1-2\/","title":{"rendered":"LMF2019: Deducci\u00f3n natural en l\u00f3gica de primer orden (1\/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 presentado la ampliaci\u00f3n del c\u00e1lculo de deducci\u00f3n natural proposional para tratar los cuantificadores.<\/p>\n<p>Las transparencias de esta clase son las p\u00e1ginas 1 a 13 del <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\/temas\/tema-4.pdf\">tema 4<\/a>.<br \/>\n<iframe src=\"\/\/docs.google.com\/viewer?url=https%3A%2F%2Fwww.cs.us.es%2F%7Ejalonso%2Fcursos%2Flmf-19%2Ftemas%2Ftema-4.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=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\/temas\/tema-4.pdf\" class=\"gde-link\">Descargar (PDF, 168KB)<\/a><\/p><\/p>\n<p>A la vez que se han ido haciendo las demostraciones se ha explicado c\u00f3mo hacerlas en Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 4a: Deducci\u00f3n natural en l\u00f3gica de primer orden\u203a\n\ntheory T4a_Deduccion_natural_en_logica_de_primer_orden\nimports Main \nbegin\n\ntext \u2039El objetivo de este tema es presentar la deducci\u00f3n natural en \n  l\u00f3gica de primer orden con Isabelle\/HOL. La presentaci\u00f3n se \n  basa en los ejemplos de tema 4 del curso LMF que se encuentra \n  en http:\/\/goo.gl\/uJj8d (que a su vez se basa en el libro de \n  Huth y Ryan \"Logic in Computer Science\" http:\/\/goo.gl\/qsVpY ). \n\n  La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las \n  transparencias de LMF donde se encuentra la demostraci\u00f3n.\u203a\n\nsection \u2039Reglas del cuantificador universal\u203a\n\ntext \u2039Las reglas del cuantificador universal son\n  \u00b7 allE:    \u27e6\u2200x. P x; P a \u27f9 R\u27e7 \u27f9 R\n  \u00b7 allI:    (\u22c0x. P x) \u27f9 \u2200x. P x\n\u203a\n\nsubsection \u2039Ejemplo 1\u203a\n\ntext \u2039Ejemplo 1 (p. 10). Demostrar que\n     P(c), \u2200x. (P(x) \u27f6 \u00acQ(x)) \u22a2 \u00acQ(c)\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_1a: \n  assumes 1: \"P(c)\" and\n          2: \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\n  shows \"\u00acQ(c)\"\nproof -\n  have 3: \"P(c) \u27f6 \u00acQ(c)\" using 2 by (rule allE)\n  show 4: \"\u00acQ(c)\" using 3 1 by (rule mp)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_1b: \n  assumes \"P(c)\"\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\n  shows \"\u00acQ(c)\"\nproof -\n  have \"P(c) \u27f6 \u00acQ(c)\" using assms(2) ..\n  then show \"\u00acQ(c)\" using assms(1) ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_1c: \n  assumes \"P(c)\"\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\n  shows \"\u00acQ(c)\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_1d: \n  \"\u27e6P(c); \u2200x. (P(x) \u27f6 \u00acQ(x))\u27e7 \u27f9 \u00acQ(c)\"\n  apply (erule allE) (* da \u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c *)\n  apply (erule mp)   (* da P c \u27f9 P c *)\n  apply assumption   (* da No subgoals! *)\n  done\n    \ntext \u2039Explicaciones\n  apply (erule allE) \n  + Objetivo:       \"\u27e6P(c); \u2200x. (P(x) \u27f6 \u00acQ(x))\u27e7 \u27f9 \u00acQ(c)\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"\u00acQ(c)\", \"\u2200x. (P(x) \u27f6 \u00acQ(x))\") y\n                    (\"?R\",    \"\u2200x. ?P x\")\n    es              ?R \/ \u00acQ(c)\n                    ?P x \/ P(x) \u27f6 \u00acQ(x) \n  + Nuevo objetivo: \"\u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c\"\n\n  apply (erule mp)   \n  + Objetivo:       \"\u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c\"\n  + mp:             \"\u27e6?P \u27f6 ?Q; ?P\u27e7 \u27f9 ?Q\"\n  + Unificador de   (\"\u00ac Q c\", \"P ?x \u27f6 \u00ac Q ?x\") y\n                    (\"?Q\",    \"?P \u27f6 ?Q\")\n    es              ?Q \/ \u00ac Q c\n                    ?P \/ P c\n  + Nuevo objetivo: \"P c \u27f9 P c\" \n\u203a\n\nsubsection \u2039Ejemplo 2\u203a\n\ntext \u2039Ejemplo 2 (p. 11). Demostrar que\n     \u2200x. (P x \u27f6 \u00ac(Q x)), \u2200x. P x \u22a2 \u2200x. \u00ac(Q x)\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_2a: \n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\n          2: \"\u2200x. P x\"\n  shows \"\u2200x. \u00ac(Q x)\"\nproof -\n  { fix a\n    have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\n    have 4: \"P a\" using 2 by (rule allE)\n    have 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) }\n  then show \"\u2200x. \u00ac(Q x)\" by (rule allI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada hacia atr\u00e1s es\u203a\nlemma ejemplo_2b: \n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\n          2: \"\u2200x. P x\"\n  shows \"\u2200x. \u00ac(Q x)\"\nproof (rule allI)\n  fix a\n  have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\n  have 4: \"P a\" using 2 by (rule allE)\n  show 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) \nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_2c: \n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\n          \"\u2200x. P x\"\n  shows \"\u2200x. \u00ac(Q x)\"\nproof \n  fix a\n  have \"P a\" using assms(2) ..\n  have \"P a \u27f6 \u00ac(Q a)\" using assms(1) ..\n  then show \"\u00ac(Q a)\" using \u2039P a\u203a ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_2d: \n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\n          \"\u2200x. P x\"\n  shows   \"\u2200x. \u00ac(Q x)\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_2e: \n  \"\u27e6\u2200x. (P x \u27f6 \u00ac(Q x)); \u2200y. P y\u27e7 \u27f9 \u2200z. \u00ac(Q z)\"\n  apply (rule allI)   (* da \u22c0z. \u27e6P (?x2 z) \u27f6 \u00ac Q (?x2 z);\n                                 P (?y4 z)\u27e7\n                                \u27f9 \u00ac Q z*)\n  apply (erule allE)+ (* da \u22c0z. \u27e6P (?x2 z) \u27f6 \u00ac Q (?x2 z);\n                                 P (?y4 z)\u27e7\n                                \u27f9 \u00ac Q z *)\n  apply (erule mp)    (* da \u22c0z. P (?y4 z) \u27f9 P z *)\n  apply assumption    (* da No subgoals! *) \n  done\n\nsection \u2039Reglas del cuantificador existencial\u203a\n\ntext \u2039Las reglas del cuantificador existencial son\n  \u00b7 exI:     P a \u27f9 \u2203x. P x\n  \u00b7 exE:     \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\n\n  En la regla exE la nueva variable se introduce mediante la declaraci\u00f3n \n  \"obtain ... where ... by (rule exE)\" \n\u203a\n\nsubsection \u2039Ejemplo 3\u203a\n\ntext \u2039Ejemplo 3 (p. 12). Demostrar que\n     \u2200x. P x \u22a2 \u2203x. P x\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_3a:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof -\n  fix a\n  have \"P a\" using assms by (rule allE)\n  then show \"\u2203x. P x\" by (rule exI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_3b:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof -\n  fix a\n  have \"P a\" using assms ..\n  then show \"\u2203x. P x\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada se puede simplificar\u203a\nlemma ejemplo_3c:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof (rule exI)\n  fix a\n  show \"P a\" using assms ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada se puede simplificar a\u00fan m\u00e1s\u203a\nlemma ejemplo_3d:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\nproof \n  fix a\n  show \"P a\" using assms ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_3e:\n  assumes \"\u2200x. P x\"\n  shows \"\u2203x. P x\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_3f: \n  \"\u2200x. P x \u27f9 \u2203y. P y\"\n  apply (erule allE) (* da P ?x \u27f9 \u2203y. P y *)\n  apply (erule exI)  (* da No subgoals! *)\n  done\n\nsubsection \u2039Ejemplo 4\u203a\n\ntext \u2039Ejemplo 4 (p. 13). Demostrar\n     \u2200x. (P x \u27f6 Q x), \u2203x. P x \u22a2 \u2203x. Q x\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_4a:\n  assumes 1: \"\u2200x. (P x \u27f6 Q x)\" and\n          2: \"\u2203x. P x\"\n  shows \"\u2203x. Q x\"\nproof -\n  obtain a where 3: \"P a\" using 2 by (rule exE)\n  have 4: \"P a \u27f6 Q a\" using 1 by (rule allE)\n  have 5: \"Q a\" using 4 3 by (rule mp)\n  then show 6: \"\u2203x. Q x\" by (rule exI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_4b:\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\n          \"\u2203x. P x\"\n  shows \"\u2203x. Q x\"\nproof -\n  obtain a where \"P a\" using assms(2) ..\n  have \"P a \u27f6 Q a\" using assms(1) ..\n  then have \"Q a\" using \u2039P a\u203a ..\n  then show \"\u2203x. Q x\" ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_4c:\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\n          \"\u2203x. P x\"\n  shows \"\u2203x. Q x\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_4f: \n  \"\u27e6\u2200x. P x \u27f6 Q x; \u2203y. P y\u27e7 \u27f9 \u2203z. Q z\"\n  apply (erule exE)  (* da \u22c0y. \u27e6\u2200x. P x \u27f6 Q x; P y\u27e7 \u27f9 \u2203z. Q z *)\n  apply (erule allE) (* da \u22c0y. \u27e6P y; P (?x2 y) \u27f6 Q (?x2 y)\u27e7 \u27f9 \u2203z. Q z *)\n  apply (rule exI)   (* da \u22c0y. \u27e6P y; P (?x2 y) \u27f6 Q (?x2 y)\u27e7 \u27f9 Q (?z4 y) *)\n  apply (erule mp)   (* da \u22c0y. P y \u27f9 P (?x2 y) *)\n  apply assumption   (* da No subgoals! *)\n  done\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se presentado la ampliaci\u00f3n del c\u00e1lculo de deducci\u00f3n natural proposional para tratar los cuantificadores. Las transparencias de esta clase son las p\u00e1ginas 1 a 13 del tema 4. A la vez que se han ido haciendo las demostraciones se ha explicado c\u00f3mo hacerlas en&#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\/7096"}],"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=7096"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7096\/revisions"}],"predecessor-version":[{"id":7100,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7096\/revisions\/7100"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7096"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7096"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7096"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}