{"id":3195,"date":"2013-04-09T15:38:50","date_gmt":"2013-04-09T15:38:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3195"},"modified":"2013-04-10T05:39:44","modified_gmt":"2013-04-10T05:39:44","slug":"lmf2013-deduccion-natural-en-logica-de-primer-orden","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-deduccion-natural-en-logica-de-primer-orden\/","title":{"rendered":"LMF2013: Deducci\u00f3n natural en l\u00f3gica de primer orden"},"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 ha estudiado la deducci\u00f3n natural en la l\u00f3gica de primer orden.<\/p>\n<p>Las transparencias de estas clases son las del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\/temas\/tema-8.pdf\">tema 8<\/a>.<\/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<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 2: Deducci\u00f3n natural en l\u00f3gica de primer orden *}\r\n\r\ntheory T2\r\nimports Main \r\nbegin\r\n\r\nsection {* Reglas del cuantificador universal *}\r\n\r\ntext {*\r\n  Las reglas del cuantificador universal son\r\n  \u00b7 allE:    \u27e6\u2200x. P x; P a \u27f9 R\u27e7 \u27f9 R\r\n  \u00b7 allI:    (\u22c0x. P x) \u27f9 \u2200x. P x\r\n  *}\r\n\r\ntext {* \r\n  Ejemplo 1 (p. 10). Demostrar que\r\n     P(c), \u2200x. (P(x) \u27f6 \u00acQ(x)) \u22a2 \u00acQ(c)\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_1a: \r\n  assumes 1: \"P(c)\" and\r\n          2: \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\r\n  shows \"\u00acQ(c)\"\r\nproof -\r\n  have 3: \"P(c) \u27f6 \u00acQ(c)\" using 2 by (rule allE)\r\n  show 4: \"\u00acQ(c)\" using 3 1 by (rule mp)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_1b: \r\n  assumes \"P(c)\"\r\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\r\n  shows \"\u00acQ(c)\"\r\nproof -\r\n  have \"P(c) \u27f6 \u00acQ(c)\" using assms(2) ..\r\n  thus \"\u00acQ(c)\" using assms(1) ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_1c: \r\n  assumes \"P(c)\"\r\n          \"\u2200x. (P(x) \u27f6 \u00acQ(x))\"\r\n  shows \"\u00acQ(c)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 2 (p. 11). Demostrar que\r\n     \u2200x. (P x \u27f6 \u00ac(Q x)), \u2200x. P x \u22a2 \u2200x. \u00ac(Q x)\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_2a: \r\n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\r\n          2: \"\u2200x. P x\"\r\n  shows \"\u2200x. \u00ac(Q x)\"\r\nproof -\r\n  { fix a\r\n    have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\r\n    have 4: \"P a\" using 2 by (rule allE)\r\n    have 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) }\r\n  thus \"\u2200x. \u00ac(Q x)\" by (rule allI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada hacia atr\u00e1s es\"\r\nlemma ejemplo_2b: \r\n  assumes 1: \"\u2200x. (P x \u27f6 \u00ac(Q x))\" and\r\n          2: \"\u2200x. P x\"\r\n  shows \"\u2200x. \u00ac(Q x)\"\r\nproof (rule allI)\r\n  fix a\r\n  have 3: \"P a \u27f6 \u00ac(Q a)\" using 1 by (rule allE)\r\n  have 4: \"P a\" using 2 by (rule allE)\r\n  show 5: \"\u00ac(Q a)\" using 3 4 by (rule mp) \r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_2c: \r\n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\r\n          \"\u2200x. P x\"\r\n  shows \"\u2200x. \u00ac(Q x)\"\r\nproof \r\n  fix a\r\n  have \"P a\" using assms(2) ..\r\n  have \"P a \u27f6 \u00ac(Q a)\" using assms(1) ..\r\n  thus \"\u00ac(Q a)\" using `P a` ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_2d: \r\n  assumes \"\u2200x. (P x \u27f6 \u00ac(Q x))\"\r\n          \"\u2200x. P x\"\r\n  shows   \"\u2200x. \u00ac(Q x)\"\r\nusing assms\r\nby auto\r\n\r\nsection {* Reglas del cuantificador existencial *}\r\n\r\ntext {*\r\n  Las reglas del cuantificador existencial son\r\n  \u00b7 exI:     P a \u27f9 \u2203x. P x\r\n  \u00b7 exE:     \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\r\n\r\n  En la regla exE la nueva variable se introduce mediante la declaraci\u00f3n \r\n  \"obtain ... where ... by (rule exE)\" \r\n  *}\r\n\r\ntext {* \r\n  Ejemplo  (p. 12). Demostrar que\r\n     \u2200x. P x \u22a2 \u2203x. P x\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_3a:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof -\r\n  fix a\r\n  have \"P a\" using assms by (rule allE)\r\n  thus \"\u2203x. P x\" by (rule exI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_3b:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof -\r\n  fix a\r\n  have \"P a\" using assms ..\r\n  thus \"\u2203x. P x\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada se puede simplificar\"\r\nlemma ejemplo_3c:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof (rule exI)\r\n  fix a\r\n  show \"P a\" using assms ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada se puede simplificar a\u00fan m\u00e1s\"\r\nlemma ejemplo_3d:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nproof \r\n  fix a\r\n  show \"P a\" using assms ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_3e:\r\n  assumes \"\u2200x. P x\"\r\n  shows \"\u2203x. P x\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 4 (p. 13). Demostrar\r\n     \u2200x. (P x \u27f6 Q x), \u2203x. P x \u22a2 \u2203x. Q x\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_4a:\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  thus 6: \"\u2203x. Q x\" by (rule exI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_4b:\r\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\r\n          \"\u2203x. P x\"\r\n  shows \"\u2203x. Q x\"\r\nproof -\r\n  obtain a where \"P a\" using assms(2) ..\r\n  have \"P a \u27f6 Q a\" using assms(1) ..\r\n  hence \"Q a\" using `P a` ..\r\n  thus \"\u2203x. Q x\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_4c:\r\n  assumes \"\u2200x. (P x \u27f6 Q x)\"\r\n          \"\u2203x. P x\"\r\n  shows \"\u2203x. Q x\"\r\nusing assms\r\nby auto\r\n\r\nsection {* Demostraci\u00f3n de equivalencias *}\r\n\r\ntext {* \r\n  Ejemplo 5.1 (p. 15). Demostrar\r\n     \u00ac\u2200x. P x  \u22a2 \u2203x. \u00ac(P x) *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_5_1a:\r\n  assumes \"\u00ac(\u2200x. P(x))\"\r\n  shows   \"\u2203x. \u00acP(x)\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(\u2203x. \u00acP(x))\"\r\n  have \"\u2200x. P(x)\"\r\n  proof (rule allI)\r\n    fix a\r\n    show \"P(a)\"\r\n    proof (rule ccontr)\r\n      assume \"\u00acP(a)\"\r\n      hence \"\u2203x. \u00acP(x)\" by (rule exI)\r\n      with `\u00ac(\u2203x. \u00acP(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-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_5_1b:\r\n  assumes \"\u00ac(\u2200x. P(x))\"\r\n  shows   \"\u2203x. \u00acP(x)\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(\u2203x. \u00acP(x))\"\r\n  have \"\u2200x. P(x)\"\r\n  proof \r\n    fix a\r\n    show \"P(a)\"\r\n    proof (rule ccontr)\r\n      assume \"\u00acP(a)\"\r\n      hence \"\u2203x. \u00acP(x)\" ..\r\n      with `\u00ac(\u2203x. \u00acP(x))` show False ..\r\n    qed\r\n  qed\r\n  with assms show False ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_5_1c:\r\n  assumes \"\u00ac(\u2200x. P(x))\"\r\n  shows   \"\u2203x. \u00acP(x)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 5.2 (p. 16). Demostrar\r\n     \u2203x. \u00ac(P x)  \u22a2 \u00ac\u2200x. P x *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_5_2a:\r\n  assumes \"\u2203x. \u00acP(x)\"\r\n  shows   \"\u00ac(\u2200x. P(x))\"\r\nproof (rule notI)\r\n  assume \"\u2200x. P(x)\"\r\n  obtain a where \"\u00acP(a)\" using assms by (rule exE)\r\n  have \"P(a)\" using `\u2200x. P(x)` by (rule allE)\r\n  with `\u00acP(a)` show False by (rule notE)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_5_2b:\r\n  assumes \"\u2203x. \u00acP(x)\"\r\n  shows   \"\u00ac(\u2200x. P(x))\"\r\nproof \r\n  assume \"\u2200x. P(x)\"\r\n  obtain a where \"\u00acP(a)\" using assms ..\r\n  have \"P(a)\" using `\u2200x. P(x)` ..\r\n  with `\u00acP(a)` show False ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_5_2c:\r\n  assumes \"\u2203x. \u00acP(x)\"\r\n  shows   \"\u00ac(\u2200x. P(x))\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 5.3 (p. 17). Demostrar\r\n     \u22a2 \u00ac\u2200x. P x  \u27f7 \u2203x. \u00ac(P x) *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_5_3a:\r\n  \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\r\nproof (rule iffI)\r\n  assume \"\u00ac(\u2200x. P(x))\"\r\n  thus \"\u2203x. \u00acP(x)\" by (rule ejemplo_5_1a)\r\nnext\r\n  assume \"\u2203x. \u00acP(x)\"\r\n  thus \"\u00ac(\u2200x. P(x))\" by (rule ejemplo_5_2a)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_5_3b:\r\n  \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 6.1 (p. 18). Demostrar\r\n     \u2200x. P(x) \u2227 Q(x) \u22a2  (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_6_1a:\r\n  assumes \"\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 a\r\n    have \"P(a) \u2227 Q(a)\" using assms by (rule allE)\r\n    thus \"P(a)\" by (rule conjunct1)\r\n  qed\r\nnext\r\n  show \"\u2200x. Q(x)\"\r\n  proof (rule allI)\r\n    fix a\r\n    have \"P(a) \u2227 Q(a)\" using assms by (rule allE)\r\n    thus \"Q(a)\" by (rule conjunct2)\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_6_1b:\r\n  assumes \"\u2200x. P(x) \u2227 Q(x)\"\r\n  shows   \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\nproof \r\n  show \"\u2200x. P(x)\"\r\n  proof \r\n    fix a\r\n    have \"P(a) \u2227 Q(a)\" using assms ..\r\n    thus \"P(a)\" ..\r\n  qed\r\nnext\r\n  show \"\u2200x. Q(x)\"\r\n  proof \r\n    fix a\r\n    have \"P(a) \u2227 Q(a)\" using assms ..\r\n    thus \"Q(a)\" ..\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_6_1c:\r\n  assumes \"\u2200x. P(x) \u2227 Q(x)\"\r\n  shows   \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 6.2 (p. 19). Demostrar\r\n     (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) \u22a2 \u2200x. P(x) \u2227 Q(x)  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_6_2a:\r\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\r\nproof (rule allI)\r\n  fix a\r\n  have \"\u2200x. P(x)\" using assms by (rule conjunct1)\r\n  hence \"P(a)\" by (rule allE)\r\n  have \"\u2200x. Q(x)\" using assms by (rule conjunct2)\r\n  hence \"Q(a)\" by (rule allE)\r\n  with `P(a)` show \"P(a) \u2227 Q(a)\" by (rule conjI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_6_2b:\r\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\r\nproof\r\n  fix a\r\n  have \"\u2200x. P(x)\" using assms ..\r\n  hence \"P(a)\" by (rule allE)\r\n  have \"\u2200x. Q(x)\" using assms ..\r\n  hence \"Q(a)\" ..\r\n  with `P(a)` show \"P(a) \u2227 Q(a)\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_6_2c:\r\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 6.3 (p. 20). Demostrar\r\n     \u22a2 \u2200x. P(x) \u2227 Q(x) \u27f7 (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_6_3a:\r\n  \"(\u2200x. P(x) \u2227 Q(x)) \u27f7 ((\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 ejemplo_6_1a)\r\nnext\r\n  assume \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\r\n  thus \"\u2200x. P(x) \u2227 Q(x)\" by (rule ejemplo_6_2a)\r\nqed\r\n\r\ntext {* \r\n  Ejemplo 7.1 (p. 21). Demostrar\r\n     (\u2203x. P(x)) \u2228 (\u2203x. Q(x)) \u22a2 \u2203x. P(x) \u2228 Q(x)  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_7_1a:\r\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\r\nusing assms\r\nproof (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\nnext\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\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_7_1b:\r\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\r\nusing assms\r\nproof\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\nnext\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\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_7_1c:\r\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 7.2 (p. 22). Demostrar\r\n     \u2203x. P(x) \u2228 Q(x) \u22a2 (\u2203x. P(x)) \u2228 (\u2203x. Q(x))  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_7_2a:\r\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\r\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\nproof -\r\n  obtain a where \"P(a) \u2228 Q(a)\" using assms 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\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_7_2b:\r\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\r\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\nproof -\r\n  obtain a where \"P(a) \u2228 Q(a)\" using assms ..\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 autom\u00e1tica es\"\r\nlemma ejercicio_7_2c:\r\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\r\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 7.3 (p. 23). Demostrar\r\n     \u22a2 ((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_7_3a:\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)\" by (rule ejemplo_7_1a)\r\nnext\r\n  assume \"\u2203x. P(x) \u2228 Q(x)\"\r\n  thus \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule ejemplo_7_2a)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_7_3b:\r\n  \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 8.1 (p. 24). Demostrar\r\n     \u2203x y. P(x,y) \u22a2 \u2203y x. P(x,y)  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_8_1a:\r\n  assumes \"\u2203x y. P(x,y)\"\r\n  shows   \"\u2203y x. P(x,y)\"\r\nproof -\r\n  obtain a where \"\u2203y. P(a,y)\" using assms by (rule exE)\r\n  then obtain b where \"P(a,b)\" by (rule exE)\r\n  hence \"\u2203x. P(x,b)\" by (rule exI)\r\n  thus \"\u2203y x. P(x,y)\" by (rule exI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_8_1b:\r\n  assumes \"\u2203x y. P(x,y)\"\r\n  shows   \"\u2203y x. P(x,y)\"\r\nproof -\r\n  obtain a where \"\u2203y. P(a,y)\" using assms ..\r\n  then obtain b where \"P(a,b)\" ..\r\n  hence \"\u2203x. P(x,b)\" ..\r\n  thus \"\u2203y x. P(x,y)\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_8_1c:\r\n  assumes \"\u2203x y. P(x,y)\"\r\n  shows   \"\u2203y x. P(x,y)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 8.2. Demostrar\r\n     \u2203y x. P(x,y) \u22a2 \u2203x y. P(x,y)  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_8_2a:\r\n  assumes \"\u2203y x. P(x,y)\"\r\n  shows   \"\u2203x y. P(x,y)\"\r\nproof -\r\n  obtain b where \"\u2203x. P(x,b)\" using assms by (rule exE)\r\n  then obtain a where \"P(a,b)\" by (rule exE)\r\n  hence \"\u2203y. P(a,y)\" by (rule exI)\r\n  thus \"\u2203x y. P(x,y)\" by (rule exI)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_8_2b:\r\n  assumes \"\u2203y x. P(x,y)\"\r\n  shows   \"\u2203x y. P(x,y)\"\r\nproof -\r\n  obtain b where \"\u2203x. P(x,b)\" using assms ..\r\n  then obtain a where \"P(a,b)\" ..\r\n  hence \"\u2203y. P(a,y)\" ..\r\n  thus \"\u2203x y. P(x,y)\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_8_2c:\r\n  assumes \"\u2203y x. P(x,y)\"\r\n  shows   \"\u2203x y. P(x,y)\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 8.3 (p. 25). Demostrar\r\n     \u22a2 (\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))  *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_8_3a:\r\n  \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\r\nproof (rule iffI)\r\n  assume \"\u2203x y. P(x,y)\"\r\n  thus \"\u2203y x. P(x,y)\" by (rule ejemplo_8_1a)\r\nnext\r\n  assume \"\u2203y x. P(x,y)\"\r\n  thus \"\u2203x y. P(x,y)\" by (rule ejemplo_8_2a)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_8_3b:\r\n  \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\r\nby auto\r\n\r\nsection {* Reglas de la igualdad *}\r\n\r\ntext {*\r\n  Las reglas b\u00e1sicas de la igualdad son:\r\n  \u00b7 refl:  t = t\r\n  \u00b7 subst: \u27e6s = t; P s\u27e7 \u27f9 P t\r\n*}\r\n\r\ntext {* \r\n  Ejemplo 9 (p. 27). Demostrar\r\n     x+1 = 1+x, x+1 > 1 \u27f6 x+1 > 0 \u22a2 1+x > 1 \u27f6 1+x > 0\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_9a: \r\n  assumes \"x+1 = 1+x\" \r\n          \"x+1 > 1 \u27f6 x+1 > 0\"\r\n  shows   \"1+x > 1 \u27f6 1+x > 0\"\r\nproof -\r\n  show \"1+x > 1 \u27f6 1+x > 0\" using assms by (rule subst)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_9b: \r\n  assumes \"x+1 = 1+x\" \r\n          \"x+1 > 1 \u27f6 x+1 > 0\"\r\n  shows   \"1+x > 1 \u27f6 1+x > 0\"\r\nusing assms \r\nby (rule subst)\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_9c: \r\n  assumes \"x+1 = 1+x\" \r\n          \"x+1 > 1 \u27f6 x+1 > 0\"\r\n  shows   \"1+x > 1 \u27f6 1+x > 0\"\r\nusing assms \r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 10 (p. 27). Demostrar\r\n     x = y, y = z \u22a2 x = z\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_10a:\r\n  assumes \"x = y\" \r\n          \"y = z\"\r\n  shows   \"x = z\"\r\nproof -\r\n  show \"x = z\" using assms(2,1) by (rule subst)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_10b: \r\n  assumes \"x = y\" \r\n          \"y = z\"\r\n  shows   \"x = z\"\r\nusing assms(2,1)\r\nby (rule subst)\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_10c: \r\n  assumes \"x = y\" \r\n          \"y = z\"\r\n  shows   \"x = z\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 11 (p. 28). Demostrar\r\n     s = t \u22a2 t = s\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_11a:\r\n  assumes \"s = t\"\r\n  shows   \"t = s\"\r\nproof -\r\n  have \"s = s\" by (rule refl)\r\n  with assms show \"t = s\" by (rule subst)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_11b:\r\n  assumes \"s = t\"\r\n  shows   \"t = s\"\r\nusing assms\r\nby auto\r\n\r\nend\r\n<\/pre>\n<p>Como tarea se propuso la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2013\/index.php5\/Rel_7\">relaci\u00f3n 7<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado la deducci\u00f3n natural en la l\u00f3gica de primer orden. Las transparencias de estas clases son las del tema 8. A la vez que se presentaba las reglas, se ha comentado su formalizaci\u00f3n en Isabelle\/HOL. La teor\u00eda correspondiente es<\/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,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\/3195"}],"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=3195"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3195\/revisions"}],"predecessor-version":[{"id":3196,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3195\/revisions\/3196"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3195"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3195"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3195"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}