{"id":3219,"date":"2013-04-12T19:03:40","date_gmt":"2013-04-12T19:03:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3219"},"modified":"2013-04-13T11:04:40","modified_gmt":"2013-04-13T11:04:40","slug":"lmf2013-ejercicios-de-deduccion-natural-en-logica-de-primer-orden-con-isabellehol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-ejercicios-de-deduccion-natural-en-logica-de-primer-orden-con-isabellehol-2\/","title":{"rendered":"LMF2013: Ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL (2)"},"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 22, 27, 28, 29, 32 y 34 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 22. Demostrar\r\n     {\u2200x. P x \u27f6 Q x \u2228 R x, \u00ac(\u2203x. P x \u2227 R x)} \u22a2 \u2200x. P x \u27f6 Q x\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_22a:\r\n  \"\u27e6\u2200x. P x \u27f6 Q x \u2228 R x; \u00ac(\u2203x. P x \u2227 R x)\u27e7 \u27f9 \u2200x. P x \u27f6 Q x\"\r\nby auto \r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_22b:\r\n  assumes \"\u2200x. P x \u27f6 Q x \u2228 R x\" \r\n          \"\u00ac(\u2203x. P x \u2227 R x)\"\r\n  shows   \"\u2200x. P x \u27f6 Q x\"\r\nproof\r\n  fix a\r\n  show \"P a \u27f6 Q a\"\r\n  proof\r\n    assume \"P a\"\r\n    have \"P a \u27f6 Q a \u2228 R a\" using assms(1) ..\r\n    hence \"Q a \u2228 R a\" using `P a` ..\r\n    thus \"Q a\"\r\n    proof\r\n      assume \"Q a\"\r\n      thus \"Q a\" .\r\n    next\r\n      assume \"R a\"\r\n      with `P a` have \"P a \u2227 R a\" ..\r\n      hence \"\u2203x. P x \u2227 R x\" ..\r\n      with assms(2) show \"Q a\" ..\r\n    qed\r\n  qed \r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_22c:\r\n  assumes \"\u2200x. P x \u27f6 Q x \u2228 R x\" \r\n          \"\u00ac(\u2203x. P x \u2227 R x)\"\r\n  shows   \"\u2200x. P x \u27f6 Q x\"\r\nproof (rule allI)\r\n  fix a\r\n  show \"P a \u27f6 Q a\"\r\n  proof (rule impI)\r\n    assume \"P a\"\r\n    have \"P a \u27f6 Q a \u2228 R a\" using assms(1) by (rule allE)\r\n    hence \"Q a \u2228 R a\" using `P a` by (rule mp)\r\n    thus \"Q a\"\r\n    proof (rule disjE)\r\n      assume \"Q a\"\r\n      thus \"Q a\" by this\r\n    next\r\n      assume \"R a\"\r\n      with `P a` have \"P a \u2227 R a\" by (rule conjI)\r\n      hence \"\u2203x. P x \u2227 R x\" by (rule exI)\r\n      with assms(2) show \"Q a\" by (rule notE)\r\n    qed\r\n  qed \r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 27. Demostrar o refutar\r\n       ((\u2200x. P x) \u2228 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2228 Q x)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_27: \"((\u2200x. P x) \u2228 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2228 Q x)\"\r\noops\r\n\r\n(*\r\nAuto Quickcheck found a counterexample:\r\nP = {a\\<^isub>1}\r\nQ = {a\\<^isub>2}\r\n*)\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 28. Demostrar o refutar\r\n       ((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_28a: \r\n  \"((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_28b: \r\n  \"((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\"\r\nproof\r\n  assume \"(\u2203x. P x) \u2228 (\u2203x. Q x)\"\r\n  thus \"\u2203x. P x \u2228 Q x\"\r\n  proof\r\n    assume \"\u2203x. P x\"\r\n    then obtain a where \"P a\" ..\r\n    hence \"P a \u2228 Q a\" ..\r\n    thus \"\u2203x. P x \u2228 Q x\" ..\r\n  next\r\n    assume \"\u2203x. Q x\"\r\n    then obtain a where \"Q a\" ..\r\n    hence \"P a \u2228 Q a\" ..\r\n    thus \"\u2203x. P x \u2228 Q x\" ..\r\n  qed\r\nnext\r\n  assume \"\u2203x. P x \u2228 Q x\"\r\n  then obtain a where \"P a \u2228 Q a\" ..\r\n  thus \"(\u2203x. P x) \u2228 (\u2203x. Q x)\"\r\n  proof\r\n    assume \"P a\"\r\n    hence \"\u2203x. P x\" ..\r\n    thus \"(\u2203x. P x) \u2228 (\u2203x. Q x)\" ..\r\n  next\r\n    assume \"Q a\"\r\n    hence \"\u2203x. Q x\" ..\r\n    thus \"(\u2203x. P x) \u2228 (\u2203x. Q x)\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_28c: \r\n  \"((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\"\r\nproof (rule iffI)\r\n  assume \"(\u2203x. P x) \u2228 (\u2203x. Q x)\"\r\n  thus \"\u2203x. P x \u2228 Q x\"\r\n  proof (rule disjE)\r\n    assume \"\u2203x. P x\"\r\n    then obtain a where \"P a\" by (rule exE)\r\n    hence \"P a \u2228 Q a\" by (rule disjI1)\r\n    thus \"\u2203x. P x \u2228 Q x\" by (rule exI)\r\n  next\r\n    assume \"\u2203x. Q x\"\r\n    then obtain a where \"Q a\" by (rule exE)\r\n    hence \"P a \u2228 Q a\" by (rule disjI2)\r\n    thus \"\u2203x. P x \u2228 Q x\" by (rule exI)\r\n  qed\r\nnext\r\n  assume \"\u2203x. P x \u2228 Q x\"\r\n  then obtain a where \"P a \u2228 Q a\" by (rule exE)\r\n  thus \"(\u2203x. P x) \u2228 (\u2203x. Q x)\"\r\n  proof (rule disjE)\r\n    assume \"P a\"\r\n    hence \"\u2203x. P x\" by (rule exI)\r\n    thus \"(\u2203x. P x) \u2228 (\u2203x. Q x)\" by (rule disjI1)\r\n  next\r\n    assume \"Q a\"\r\n    hence \"\u2203x. Q x\" by (rule exI)\r\n    thus \"(\u2203x. P x) \u2228 (\u2203x. Q x)\" by (rule disjI2)\r\n  qed\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 29. Demostrar o refutar\r\n       (\u2200x. \u2203y. P x y) \u27f6 (\u2203y. \u2200x. P x y)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_29: \r\n  \"(\u2200x. \u2203y. P x y) \u27f6 (\u2203y. \u2200x. P x y)\"\r\nquickcheck\r\n(*\r\nQuickcheck found a counterexample:\r\n\r\nP = (\u03bbx. undefined)(a\\<^isub> := {b}, b := {a})\r\n*)\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 32. Demostrar o refutar\r\n       \u2203x y. R x y \u2228 R y x; \u00ac(\u2203x. R x x)\u27e7 \u27f9 \u2203x y. x \u2260 y\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_32a:\r\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\r\n  assumes \"\u2203x y. R x y \u2228 R y x\"\r\n          \"\u00ac(\u2203x. R x x)\"\r\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\r\nusing assms\r\nby metis\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_32b:\r\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\r\n  assumes \"\u2203x y. R x y \u2228 R y x\"\r\n          \"\u00ac(\u2203x. R x x)\"\r\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\r\nproof -\r\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms(1) ..\r\n  then obtain b where \"R a b \u2228 R b a\" ..\r\n  hence \"a \u2260 b\"\r\n  proof\r\n    assume \"R a b\"\r\n    show \"a \u2260 b\"\r\n    proof\r\n      assume \"a = b\"\r\n      hence \"R b b\" using `R a b` by (rule subst)\r\n      hence \"\u2203x. R x x\" ..\r\n      with assms(2) show False ..\r\n    qed\r\n  next\r\n    assume \"R b a\"\r\n    show \"a \u2260 b\"\r\n    proof\r\n      assume \"a = b\"\r\n      hence \"R a a\" using `R b a` by (rule ssubst)\r\n      hence \"\u2203x. R x x\" ..\r\n      with assms(2) show False ..\r\n    qed\r\n  qed\r\n  hence \"\u2203y. a \u2260 y\" ..\r\n  thus \"\u2203(x::'c) y. x \u2260 y\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_32c:\r\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\r\n  assumes \"\u2203x y. R x y \u2228 R y x\"\r\n          \"\u00ac(\u2203x. R x x)\"\r\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\r\nproof -\r\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms(1) by (rule exE)\r\n  then obtain b where \"R a b \u2228 R b a\" by (rule exE)\r\n  hence \"a \u2260 b\"\r\n  proof (rule disjE)\r\n    assume \"R a b\"\r\n    show \"a \u2260 b\"\r\n    proof (rule notI)\r\n      assume \"a = b\"\r\n      hence \"R b b\" using `R a b` by (rule subst)\r\n      hence \"\u2203x. R x x\" by (rule exI)\r\n      with assms(2) show False by (rule notE)\r\n    qed\r\n  next\r\n    assume \"R b a\"\r\n    show \"a \u2260 b\"\r\n    proof (rule notI)\r\n      assume \"a = b\"\r\n      hence \"R a a\" using `R b a` by (rule ssubst)\r\n      hence \"\u2203x. R x x\" by (rule exI)\r\n      with assms(2) show False by (rule notE)\r\n    qed\r\n  qed\r\n  hence \"\u2203y. a \u2260 y\" by (rule exI)\r\n  thus \"\u2203(x::'c) y. x \u2260 y\" by (rule exI)\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 34. Demostrar o refutar\r\n     {\u2200x. P a x x, \r\n      \u2200x y z. P x y z \u27f6 P (f x) y (f z)\u27e7\r\n     \u22a2 \u2203z. P (f a) z (f (f a))\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_34a:\r\n  \"\u27e6\u2200x. P a x x; \u2200x y z. P x y z \u27f6 P (f x) y (f z)\u27e7\r\n   \u27f9 \u2203z. P (f a) z (f (f a))\"\r\nby metis\r\n\r\n-- \"La demostraci\u00f3n estructura es\"\r\nlemma ejercicio_34b:\r\n  assumes \"\u2200x. P a x x\" \r\n          \"\u2200x y z. P x y z \u27f6 P (f x) y (f z)\"\r\n  shows   \"\u2203z. P (f a) z (f (f a))\"\r\nproof -\r\n  have \"P a (f a) (f a)\" using assms(1) ..\r\n  have \"\u2200y z. P a y z \u27f6 P (f a) y (f z)\" using assms(2) ..\r\n  hence \"\u2200z. P a (f a) z \u27f6 P (f a) (f a) (f z)\" ..\r\n  hence \"P a (f a) (f a) \u27f6 P (f a) (f a) (f (f a))\" ..\r\n  hence \"P (f a) (f a) (f (f a))\" using `P a (f a) (f a)` ..\r\n  thus \"\u2203z. P (f a) z (f (f a))\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_34c:\r\n  assumes \"\u2200x. P a x x\" \r\n          \"\u2200x y z. P x y z \u27f6 P (f x) y (f z)\"\r\n  shows   \"\u2203z. P (f a) z (f (f a))\"\r\nproof -\r\n  have \"P a (f a) (f a)\" using assms(1) by (rule allE)\r\n  have \"\u2200y z. P a y z \u27f6 P (f a) y (f z)\" using assms(2) by (rule allE)\r\n  hence \"\u2200z. P a (f a) z \u27f6 P (f a) (f a) (f z)\" by (rule allE)\r\n  hence \"P a (f a) (f a) \u27f6 P (f a) (f a) (f (f a))\" by (rule allE)\r\n  hence \"P (f a) (f a) (f (f a))\" using `P a (f a) (f a)` by (rule mp)\r\n  thus \"\u2203z. P (f a) z (f (f a))\" by (rule exI)\r\nqed\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 22, 27, 28, 29, 32 y 34 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\/3219"}],"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=3219"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3219\/revisions"}],"predecessor-version":[{"id":3221,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3219\/revisions\/3221"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3219"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3219"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3219"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}