{"id":1184,"date":"2011-02-04T09:17:11","date_gmt":"2011-02-04T09:17:11","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1184"},"modified":"2013-03-08T05:50:03","modified_gmt":"2013-03-08T05:50:03","slug":"deduccion-natural-en-logica-de-primer-orden-con-isabelleisar","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/deduccion-natural-en-logica-de-primer-orden-con-isabelleisar\/","title":{"rendered":"Deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/Isar"},"content":{"rendered":"<p>En esta teor\u00eda se presenta la formalizaci\u00f3n en Isabelle\/Isar de los ejemplos del tema de deducci\u00f3n natural en la l\u00f3gica de primer orde siguiendo la presentaci\u00f3n de Huth y Ryan en su libro <a href=\"http:\/\/www.cs.bham.ac.uk\/research\/projects\/lics\">Logic in Computer Science<\/a> y, m\u00e1s concretamente, a la forma como se explica en la asignatura de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-10\">L\u00f3gica inform\u00e1tica<\/a> y que puede verse en  las <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-10\/temas\/tema-7.pdf\">transparencias del tema 7<\/a>.<\/p>\n<p>La p\u00e1ginas en los teorema indican la p\u00e1gina de las anteriores transparencias donde se encuentra la demostraci\u00f3n.<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Deducci\u00f3n natural en la l\u00f3gica de primer orden *}\r\n\r\ntheory LogicaDePrimerOrden\r\nimports Main \r\nbegin\r\n\r\nsection {* Reglas del cuantificador universal *}\r\n\r\ntext {*\r\n  La regla de eliminaci\u00f3n del cuantificador universal es\r\n  \u00b7 allI: \u27e6\u2200x. P x; P x \u27f9 R\u27e7 \u27f9 R\r\n  La regla de introducci\u00f3n del cuantificador universal es\r\n  \u00b7 allE: (\u22c0x. P x) \u27f9 \u2200x. P x\r\n*}\r\n\r\nlemma -- \"p. 10\"\r\n  assumes 1: \"P(c)\" and \r\n          2: \"\u2200x. P(x) \u27f6 \u00acQ(x)\" \r\n  shows \"\u00acQ(c)\"\r\nproof (rule notI)\r\n  assume 3: \"Q(c)\"\r\n  have \"P(c) \u27f6 \u00acQ(c)\" using 2 by (rule allE)\r\n  hence \"\u00acQ(c)\" using 1 by (rule mp)\r\n  thus False using 3 by (rule notE)\r\nqed \r\n\r\nlemma -- \"p. 11\"\r\n  assumes 1: \"\u2200x. P(x) \u27f6 Q(x)\" and  \r\n          2: \"\u2200x. P(x)\" \r\n  shows \"\u2200x. Q(x)\"\r\nproof (rule allI)\r\n  fix x\r\n  have 3: \"P(x) \u27f6 Q(x)\" using 1 by (rule allE)\r\n  have 4: \"P(x)\" using 2 by (rule allE)\r\n  show \"Q(x)\" using 3 4 by (rule mp)\r\nqed\r\n\r\nsection {* Reglas del cuantificador existencial *}\r\n\r\ntext {*\r\n  La regla de eliminaci\u00f3n del cuantificador existencial es\r\n  \u00b7 exI: P x \u27f9 \u2203x. P x\r\n  La regla de introducci\u00f3n del cuantificador existencial es\r\n  \u00b7 exE: \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\r\n*}\r\n\r\nlemma -- \"p. 12\"\r\n  assumes 1: \"\u2200x. P(x)\" \r\n  shows \"\u2203x. P(x)\"\r\nproof -\r\n  have 2: \"P(x)\" using 1 by (rule allE)\r\n  show \"\u2203x. P(x)\" using 2 by (rule exI)\r\nqed\r\n\r\nlemma -- \"p. 12\"\r\n  assumes 1: \"\u2200x. P(x)\" \r\n  shows \"\u2203x. P(x)\"\r\nproof (rule exI) \r\n  show \"P(x)\" using 1 by (rule allE)\r\nqed\r\n\r\nlemma -- \"p. 12\"\r\n  assumes 1: \"\u2200x. P(x)\" \r\n  shows \"\u2203x. P(x)\"\r\nproof \r\n  show \"P(x)\" using 1 ..\r\nqed\r\n\r\nlemma -- \"p. 13\"\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  show \"\u2203x. Q(x)\" using 5 by (rule exI)\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"\u2200x. Q(x) \u27f6 R(x)\" and  \r\n          2: \"\u2203x. P(x) \u2227 Q(x)\" \r\n  shows \"\u2203x. P(x) \u2227 R(x)\"\r\nproof -\r\n  obtain x where 3: \"P(x) \u2227 Q(x)\" using 2 by (rule exE)\r\n  have 5: \"P(x)\" using 3 by (rule conjunct1)\r\n  have 6: \"Q(x) \u27f6 R(x)\" using 1 by (rule allE)\r\n  have 7: \"Q(x)\" using  3 by (rule conjunct2)\r\n  have 8: \"R(x)\" using 6 7 by (rule mp)\r\n  have 9: \"P(x) \u2227 R(x)\" using 5 8 by (rule conjI)\r\n  show \"\u2203x. P(x) \u2227 R(x)\" using 9 by (rule exI)\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"\u2203x. P(x)\" and  \r\n          2: \"\u2200x.\u2200y. P(x) \u27f6 Q(y)\" \r\n  shows \"\u2200y. Q(y)\"\r\nproof (rule allI)\r\n  fix y\r\n  obtain x where 3: \"P(x)\" using 1 by (rule exE)\r\n  have 4: \"\u2200y. P(x) \u27f6 Q(y)\" using 2 by (rule allE)\r\n  have 5: \"P(x) \u27f6 Q(y)\" using 4 by (rule allE)\r\n  show \"Q(y)\" using 5 3 by (rule mp)\r\nqed\r\n\r\nsection {* Equivalencias *}\r\n\r\n-- \"p. 15\"\r\nlemma equivalencia_1a1:\r\n  assumes 1: \"\u00ac(\u2200x. P(x))\"\r\n  shows \"\u2203x. \u00acP(x)\"\r\nproof (rule ccontr)\r\n  assume 2: \"\u00ac(\u2203x. \u00acP(x))\"\r\n  note 1\r\n  thus False\r\n  proof (rule notE)\r\n    show \"\u2200x. P(x)\"\r\n    proof (rule allI)\r\n      fix x\r\n      show \"P(x)\"\r\n      proof (rule ccontr)\r\n        assume 3: \"\u00acP(x)\"\r\n        have 4: \"\u2203x. \u00acP(x)\" using 3 by (rule exI)\r\n        show False using 2 4 by (rule notE)\r\n      qed\r\n    qed\r\n  qed\r\nqed\r\n\r\n-- \"p. 16\"\r\nlemma equivalencia_1a2:\r\n  assumes 1: \"\u2203x. \u00acP(x)\" \r\n  shows \"\u00ac(\u2200x. P(x))\"\r\nproof (rule ccontr)\r\n  assume 2: \"\u00ac\u00ac(\u2200x. P(x))\"\r\n  obtain x where 3: \"\u00acP(x)\" using 1 by (rule exE)\r\n  have 4: \"\u2200x. P(x)\" using 2 by (rule notnotD)\r\n  have 5: \"P(x)\" using 4 by (rule allE)\r\n  show False using 3 5 by (rule notE)\r\nqed\r\n\r\n-- \"p. 17\"\r\ntheorem equivalencia_1a:\r\n  \"(\u00ac(\u2200x. P(x))) = (\u2203x. \u00acP(x))\"\r\nproof (rule iffI)\r\n  { assume \"\u00ac(\u2200x. P x)\"\r\n    thus \"\u2203x. \u00acP x\" by (rule equivalencia_1a1)}\r\nnext\r\n  { assume \"\u2203x. \u00acP x\"\r\n    thus \"\u00ac(\u2200x. P x)\" by (rule equivalencia_1a2) }\r\nqed\r\n\r\n-- \"p. 18\"\r\nlemma equivalencia_3a1:\r\n  assumes 1: \"\u2200x. P(x) \u2227 Q(x)\" \r\n  shows \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\nproof (rule conjI)\r\n  show \"\u2200x. P(x)\"\r\n  proof (rule allI)\r\n    fix x\r\n    have 2: \"P(x) \u2227 Q(x)\" using 1 by (rule allE)\r\n    show \"P(x)\" using 2 by (rule conjunct1) \r\n  qed\r\nnext\r\n  show \"\u2200x. Q(x)\"\r\n  proof (rule allI)\r\n    fix x\r\n    have 3: \"P(x) \u2227 Q(x)\" using 1 by (rule allE)\r\n    show \"Q(x)\" using 3 by (rule conjunct2)\r\n  qed\r\nqed\r\n\r\n-- \"p. 19\"\r\nlemma equivalencia_3a2:\r\n  assumes 1: \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\" \r\n  shows \"\u2200x. P(x) \u2227 Q(x)\"\r\nproof (rule allI)\r\n  fix x\r\n  have 2: \"\u2200x. P(x)\" using 1 by (rule conjunct1)\r\n  have 3: \"\u2200x. Q(x)\" using 1 by (rule conjunct2)\r\n  have 4: \"P(x)\" using 2 by (rule allE)\r\n  have 5: \"Q(x)\" using 3 by (rule allE)\r\n  show \"P(x) \u2227 Q(x)\" using 4 5 by (rule conjI)\r\nqed\r\n\r\n-- \"p. 20\" \r\nlemma equivalencia_3a:\r\n  \"(\u2200x. P(x) \u2227 Q(x)) = ((\u2200x. P(x)) \u2227 (\u2200x. Q(x)))\"\r\nproof (rule iffI)\r\n  { assume \"\u2200x. P(x) \u2227 Q(x)\"\r\n    thus \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\" by (rule equivalencia_3a1) }\r\nnext\r\n  { assume \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\n    thus \"\u2200x. P(x) \u2227 Q(x)\" by (rule equivalencia_3a2) }\r\nqed\r\n\r\n-- \"p. 21\"\r\nlemma equivalencia_3b1: \r\n  assumes 1: \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" \r\n  shows \"\u2203x. P(x) \u2228 Q(x)\"\r\nusing 1\r\nproof (rule disjE)\r\n  { assume \"\u2203x. P(x)\"\r\n    then obtain x where \"P(x)\" by (rule exE)\r\n    hence \"P(x) \u2228 Q(x)\" by (rule disjI1)\r\n    thus \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI) }\r\nnext\r\n  { assume \"\u2203x. Q(x)\"\r\n    then obtain x where \"Q(x)\" by (rule exE)\r\n    hence \"P(x) \u2228 Q(x)\" by (rule disjI2)\r\n    thus \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI) }\r\nqed\r\n\r\n-- \"p. 22\"\r\nlemma equivalencia_3b2:\r\n  assumes 1: \"\u2203x. P(x) \u2228 Q(x)\" \r\n  shows \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\nproof -\r\n  obtain x where 2: \"P(x) \u2228 Q(x)\" using 1 by (rule exE)\r\n  thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\n  proof (rule disjE)\r\n    { assume \"P(x)\"\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(x)\"\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\n-- \"p. 23\"\r\nlemma equivalencia_3b:\r\n  \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) = (\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)\" by (rule equivalencia_3b1) }\r\nnext\r\n  { assume \"\u2203x. P(x) \u2228 Q(x)\"\r\n    thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule equivalencia_3b2) }\r\nqed\r\n\r\n-- \"p. 24\"\r\nlemma equivalencia_4b1:\r\n  assumes 1: \"\u2203x.\u2203y. P x y\" \r\n  shows \"\u2203y.\u2203x. P x y\"\r\nproof -\r\n  obtain x where \"\u2203y. P x y\" using 1 by (rule exE)\r\n  then obtain y where \"P x y\" by (rule exE)\r\n  hence \"\u2203x. P x y\" by (rule exI)\r\n  thus \"\u2203y.\u2203x. P x y\" by (rule exI)\r\nqed\r\n\r\n-- \"p. 25\"\r\ntheorem equivalencia_4b:\r\n  \"(\u2203x.\u2203y. P x y) = (\u2203y.\u2203x. P x y)\"\r\nproof (rule iffI)\r\n  { assume \"\u2203x.\u2203y. P x y\"\r\n    thus \"\u2203y.\u2203x. P x y\" by (rule equivalencia_4b1) }\r\nnext\r\n  {assume \"\u2203y.\u2203x. P x y\"\r\n    thus \"\u2203x.\u2203y. P x y\" by (rule equivalencia_4b1) }\r\nqed\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En esta teor\u00eda se presenta la formalizaci\u00f3n en Isabelle\/Isar de los ejemplos del tema de deducci\u00f3n natural en la l\u00f3gica de primer orde siguiendo la presentaci\u00f3n de Huth y Ryan en su libro Logic in Computer Science y, m\u00e1s concretamente, a la forma como se explica en la asignatura de L\u00f3gica inform\u00e1tica y que puede&#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":[170],"tags":[85,148],"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\/1184"}],"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=1184"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1184\/revisions"}],"predecessor-version":[{"id":2937,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1184\/revisions\/2937"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1184"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1184"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1184"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}