{"id":1375,"date":"2011-04-21T19:19:16","date_gmt":"2011-04-21T19:19:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1375"},"modified":"2013-03-28T05:06:38","modified_gmt":"2013-03-28T05:06:38","slug":"dao2011-ejercicios-de-deduccion-natural-en-logica-de-primer-orden-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao2011-ejercicios-de-deduccion-natural-en-logica-de-primer-orden-con-isabellehol\/","title":{"rendered":"DAO2011: Ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO2011\">Demostraci\u00f3n asistida por ordenador<\/a> se han comentado las soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL\/Isar.<\/p>\n<p>A continuaci\u00f3n se muestra la teor\u00eda correspondiente a las soluciones de los ejercicios<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Deducci\u00f3n natural en la l\u00f3gica de primer orden (Ejercicios) *}\r\n\r\ntheory LogicaDePrimerOrdenEj\r\nimports Main \r\nbegin\r\n\r\ntext {* \r\n  Los siguientes ejercicios son los del tema 7 del curso de LI\r\n  demostrado usando las reglas de deducci\u00f3n natural.\r\n*}\r\n\r\ntext {*\r\n  Se usar\u00e1n las reglas del modus tollens y de la introducci\u00f3n de la\r\n  doble negaci\u00f3n.\r\n*}\r\n\r\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\r\nby auto\r\n\r\nlemma notnotI:\r\n  \"P \u27f9 \u00ac\u00acP\"\r\nby auto\r\n\r\nlemma \r\n  assumes \"\u2200x. P x \u27f6 Q x\" \r\n  shows \"(\u2200x. P x) \u27f6 (\u2200x. Q x)\"\r\nproof (rule impI)\r\n  assume 1: \"\u2200x. P x\"\r\n  show \"\u2200x. Q x\"\r\n  proof (rule allI)\r\n    fix x \r\n    have 2: \"P x \u27f6 Q x\" using assms by (rule allE)\r\n    have 3: \"P x\" using 1 by (rule allE)\r\n    show \"Q x\" using 2 3 by (rule mp)\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x. \u00acP x\" \r\n  shows \" \u00ac(\u2200x. P x)\"\r\nproof (rule notI) \r\n  assume 1: \"\u2200x. P x\"\r\n  obtain a where 2: \"\u00acP a\" using assms(1) by (rule exE)\r\n  have 3: \"P a\" using 1 by (rule allE)\r\n  show False using 2 3 by (rule notE)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. P x\" \r\n  shows \"\u2200y. P y\"\r\nproof (rule allI)\r\n  fix a\r\n  show \"P a\" using assms(1) by (rule allE)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. P x \u27f6 Q x\" \r\n  shows \"(\u2200x. \u00acQ x) \u27f6 (\u2200x. \u00acP x)\"\r\nproof (rule impI)\r\n  assume 1: \"\u2200x. \u00acQ x\"\r\n  show \"\u2200x. \u00acP x\"\r\n  proof (rule allI)\r\n    fix x\r\n    have 2: \"P x \u27f6 Q x\" using assms(1) by (rule allE)\r\n    have 3: \"\u00acQ x\" using 1 by (rule allE)\r\n    show \"\u00acP x\" using 2 3 by (rule mt)\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. P x \u27f6 \u00acQ x\" \r\n  shows \"\u00ac(\u2203x. P x \u2227 Q x)\"\r\nproof (rule notI)\r\n  assume \"\u2203x. P x \u2227 Q x\"\r\n  then obtain a where 1: \"P a \u2227 Q a\" by (rule exE)\r\n  have 2: \"P a \u27f6 \u00acQ a\" using assms(1) by (rule allE)\r\n  have 3: \"P a\" using 1 by (rule conjunct1)\r\n  have 4: \"\u00acQ a\" using 2 3 by (rule mp)\r\n  have 5: \"Q a\" using 1 by (rule conjunct2)\r\n  show False using 4 5 by (rule notE)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. \u2200y. P x y\" \r\n  shows \"\u2200u. \u2200v. P u v\"\r\nproof (rule allI)\r\n  fix u\r\n  show \"\u2200v. P u v\"\r\n  proof (rule allI)\r\n    fix v\r\n    have \"\u2200y. P u y\" using assms(1) by (rule allE)\r\n    thus \"P u v\" by (rule allE)\r\n  qed \r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x. \u2203y. P x y\" \r\n  shows \"\u2203u. \u2203v. P u v\"\r\nproof -\r\n  obtain a where \"\u2203y. P a y\" using assms(1) by (rule exE)\r\n  then obtain b where \"P a b\" by (rule exE)\r\n  hence \"\u2203v. P a v\" by (rule exI)\r\n  thus \"\u2203u. \u2203v. P u v\" by (rule exI)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x. \u2200y. P x y\" \r\n  shows \"\u2200y. \u2203x. P x y\"\r\nproof (rule allI)\r\n  fix y\r\n  obtain a where \"\u2200y. P a y\" using assms(1) by (rule exE)\r\n  hence \"P a y\" by (rule allE)\r\n  thus \"\u2203x. P x y\" by (rule exI)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x. P a \u27f6 Q x\" \r\n  shows \"P a \u27f6 (\u2203x. Q x)\"\r\nproof (rule impI)\r\n  assume 1: \"P a\"\r\n  obtain b where \"P a \u27f6 Q b\" using assms(1) by (rule exE)\r\n  hence \"Q b\" using 1 by (rule mp)\r\n  thus \"\u2203x. Q x\" by (rule exI)\r\nqed\r\n\r\nlemma \r\n  assumes \"P a \u27f6 (\u2203x. Q x)\" \r\n  shows \"\u2203x. P a \u27f6 Q x\"\r\nproof -\r\n  have \"\u00acP 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 \"\u00acP a\"\r\n      hence \"P a \u27f6 Q b\" by simp\r\n      thus \"\u2203x. P a \u27f6 Q x\" by (rule exI) }\r\n  next\r\n    { assume \"P a\"\r\n      hence \"\u2203x. Q x\" using assms(1) by simp\r\n      then obtain c where \"Q c\" by (rule exE)\r\n      hence \"P a \u27f6 Q c\" by simp\r\n      thus \"\u2203x. P a \u27f6 Q x\" by (rule exI) }\r\n  qed\r\nqed\r\n\r\nlemma \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 x\r\n  show \"P x \u27f6 Q a\"\r\n  proof\r\n    assume \"P x\"\r\n    hence 1: \"\u2203x. P x\" by (rule exI)\r\n    show \"Q a\" using assms(1) 1 by (rule mp)\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. P x \u27f6 Q a\" \r\n  shows \"\u2203x. P x \u27f6 Q a\"\r\nproof (rule exI)\r\n  show \"P b \u27f6 Q a\" using assms(1) ..\r\nqed\r\n\r\nlemma \r\n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\" \r\n  shows \"\u2200x. P x \u2228 Q x\"\r\nusing assms\r\nproof (rule disjE)\r\n  { assume 1: \"\u2200x. P x\"\r\n    show \"\u2200x. P x \u2228 Q x\"\r\n    proof (rule allI)\r\n      fix x\r\n      have \"P x\" using 1 by (rule allE)\r\n      thus \"P x \u2228 Q x\" by (rule disjI1)\r\n    qed }\r\nnext\r\n  { assume 2: \"\u2200x. Q x\"\r\n    show \"\u2200x. P x \u2228 Q x\"\r\n    proof (rule allI)\r\n      fix x\r\n      have \"Q x\" using 2 by (rule allE)\r\n      thus \"P x \u2228 Q x\" by (rule disjI2)\r\n    qed }\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x. P x \u2227 Q x\" \r\n  shows \"(\u2203x. P x) \u2227 (\u2203x. Q x)\"\r\nproof -\r\n  obtain a where 1: \"P a \u2227 Q a\" using assms(1) by (rule exE)\r\n  hence \"P a\" by (rule conjunct1)\r\n  hence 2: \"\u2203x. P x\" by (rule exI)\r\n  have \"Q a\" using 1 by (rule conjunct2)\r\n  hence 3: \"\u2203x. Q x\" by (rule exI)\r\n  show \"(\u2203x. P x) \u2227 (\u2203x. Q x)\" using 2 3 by (rule conjI)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x.\u2200y. P y \u27f6 Q x\" \r\n  shows \"(\u2203y. P y) \u27f6 (\u2200x. Q x)\"\r\nproof (rule impI)\r\n  assume 1: \"\u2203y. P y\"\r\n  show \"\u2200x. Q x\"\r\n  proof (rule allI)\r\n    fix x\r\n    have 2: \"\u2200y. P y \u27f6 Q x\" using assms by (rule allE)\r\n    obtain b where 3: \"P b\" using 1 by (rule exE)\r\n    have \"P b \u27f6 Q x\" using 2 by (rule allE)\r\n    thus \"Q x\" using 3 by (rule mp)\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u00ac(\u2200x. \u00acP x)\" \r\n  shows \"\u2203x. P x\"\r\nproof (rule ccontr)\r\n  assume 1: \"\u00ac(\u2203x. P x)\"\r\n  have 2: \"\u2200x. \u00acP x\"\r\n  proof\r\n    fix x\r\n    show \"\u00acP x\"\r\n    proof\r\n      assume \"P x\"\r\n      hence 3: \"\u2203x. P x\" by (rule exI)\r\n      show False using 1 3 by (rule notE)\r\n    qed\r\n  qed\r\n  show False using assms(1) 2 by (rule notE)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. \u00acP x\" \r\n  shows \"\u00ac(\u2203x. P x)\"\r\nproof (rule notI)\r\n  assume \"\u2203x. P x\"\r\n  then obtain a where 1: \"P a\" by (rule exE)\r\n  have \"\u00acP a\" using assms(1) by (rule allE)\r\n  thus False using 1 by (rule notE)\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x. P x\" \r\n  shows \"\u00ac(\u2200x. \u00acP x)\"\r\nproof (rule notI)\r\n  assume 1: \"\u2200x. \u00acP x\"\r\n  obtain a where 2: \"P a\" using assms(1) by (rule exE)\r\n  have \"\u00acP a\" using 1 by (rule allE)\r\n  thus False using 2 by (rule notE)\r\nqed\r\n\r\nlemma \r\n  assumes \"P a \u27f6 (\u2200x. Q x)\" \r\n  shows \"\u2200x. P a \u27f6 Q x\"\r\nproof (rule allI)\r\n  fix x\r\n  show \"P a \u27f6 Q x\"\r\n  proof\r\n    assume 1: \"P a\"\r\n    have \"\u2200x. Q x\" using assms(1) 1 by (rule mp)\r\n    thus \"Q x\" by (rule allE)\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x.\u2200y.\u2200z. R x y \u2227 R y z \u27f6 R x z\" and\r\n          \"\u2200x. \u00acR x x\"\r\n  shows \"\u2200x.\u2200y. R x y \u27f6 \u00acR y x\"\r\nproof (rule allI)\r\n  fix x\r\n  show \"\u2200y. R x y \u27f6 \u00acR y x\"\r\n  proof (rule allI)\r\n    fix y\r\n    show \"R x y \u27f6 \u00acR y x\"\r\n    proof (rule impI)\r\n      assume 1: \"R x y\"\r\n      show \"\u00acR y x\"\r\n      proof\r\n        assume 2: \"R y x\"\r\n        have \"\u2200y.\u2200z. R x y \u2227 R y z \u27f6 R x z\" using assms(1) by (rule allE)\r\n        hence \"\u2200z. R x y \u2227 R y z \u27f6 R x z\" by (rule allE)\r\n        hence 3: \"R x y \u2227 R y x \u27f6 R x x\" by (rule allE)\r\n        have 4: \"R x y \u2227 R y x\" using 1 2 by (rule conjI)\r\n        have 5: \"R x x\" using 3 4  by (rule mp)\r\n        have \"\u00acR x x\" using assms(2) by (rule allE)\r\n        thus False using 5 by (rule notE)\r\n      qed\r\n    qed\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. P x \u2228 Q x\" and\r\n          \"\u2203x. \u00acQ x\" and\r\n          \"\u2200x. R x \u27f6 \u00acP x\"\r\n  shows \"\u2203x. \u00acR x\"\r\nproof -\r\n  obtain a where 1: \"\u00acQ a\" using assms(2) ..\r\n  have \"P a \u2228 Q a\" using assms(1) ..\r\n  thus \"\u2203x. \u00acR x\"\r\n  proof (rule disjE)\r\n    { assume \"P a\"\r\n      hence 2: \"\u00ac\u00acP a\" by (rule notnotI)\r\n      have \"R a \u27f6 \u00acP a\" using assms(3) by (rule allE)\r\n      hence \"\u00acR a\" using 2 by (rule mt)\r\n      thus \"\u2203x. \u00acR x\" by (rule exI) }\r\n  next\r\n    { assume 3: \"Q a\"\r\n      show \"\u2203x. \u00acR x\" using 1 3 by (rule notE) }\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2200x. P x \u27f6 Q x \u2228 R x\" and\r\n          \"\u00ac(\u2203x. P x \u2227 R x)\"\r\n  shows \"\u2200x. P x \u27f6 Q x\"\r\nproof\r\n  fix x\r\n  show \"P x \u27f6 Q x\"\r\n  proof\r\n    assume 1: \"P x\"\r\n    have \"P x \u27f6 Q x \u2228 R x\" using assms(1) by (rule allE)\r\n    hence \"Q x \u2228 R x\" using 1 by (rule mp)\r\n    thus \"Q x\"\r\n    proof (rule disjE)\r\n      { assume \"Q x\"\r\n        thus \"Q x\" by this }\r\n    next\r\n      { assume 2: \"R x\"\r\n        have \"P x \u2227 R x\" using 1 2 by (rule conjI)\r\n        hence 3: \"\u2203x. P x \u2227 R x\" by (rule exI)\r\n        show \"Q x\" using assms(2) 3 by (rule notE) }\r\n    qed\r\n  qed\r\nqed\r\n\r\nlemma \r\n  assumes \"\u2203x.\u2203y. R x y \u2228 R y x\" \r\n  shows \"\u2203x.\u2203y. R x 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  thus \"\u2203x.\u2203y. R x y\"\r\n  proof\r\n    { assume \"R a b\"\r\n      hence \"\u2203y. R a y\" by (rule exI)\r\n      thus \"\u2203x.\u2203y. R x y\" by (rule exI) }\r\n  next\r\n    { assume \"R b a\"\r\n      hence \"\u2203y. R b y\" by (rule exI)\r\n      thus \"\u2203x.\u2203y. R x y\" by (rule exI) }\r\n  qed\r\nqed\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Demostraci\u00f3n asistida por ordenador se han comentado las soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL\/Isar. A continuaci\u00f3n se muestra la teor\u00eda correspondiente a las soluciones de los ejercicios<\/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":[165],"tags":[289],"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\/1375"}],"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=1375"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1375\/revisions"}],"predecessor-version":[{"id":3144,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1375\/revisions\/3144"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1375"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1375"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1375"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}