{"id":3217,"date":"2013-04-10T19:52:45","date_gmt":"2013-04-10T19:52:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3217"},"modified":"2013-04-13T10:53:46","modified_gmt":"2013-04-13T10:53:46","slug":"lmf2013-ejercicios-de-deduccion-natural-en-logica-de-primer-orden-con-isabellehol-1","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-ejercicios-de-deduccion-natural-en-logica-de-primer-orden-con-isabellehol-1\/","title":{"rendered":"LMF2013: Ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL (1)"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se han resuelto los ejercicios 10, 11, 12, 13 y 16 de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2013\/index.php5\/Rel_7\">relaci\u00f3n 7<\/a> sobre deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL.<\/p>\n<p>Las soluciones de los ejercicios resueltos se muestran a continuaci\u00f3n:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 10. Demostrar\r\n       P a \u27f6 (\u2203x. Q x) \u22a2 \u2203x. P a \u27f6 Q x \r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_10a: \r\n  \"P a \u27f6 (\u2203x. Q x) \u27f9 \u2203x. P a \u27f6 Q x\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_10b: \r\n  fixes P Q :: \"'b \u21d2 bool\" \r\n  assumes \"P a \u27f6 (\u2203x. Q x)\"\r\n  shows   \"\u2203x. P a \u27f6 Q x\"\r\nproof -\r\n  have \"\u00ac(P a) \u2228 P a\" ..\r\n  thus \"\u2203x. P a \u27f6 Q x\"\r\n  proof \r\n    assume \"\u00ac(P a)\"\r\n    have \"P a \u27f6 Q a\"\r\n    proof\r\n      assume \"P a\"\r\n      with `\u00ac(P a)` show \"Q a\" ..\r\n    qed\r\n    thus \"\u2203x. P a \u27f6 Q x\" ..\r\n  next\r\n    assume \"P a\"\r\n    with assms have \"\u2203x. Q x\" by (rule mp)\r\n    then obtain b where \"Q b\" .. \r\n    have \"P a \u27f6 Q b\"\r\n    proof\r\n      assume \"P a\"\r\n      note `Q b` \r\n      thus \"Q b\" .\r\n    qed\r\n    thus \"\u2203x. P a \u27f6 Q x\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_10c: \r\n  fixes P Q :: \"'b \u21d2 bool\" \r\n  assumes \"P a \u27f6 (\u2203x. Q x)\"\r\n  shows   \"\u2203x. P a \u27f6 Q x\"\r\nproof -\r\n  have \"\u00ac(P a) \u2228 P a\" by (rule excluded_middle)\r\n  thus \"\u2203x. P a \u27f6 Q x\"\r\n  proof (rule disjE)\r\n    assume \"\u00ac(P a)\"\r\n    have \"P a \u27f6 Q a\"\r\n    proof (rule impI)\r\n      assume \"P a\"\r\n      with `\u00ac(P a)` show \"Q a\" by (rule notE)\r\n    qed\r\n    thus \"\u2203x. P a \u27f6 Q x\" by (rule exI)\r\n  next\r\n    assume \"P a\"\r\n    with assms have \"\u2203x. Q x\" by (rule mp)\r\n    then obtain b where \"Q b\" by (rule exE)\r\n    have \"P a \u27f6 Q b\"\r\n    proof (rule impI)\r\n      assume \"P a\"\r\n      note `Q b` \r\n      thus \"Q b\" by this\r\n    qed\r\n    thus \"\u2203x. P a \u27f6 Q x\" by (rule exI)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 11. Demostrar\r\n       (\u2203x. P x) \u27f6 Q a \u22a2 \u2200x. P x \u27f6 Q a\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_11a: \r\n  \"(\u2203x. P x) \u27f6 Q a \u27f9 \u2200x. P x \u27f6 Q a\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_11b: \r\n  assumes \"(\u2203x. P x) \u27f6 Q a\"\r\n  shows   \"\u2200x. P x \u27f6 Q a\"\r\nproof\r\n  fix b\r\n  show \"P b \u27f6 Q a\"\r\n  proof\r\n    assume \"P b\"\r\n    hence \"\u2203x. P x\" ..\r\n    with assms show \"Q a\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_11c: \r\n  assumes \"(\u2203x. P x) \u27f6 Q a\"\r\n  shows   \"\u2200x. P x \u27f6 Q a\"\r\nproof (rule allI)\r\n  fix b\r\n  show \"P b \u27f6 Q a\"\r\n  proof (rule impI)\r\n    assume \"P b\"\r\n    hence \"\u2203x. P x\" by (rule exI)\r\n    with assms show \"Q a\" by (rule mp)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 12. Demostrar\r\n       \u2200x. P x \u27f6 Q a \u22a2 \u2203 x. P x \u27f6 Q a\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_12a: \r\n  \"\u2200x. P x \u27f6 Q a \u27f9 \u2203x. P x \u27f6 Q a\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_12b: \r\n  assumes \"\u2200x. P x \u27f6 Q a\"\r\n  shows   \"\u2203x. P x \u27f6 Q a\"\r\nproof -\r\n  have \"P b \u27f6 Q a\" using assms ..\r\n  thus \"\u2203x. P x \u27f6 Q a\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_12c: \r\n  assumes \"\u2200x. P x \u27f6 Q a\"\r\n  shows   \"\u2203x. P x \u27f6 Q a\"\r\nproof -\r\n  have \"P b \u27f6 Q a\" using assms by (rule allE)\r\n  thus \"\u2203x. P x \u27f6 Q a\" by (rule exI)\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 13. Demostrar\r\n       (\u2200x. P x) \u2228 (\u2200x. Q x) \u22a2 \u2200x. P x \u2228 Q x\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_13a: \r\n  \"(\u2200x. P x) \u2228 (\u2200x. Q x) \u27f9 \u2200x. P x \u2228 Q x\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_13b: \r\n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\"\r\n  shows   \"\u2200x. P x \u2228 Q x\"\r\nproof\r\n  fix a\r\n  note assms\r\n  thus \"P a \u2228 Q a\"\r\n  proof\r\n    assume \"\u2200x. P x\"\r\n    hence \"P a\" ..\r\n    thus \"P a \u2228 Q a\" ..\r\n  next\r\n    assume \"\u2200x. Q x\"\r\n    hence \"Q a\" ..\r\n    thus \"P a \u2228 Q a\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_13c: \r\n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\"\r\n  shows   \"\u2200x. P x \u2228 Q x\"\r\nproof (rule  allI)\r\n  fix a\r\n  note assms\r\n  thus \"P a \u2228 Q a\"\r\n  proof (rule disjE)\r\n    assume \"\u2200x. P x\"\r\n    hence \"P a\" by (rule allE)\r\n    thus \"P a \u2228 Q a\" by (rule disjI1)\r\n  next\r\n    assume \"\u2200x. Q x\"\r\n    hence \"Q a\" by (rule allE)\r\n    thus \"P a \u2228 Q a\" by (rule disjI2)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 16. Demostrar\r\n       \u00ac(\u2200x. \u00ac(P x)) \u22a2 \u2203x. P x\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_16a: \r\n  \"\u00ac(\u2200x. \u00ac(P x)) \u27f9 \u2203x. P x\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_16b: \r\n  assumes \"\u00ac(\u2200x. \u00ac(P x))\"\r\n  shows   \"\u2203x. P x\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(\u2203x. P x)\"\r\n  have \"\u2200x. \u00ac(P x)\"\r\n  proof\r\n    fix a\r\n    show \"\u00ac(P a)\"\r\n    proof\r\n      assume \"P a\"\r\n      hence \"\u2203x. P x\" ..\r\n      with `\u00ac(\u2203x. P x)` show False ..\r\n    qed\r\n  qed\r\n  with assms show False ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_16c: \r\n  assumes \"\u00ac(\u2200x. \u00ac(P x))\"\r\n  shows   \"\u2203x. P x\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(\u2203x. P x)\"\r\n  have \"\u2200x. \u00ac(P x)\"\r\n  proof (rule allI)\r\n    fix a\r\n    show \"\u00ac(P a)\"\r\n    proof\r\n      assume \"P a\"\r\n      hence \"\u2203x. P x\" by (rule exI)\r\n      with `\u00ac(\u2203x. P x)` show False by (rule notE)\r\n    qed\r\n  qed\r\n  with assms show False by (rule notE)\r\nqed\r\n\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se han resuelto los ejercicios 10, 11, 12, 13 y 16 de la relaci\u00f3n 7 sobre deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL. Las soluciones de los ejercicios resueltos se muestran a continuaci\u00f3n:<\/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":[1],"tags":[206,144,202],"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\/3217"}],"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=3217"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3217\/revisions"}],"predecessor-version":[{"id":3218,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3217\/revisions\/3218"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3217"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3217"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3217"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}