tema 8<\/a>.<\/p>\n<<\/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
\n<\/p>\n
\nheader {* Tema 8: Deducci\u00f3n natural en l\u00f3gica de primer orden *}\n\ntheory T8\nimports Main \nbegin\n\nsection {* Demostraci\u00f3n de equivalencias *}\n\ntext {* \n Ejemplo 5.1 (p. 15). Demostrar\n \u00ac\u2200x. P x \u22a2 \u2203x. \u00ac(P x) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_5_1a:\n assumes \"\u00ac(\u2200x. P(x))\"\n shows \"\u2203x. \u00acP(x)\"\nproof (rule ccontr)\n assume \"\u00ac(\u2203x. \u00acP(x))\"\n have \"\u2200x. P(x)\"\n proof (rule allI)\n fix a\n show \"P(a)\"\n proof (rule ccontr)\n assume \"\u00acP(a)\"\n hence \"\u2203x. \u00acP(x)\" by (rule exI)\n with `\u00ac(\u2203x. \u00acP(x))` show False by (rule notE)\n qed\n qed\n with assms show False by (rule notE)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_5_1b:\n assumes \"\u00ac(\u2200x. P(x))\"\n shows \"\u2203x. \u00acP(x)\"\nproof (rule ccontr)\n assume \"\u00ac(\u2203x. \u00acP(x))\"\n have \"\u2200x. P(x)\"\n proof \n fix a\n show \"P(a)\"\n proof (rule ccontr)\n assume \"\u00acP(a)\"\n hence \"\u2203x. \u00acP(x)\" ..\n with `\u00ac(\u2203x. \u00acP(x))` show False ..\n qed\n qed\n with assms show False ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_5_1c:\n assumes \"\u00ac(\u2200x. P(x))\"\n shows \"\u2203x. \u00acP(x)\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 5.2 (p. 16). Demostrar\n \u2203x. \u00ac(P x) \u22a2 \u00ac\u2200x. P x *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_5_2a:\n assumes \"\u2203x. \u00acP(x)\"\n shows \"\u00ac(\u2200x. P(x))\"\nproof (rule notI)\n assume \"\u2200x. P(x)\"\n obtain a where \"\u00acP(a)\" using assms by (rule exE)\n have \"P(a)\" using `\u2200x. P(x)` by (rule allE)\n with `\u00acP(a)` show False by (rule notE)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_5_2b:\n assumes \"\u2203x. \u00acP(x)\"\n shows \"\u00ac(\u2200x. P(x))\"\nproof \n assume \"\u2200x. P(x)\"\n obtain a where \"\u00acP(a)\" using assms ..\n have \"P(a)\" using `\u2200x. P(x)` ..\n with `\u00acP(a)` show False ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_5_2c:\n assumes \"\u2203x. \u00acP(x)\"\n shows \"\u00ac(\u2200x. P(x))\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 5.3 (p. 17). Demostrar\n \u22a2 \u00ac\u2200x. P x \u27f7 \u2203x. \u00ac(P x) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_5_3a:\n \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\nproof (rule iffI)\n assume \"\u00ac(\u2200x. P(x))\"\n thus \"\u2203x. \u00acP(x)\" by (rule ejemplo_5_1a)\nnext\n assume \"\u2203x. \u00acP(x)\"\n thus \"\u00ac(\u2200x. P(x))\" by (rule ejemplo_5_2a)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_5_3b:\n \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\nby auto\n\ntext {* \n Ejemplo 6.1 (p. 18). Demostrar\n \u2200x. P(x) \u2227 Q(x) \u22a2 (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_6_1a:\n assumes \"\u2200x. P(x) \u2227 Q(x)\"\n shows \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\nproof (rule conjI)\n show \"\u2200x. P(x)\"\n proof (rule allI)\n fix a\n have \"P(a) \u2227 Q(a)\" using assms by (rule allE)\n thus \"P(a)\" by (rule conjunct1)\n qed\nnext\n show \"\u2200x. Q(x)\"\n proof (rule allI)\n fix a\n have \"P(a) \u2227 Q(a)\" using assms by (rule allE)\n thus \"Q(a)\" by (rule conjunct2)\n qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_6_1b:\n assumes \"\u2200x. P(x) \u2227 Q(x)\"\n shows \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\nproof \n show \"\u2200x. P(x)\"\n proof \n fix a\n have \"P(a) \u2227 Q(a)\" using assms ..\n thus \"P(a)\" ..\n qed\nnext\n show \"\u2200x. Q(x)\"\n proof \n fix a\n have \"P(a) \u2227 Q(a)\" using assms ..\n thus \"Q(a)\" ..\n qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_6_1c:\n assumes \"\u2200x. P(x) \u2227 Q(x)\"\n shows \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 6.2 (p. 19). Demostrar\n (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) \u22a2 \u2200x. P(x) \u2227 Q(x) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_6_2a:\n assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n shows \"\u2200x. P(x) \u2227 Q(x)\"\nproof (rule allI)\n fix a\n have \"\u2200x. P(x)\" using assms by (rule conjunct1)\n hence \"P(a)\" by (rule allE)\n have \"\u2200x. Q(x)\" using assms by (rule conjunct2)\n hence \"Q(a)\" by (rule allE)\n with `P(a)` show \"P(a) \u2227 Q(a)\" by (rule conjI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_6_2b:\n assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n shows \"\u2200x. P(x) \u2227 Q(x)\"\nproof\n fix a\n have \"\u2200x. P(x)\" using assms ..\n hence \"P(a)\" by (rule allE)\n have \"\u2200x. Q(x)\" using assms ..\n hence \"Q(a)\" ..\n with `P(a)` show \"P(a) \u2227 Q(a)\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_6_2c:\n assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n shows \"\u2200x. P(x) \u2227 Q(x)\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 6.3 (p. 20). Demostrar\n \u22a2 \u2200x. P(x) \u2227 Q(x) \u27f7 (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_6_3a:\n \"(\u2200x. P(x) \u2227 Q(x)) \u27f7 ((\u2200x. P(x)) \u2227 (\u2200x. Q(x)))\"\nproof (rule iffI)\n assume \"\u2200x. P(x) \u2227 Q(x)\"\n thus \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\" by (rule ejemplo_6_1a)\nnext\n assume \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n thus \"\u2200x. P(x) \u2227 Q(x)\" by (rule ejemplo_6_2a)\nqed\n\ntext {* \n Ejemplo 7.1 (p. 21). Demostrar\n (\u2203x. P(x)) \u2228 (\u2203x. Q(x)) \u22a2 \u2203x. P(x) \u2228 Q(x) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_7_1a:\n assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n shows \"\u2203x. P(x) \u2228 Q(x)\"\nusing assms\nproof (rule disjE)\n assume \"\u2203x. P(x)\"\n then obtain a where \"P(a)\" by (rule exE)\n hence \"P(a) \u2228 Q(a)\" by (rule disjI1)\n thus \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI)\nnext\n assume \"\u2203x. Q(x)\"\n then obtain a where \"Q(a)\" by (rule exE)\n hence \"P(a) \u2228 Q(a)\" by (rule disjI2)\n thus \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_7_1b:\n assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n shows \"\u2203x. P(x) \u2228 Q(x)\"\nusing assms\nproof\n assume \"\u2203x. P(x)\"\n then obtain a where \"P(a)\" ..\n hence \"P(a) \u2228 Q(a)\" ..\n thus \"\u2203x. P(x) \u2228 Q(x)\" ..\nnext\n assume \"\u2203x. Q(x)\"\n then obtain a where \"Q(a)\" ..\n hence \"P(a) \u2228 Q(a)\" ..\n thus \"\u2203x. P(x) \u2228 Q(x)\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_7_1c:\n assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n shows \"\u2203x. P(x) \u2228 Q(x)\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 7.2 (p. 22). Demostrar\n \u2203x. P(x) \u2228 Q(x) \u22a2 (\u2203x. P(x)) \u2228 (\u2203x. Q(x)) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_7_2a:\n assumes \"\u2203x. P(x) \u2228 Q(x)\"\n shows \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\nproof -\n obtain a where \"P(a) \u2228 Q(a)\" using assms by (rule exE)\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n proof (rule disjE)\n assume \"P(a)\"\n hence \"\u2203x. P(x)\" by (rule exI)\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule disjI1)\n next\n assume \"Q(a)\"\n hence \"\u2203x. Q(x)\" by (rule exI)\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule disjI2)\n qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_7_2b:\n assumes \"\u2203x. P(x) \u2228 Q(x)\"\n shows \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\nproof -\n obtain a where \"P(a) \u2228 Q(a)\" using assms ..\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n proof \n assume \"P(a)\"\n hence \"\u2203x. P(x)\" ..\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" ..\n next\n assume \"Q(a)\"\n hence \"\u2203x. Q(x)\" ..\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" ..\n qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_7_2c:\n assumes \"\u2203x. P(x) \u2228 Q(x)\"\n shows \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 7.3 (p. 23). Demostrar\n \u22a2 ((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x)) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_7_3a:\n \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\"\nproof (rule iffI)\n assume \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n thus \"\u2203x. P(x) \u2228 Q(x)\" by (rule ejemplo_7_1a)\nnext\n assume \"\u2203x. P(x) \u2228 Q(x)\"\n thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule ejemplo_7_2a)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_7_3b:\n \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 8.1 (p. 24). Demostrar\n \u2203x y. P(x,y) \u22a2 \u2203y x. P(x,y) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_8_1a:\n assumes \"\u2203x y. P(x,y)\"\n shows \"\u2203y x. P(x,y)\"\nproof -\n obtain a where \"\u2203y. P(a,y)\" using assms by (rule exE)\n then obtain b where \"P(a,b)\" by (rule exE)\n hence \"\u2203x. P(x,b)\" by (rule exI)\n thus \"\u2203y x. P(x,y)\" by (rule exI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_8_1b:\n assumes \"\u2203x y. P(x,y)\"\n shows \"\u2203y x. P(x,y)\"\nproof -\n obtain a where \"\u2203y. P(a,y)\" using assms ..\n then obtain b where \"P(a,b)\" ..\n hence \"\u2203x. P(x,b)\" ..\n thus \"\u2203y x. P(x,y)\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_8_1c:\n assumes \"\u2203x y. P(x,y)\"\n shows \"\u2203y x. P(x,y)\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 8.2. Demostrar\n \u2203y x. P(x,y) \u22a2 \u2203x y. P(x,y) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_8_2a:\n assumes \"\u2203y x. P(x,y)\"\n shows \"\u2203x y. P(x,y)\"\nproof -\n obtain b where \"\u2203x. P(x,b)\" using assms by (rule exE)\n then obtain a where \"P(a,b)\" by (rule exE)\n hence \"\u2203y. P(a,y)\" by (rule exI)\n thus \"\u2203x y. P(x,y)\" by (rule exI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_8_2b:\n assumes \"\u2203y x. P(x,y)\"\n shows \"\u2203x y. P(x,y)\"\nproof -\n obtain b where \"\u2203x. P(x,b)\" using assms ..\n then obtain a where \"P(a,b)\" ..\n hence \"\u2203y. P(a,y)\" ..\n thus \"\u2203x y. P(x,y)\" ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_8_2c:\n assumes \"\u2203y x. P(x,y)\"\n shows \"\u2203x y. P(x,y)\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 8.3 (p. 25). Demostrar\n \u22a2 (\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y)) *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_8_3a:\n \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\nproof (rule iffI)\n assume \"\u2203x y. P(x,y)\"\n thus \"\u2203y x. P(x,y)\" by (rule ejemplo_8_1a)\nnext\n assume \"\u2203y x. P(x,y)\"\n thus \"\u2203x y. P(x,y)\" by (rule ejemplo_8_2a)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_8_3b:\n \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\nby auto\n\nsection {* Reglas de la igualdad *}\n\ntext {*\n Las reglas b\u00e1sicas de la igualdad son:\n \u00b7 refl: t = t\n \u00b7 subst: \u27e6s = t; P s\u27e7 \u27f9 P t\n*}\n\ntext {* \n Ejemplo 9 (p. 27). Demostrar\n x+1 = 1+x, x+1 > 1 \u27f6 x+1 > 0 \u22a2 1+x > 1 \u27f6 1+x > 0\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_9a: \n assumes \"x+1 = 1+x\" \n \"x+1 > 1 \u27f6 x+1 > 0\"\n shows \"1+x > 1 \u27f6 1+x > 0\"\nproof -\n show \"1+x > 1 \u27f6 1+x > 0\" using assms by (rule subst)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_9b: \n assumes \"x+1 = 1+x\" \n \"x+1 > 1 \u27f6 x+1 > 0\"\n shows \"1+x > 1 \u27f6 1+x > 0\"\nusing assms \nby (rule subst)\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_9c: \n assumes \"x+1 = 1+x\" \n \"x+1 > 1 \u27f6 x+1 > 0\"\n shows \"1+x > 1 \u27f6 1+x > 0\"\nusing assms \nby auto\n\ntext {* \n Ejemplo 10 (p. 27). Demostrar\n x = y, y = z \u22a2 x = z\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_10a:\n assumes \"x = y\" \n \"y = z\"\n shows \"x = z\"\nproof -\n show \"x = z\" using assms(2,1) by (rule subst)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_10b: \n assumes \"x = y\" \n \"y = z\"\n shows \"x = z\"\nusing assms(2,1)\nby (rule subst)\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_10c: \n assumes \"x = y\" \n \"y = z\"\n shows \"x = z\"\nusing assms\nby auto\n\ntext {* \n Ejemplo 11 (p. 28). Demostrar\n s = t \u22a2 t = s\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_11a:\n assumes \"s = t\"\n shows \"t = s\"\nproof -\n have \"s = s\" by (rule refl)\n with assms show \"t = s\" by (rule subst)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_11b:\n assumes \"s = t\"\n shows \"t = s\"\nusing assms\nby auto\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 estudiado la segunda parte de la deducci\u00f3n natural en la l\u00f3gica de primer orden. En concreto, la demostraci\u00f3n de equivalencias l\u00f3gicas y las reglas de la igualdad < p>Las transparencias de estas clases son las p\u00e1ginas 14 a 29 del tema…<\/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\/4234"}],"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=4234"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4234\/revisions"}],"predecessor-version":[{"id":4284,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4234\/revisions\/4284"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4234"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4234"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4234"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}