{"id":4223,"date":"2014-03-26T20:44:23","date_gmt":"2014-03-26T19:44:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4223"},"modified":"2014-03-26T20:44:23","modified_gmt":"2014-03-26T19:44:23","slug":"lmf2014-deduccion-natural-en-logica-de-primer-orden","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-deduccion-natural-en-logica-de-primer-orden\/","title":{"rendered":"LMF2014: Deducci\u00f3n natural en l\u00f3gica de primer orden"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-13\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado la primera parte de la deducci\u00f3n natural en la l\u00f3gica de primer orden.<\/p>\n<p>Las transparencias de estas clases son las p\u00e1ginas 1 a 13 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\/temas\/tema-8.pdf\">tema 8<\/a>.<\/p>\n<p>A la vez que se presentaba las reglas, se ha comentado su formalizaci\u00f3n en Isabelle\/HOL. La teor\u00eda correspondiente es<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 8: Deducci\u00f3n natural en l\u00f3gica de primer orden *}\r\n\r\ntheory T8\r\nimports Main \r\nbegin\r\n\r\nsection {* Reglas del cuantificador universal *}\r\n\r\ntext {*\r\n  Las reglas del cuantificador universal son\r\n  \u00b7 allE:    \u27e6\u2200x. P x; P a \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 allI:    (\u22c0x. P x) \u27f9 \u2200x. P x\r\n  *}\r\n\r\ntext {* \r\n  Ejemplo 1 (p. 10). Demostrar que\r\n     P(c), \u2200x. (P(x) \u27f6 \u00acQ(x)) \u22a2 \u00acQ(c)\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_1a: \r\n  assumes 1: \"P(c)\" and\r\n          2: \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\r\n  shows \"\u00acQ(c)\"\r\nproof -\r\n  have 3: \"P(c) \u27f6 \u00acQ(c)\" using 2 by (rule allE)\r\n  show 4: \"\u00acQ(c)\" using 3 1 by (rule mp)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_1b: \r\n  assumes \"P(c)\"\r\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\r\n  shows \"\u00acQ(c)\"\r\nproof -\r\n  have \"P(c) \u27f6 \u00acQ(c)\" using assms(2) ..\r\n  thus \"\u00acQ(c)\" using assms(1) ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_1c: \r\n  assumes \"P(c)\"\r\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\r\n  shows \"\u00acQ(c)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 2 (p. 11). Demostrar que\r\n     \u2200x. (P x \u27f6 \u00ac(Q x)), \u2200x. P x \u22a2 \u2200x. \u00ac(Q x)\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_2a: \r\n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\r\n          2: \"\u2200x. P x\"\r\n  shows \"\u2200x. \u00ac(Q x)\"\r\nproof -\r\n  { fix a\r\n    have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\r\n    have 4: \"P a\" using 2 by (rule allE)\r\n    have 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) }\r\n  thus \"\u2200x. \u00ac(Q x)\" by (rule allI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada hacia atr\u00e1s es\"\r\nlemma ejemplo_2b: \r\n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\r\n          2: \"\u2200x. P x\"\r\n  shows \"\u2200x. \u00ac(Q x)\"\r\nproof (rule allI)\r\n  fix a\r\n  have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\r\n  have 4: \"P a\" using 2 by (rule allE)\r\n  show 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) \r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_2c: \r\n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\r\n          \"\u2200x. P x\"\r\n  shows \"\u2200x. \u00ac(Q x)\"\r\nproof \r\n  fix a\r\n  have \"P a\" using assms(2) ..\r\n  have \"P a \u27f6 \u00ac(Q a)\" using assms(1) ..\r\n  thus \"\u00ac(Q a)\" using `P a` ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_2d: \r\n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\r\n          \"\u2200x. P x\"\r\n  shows   \"\u2200x. \u00ac(Q x)\"\r\nusing assms\r\nby auto\r\n\r\nsection {* Reglas del cuantificador existencial *}\r\n\r\ntext {*\r\n  Las reglas del cuantificador existencial son\r\n  \u00b7 exI:     P a \u27f9 \u2203x. P x\r\n  \u00b7 exE:     \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\r\n\r\n  En la regla exE la nueva variable se introduce mediante la declaraci\u00f3n \r\n  \"obtain ... where ... by (rule exE)\" \r\n  *}\r\n\r\ntext {* \r\n  Ejemplo  (p. 12). Demostrar que\r\n     \u2200x. P x \u22a2 \u2203x. P x\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_3a:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof -\r\n  fix a\r\n  have \"P a\" using assms by (rule allE)\r\n  thus \"\u2203x. P x\" by (rule exI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_3b:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof -\r\n  fix a\r\n  have \"P a\" using assms ..\r\n  thus \"\u2203x. P x\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada se puede simplificar\"\r\nlemma ejemplo_3c:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof (rule exI)\r\n  fix a\r\n  show \"P a\" using assms ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada se puede simplificar a\u00fan m\u00e1s\"\r\nlemma ejemplo_3d:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof \r\n  fix a\r\n  show \"P a\" using assms ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_3e:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 4 (p. 13). Demostrar\r\n     \u2200x. (P x \u27f6 Q x), \u2203x. P x \u22a2 \u2203x. Q x\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_4a:\r\n  assumes 1: \"\u2200x. (P x \u27f6 Q x)\" and\r\n          2: \"\u2203x. P x\"\r\n  shows \"\u2203x. Q x\"\r\nproof -\r\n  obtain a where 3: \"P a\" using 2 by (rule exE)\r\n  have 4: \"P a \u27f6 Q a\" using 1 by (rule allE)\r\n  have 5: \"Q a\" using 4 3 by (rule mp)\r\n  thus 6: \"\u2203x. Q x\" by (rule exI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_4b:\r\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\r\n          \"\u2203x. P x\"\r\n  shows \"\u2203x. Q x\"\r\nproof -\r\n  obtain a where \"P a\" using assms(2) ..\r\n  have \"P a \u27f6 Q a\" using assms(1) ..\r\n  hence \"Q a\" using `P a` ..\r\n  thus \"\u2203x. Q x\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_4c:\r\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\r\n          \"\u2203x. P x\"\r\n  shows \"\u2203x. Q x\"\r\nusing assms\r\nby auto\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado la primera parte de la deducci\u00f3n natural en la l\u00f3gica de primer orden. Las transparencias de estas clases son las p\u00e1ginas 1 a 13 del tema 8. A la vez que se presentaba las reglas, se ha comentado su formalizaci\u00f3n en&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[234],"tags":[144,303,189],"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\/4223"}],"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=4223"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4223\/revisions"}],"predecessor-version":[{"id":4224,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4223\/revisions\/4224"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4223"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4223"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4223"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}