{"id":7103,"date":"2020-03-26T18:04:30","date_gmt":"2020-03-26T17:04:30","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7103"},"modified":"2020-03-31T19:14:21","modified_gmt":"2020-03-31T17:14:21","slug":"lmf2019-deduccion-natural-en-logica-de-primer-orden-2-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-deduccion-natural-en-logica-de-primer-orden-2-2\/","title":{"rendered":"LMF2019: Deducci\u00f3n natural en l\u00f3gica de primer orden (2\/2)"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha completado el estudio del c\u00e1lculo de deducci\u00f3n natural proposional para la l\u00f3gica de primer orden demostrando algunas equivalencias notables y presentando las reglas de la igualdad<\/p>\n<p>La clase se ha dado mediante videoconferencia y el correspondiente v\u00eddeo es<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/Hf4uNUHRDfg\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>Las transparencias de esta clase son las p\u00e1ginas 14 a 29 del <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\/temas\/tema-4.pdf\">tema 4<\/a>.<br \/>\n<iframe src=\"\/\/docs.google.com\/viewer?url=https%3A%2F%2Fwww.cs.us.es%2F%7Ejalonso%2Fcursos%2Flmf-19%2Ftemas%2Ftema-4.pdf&hl=es&embedded=true\" class=\"gde-frame\" style=\"width:100%; height:500px; border: none;\" scrolling=\"no\"><\/iframe>\n<p class=\"gde-text\"><a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\/temas\/tema-4.pdf\" class=\"gde-link\">Descargar (PDF, 168KB)<\/a><\/p><\/p>\n<p>A la vez que se han ido haciendo las demostraciones se ha explicado c\u00f3mo hacerlas en Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 4a: Deducci\u00f3n natural en l\u00f3gica de primer orden\u203a\n\ntheory T4a_Deduccion_natural_en_logica_de_primer_orden\nimports Main \nbegin\n\nchapter \u2039Tema 4a: Deducci\u00f3n natural en l\u00f3gica de primer orden\u203a\n\ntheory T4a_Deduccion_natural_en_logica_de_primer_orden\nimports Main \nbegin\n\nsection \u2039Demostraci\u00f3n de equivalencias\u203a\n\nsubsection \u2039Ejemplo 5.1\u203a\n\ntext \u2039Ejemplo 5.1 (p. 15). Demostrar\n     \u00ac\u2200x. P x  \u22a2 \u2203x. \u00ac(P x)\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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      then have \"\u2203x. \u00acP(x)\" by (rule exI)\n      with \u2039\u00ac(\u2203x. \u00acP(x))\u203a show False by (rule notE)\n    qed\n  qed\n  with assms show False by (rule notE)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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      then have \"\u2203x. \u00acP(x)\" ..\n      with \u2039\u00ac(\u2203x. \u00acP(x))\u203a show False ..\n    qed\n  qed\n  with assms show False ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_5_1c:\n  assumes \"\u00ac(\u2200x. P(x))\"\n  shows   \"\u2203x. \u00acP(x)\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_5_1d: \"\u00ac(\u2200x. P x) \u27f9 \u2203y. \u00acP y\"\n  apply (rule ccontr) (* da \u27e6\u00ac (\u2200x. P x); \u2204y. \u00ac P y\u27e7 \u27f9 False *)\n  apply (erule notE)  (* da \u2204y. \u00ac P y \u27f9 \u2200x. P x *)\n  apply (rule allI)   (* da \u22c0x. \u2204y. \u00ac P y \u27f9 P x *)\n  apply (rule ccontr) (* da \u22c0x. \u27e6\u2204y. \u00ac P y; \u00ac P x\u27e7 \u27f9 False *)\n  apply (erule notE)  (* da \u22c0x. \u00ac P x \u27f9 \u2203y. \u00ac P y *)\n   apply (erule exI)  (* da No subgoals! *)\n  done\n\ntext \u2039\n  Ejemplo 5.2 (p. 16). Demostrar\n     \u2203x. \u00ac(P x)  \u22a2 \u00ac\u2200x. P x\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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 \u2039\u2200x. P(x)\u203a by (rule allE)\n  with \u2039\u00acP(a)\u203a show False by (rule notE)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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 \u2039\u2200x. P(x)\u203a ..\n  with \u2039\u00acP(a)\u203a show False ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_5_2c:\n  assumes \"\u2203x. \u00acP(x)\"\n  shows   \"\u00ac(\u2200x. P(x))\"\n  using assms\n  by auto\n\ntext \u2039 Ejemplo 5.3 (p. 17). Demostrar\n     \u22a2 \u00ac\u2200x. P x  \u27f7 \u2203x. \u00ac(P x)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_5_3a:\n  \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\nproof (rule iffI)\n  assume \"\u00ac(\u2200x. P(x))\"\n  then show \"\u2203x. \u00acP(x)\" by (rule ejemplo_5_1a)\nnext\n  assume \"\u2203x. \u00acP(x)\"\n  then show \"\u00ac(\u2200x. P(x))\" by (rule ejemplo_5_2a)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_5_3b:\n  \"(\u00ac(\u2200x. P(x))) \u27f7 (\u2203x. \u00acP(x))\"\n  by auto\n\ntext \u2039Ejemplo 6.1 (p. 18). Demostrar\n     \u2200x. P(x) \u2227 Q(x) \u22a2  (\u2200x. P(x)) \u2227 (\u2200x. Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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    then show \"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    then show \"Q(a)\" by (rule conjunct2)\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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    then show \"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    then show \"Q(a)\" ..\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_6_1c:\n  assumes \"\u2200x. P(x) \u2227 Q(x)\"\n  shows   \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  using assms\n  by auto\n\ntext \u2039Ejemplo 6.2 (p. 19). Demostrar\n     (\u2200x. P(x)) \u2227 (\u2200x. Q(x)) \u22a2 \u2200x. P(x) \u2227 Q(x)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then have \"P(a)\" by (rule allE)\n  have \"\u2200x. Q(x)\" using assms by (rule conjunct2)\n  then have \"Q(a)\" by (rule allE)\n  with \u2039P(a)\u203a show \"P(a) \u2227 Q(a)\" by (rule conjI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then have \"P(a)\" ..\n  have \"\u2200x. Q(x)\" using assms ..\n  then have \"Q(a)\" ..\n  with \u2039P(a)\u203a show \"P(a) \u2227 Q(a)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_6_2c:\n  assumes \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  shows   \"\u2200x. P(x) \u2227 Q(x)\"\n  using assms\n  by simp\n\ntext \u2039Ejemplo 6.3 (p. 20). Demostrar\n     \u22a2 \u2200x. P(x) \u2227 Q(x) \u27f7 (\u2200x. P(x)) \u2227 (\u2200x. Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then show \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\" by (rule ejemplo_6_1a)\nnext\n  assume \"(\u2200x. P(x)) \u2227 (\u2200x. Q(x))\"\n  then show \"\u2200x. P(x) \u2227 Q(x)\" by (rule ejemplo_6_2a)\nqed\n\nlemma \n  \"(\u2200x. P(x) \u2228 Q(x)) \u27f7 ((\u2200x. P(x)) \u2228 (\u2200x. Q(x)))\"\n  oops\n\ntext \u2039Ejemplo 7.1 (p. 21). Demostrar\n     (\u2203x. P(x)) \u2228 (\u2203x. Q(x)) \u22a2 \u2203x. P(x) \u2228 Q(x)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then have \"P(a) \u2228 Q(a)\" by (rule disjI1)\n  then show \"\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  then have \"P(a) \u2228 Q(a)\" by (rule disjI2)\n  then show \"\u2203x. P(x) \u2228 Q(x)\" by (rule exI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then have \"P(a) \u2228 Q(a)\" ..\n  then show \"\u2203x. P(x) \u2228 Q(x)\" ..\nnext\n  assume \"\u2203x. Q(x)\"\n  then obtain a where \"Q(a)\" ..\n  then have \"P(a) \u2228 Q(a)\" ..\n  then show \"\u2203x. P(x) \u2228 Q(x)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_7_1c:\n  assumes \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  shows   \"\u2203x. P(x) \u2228 Q(x)\"\n  using assms\n  by auto\n\ntext \u2039Ejemplo 7.2 (p. 22). Demostrar\n     \u2203x. P(x) \u2228 Q(x) \u22a2 (\u2203x. P(x)) \u2228 (\u2203x. Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  proof (rule disjE)\n    assume \"P(a)\"\n    then have \"\u2203x. P(x)\" by (rule exI)\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule disjI1)\n  next\n    assume \"Q(a)\"\n    then have \"\u2203x. Q(x)\" by (rule exI)\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule disjI2)\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  proof \n    assume \"P(a)\"\n    then have \"\u2203x. P(x)\" ..\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" ..\n  next\n    assume \"Q(a)\"\n    then have \"\u2203x. Q(x)\" ..\n    then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" ..\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejercicio_7_2c:\n  assumes \"\u2203x. P(x) \u2228 Q(x)\"\n  shows   \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\"\n  using assms\n  by auto\n\ntext \u2039Ejemplo 7.3 (p. 23). Demostrar\n     \u22a2 ((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then show \"\u2203x. P(x) \u2228 Q(x)\" by (rule ejemplo_7_1a)\nnext\n  assume \"\u2203x. P(x) \u2228 Q(x)\"\n  then show \"(\u2203x. P(x)) \u2228 (\u2203x. Q(x))\" by (rule ejemplo_7_2a)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_7_3b:\n  \"((\u2203x. P(x)) \u2228 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2228 Q(x))\"\n  by auto\n\nlemma \n  \"((\u2203x. P(x)) \u2227 (\u2203x. Q(x))) \u27f7 (\u2203x. P(x) \u2227 Q(x))\"\n  oops\n\ntext \u2039Ejemplo 8.1 (p. 24). Demostrar\n     \u2203x y. P(x,y) \u22a2 \u2203y x. P(x,y)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then have \"\u2203x. P(x,b)\" by (rule exI)\n  then show \"\u2203y x. P(x,y)\" by (rule exI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then have \"\u2203x. P(x,b)\" ..\n  then show \"\u2203y x. P(x,y)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_8_1c:\n  assumes \"\u2203x y. P(x,y)\"\n  shows   \"\u2203y x. P(x,y)\"\n  using assms\n  by auto\n\ntext \u2039Ejemplo 8.2. Demostrar\n     \u2203y x. P(x,y) \u22a2 \u2203x y. P(x,y)\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then have \"\u2203y. P(a,y)\" by (rule exI)\n  then show \"\u2203x y. P(x,y)\" by (rule exI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then have \"\u2203y. P(a,y)\" ..\n  then show \"\u2203x y. P(x,y)\" ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_8_2c:\n  assumes \"\u2203y x. P(x,y)\"\n  shows   \"\u2203x y. P(x,y)\"\n  using assms\n  by auto\n\ntext \u2039Ejemplo 8.3 (p. 25). Demostrar\n     \u22a2 (\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then show \"\u2203y x. P(x,y)\" by (rule ejemplo_8_1a)\nnext\n  assume \"\u2203y x. P(x,y)\"\n  then show \"\u2203x y. P(x,y)\" by (rule ejemplo_8_2a)\nqed\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_8_3b:\n  \"(\u2203x y. P(x,y)) \u27f7 (\u2203y x. P(x,y))\"\n  by auto\n\nsection \u2039Reglas de la igualdad\u203a\n\ntext \u2039 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\u203a\n\ntext \u2039Ejemplo 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\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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\"\n  using assms \n  by (rule subst)\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\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\"\n  using assms \n  by auto\n\ntext \u2039Ejemplo 10 (p. 27). Demostrar\n     x = y, y = z \u22a2 x = z\n\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_10b: \n  assumes \"x = y\" \n          \"y = z\"\n  shows   \"x = z\"\n  using assms(2, 1)\n  by (rule subst)\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_10c: \n  assumes \"x = y\" \n          \"y = z\"\n  shows   \"x = z\"\n  using assms\n  by auto\n\ntext \u2039Ejemplo 11 (p. 28). Demostrar\n     s = t \u22a2 t = s\n\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_11b:\n  assumes \"s = t\"\n  shows   \"t = s\"\n  using assms\n  by 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 completado el estudio del c\u00e1lculo de deducci\u00f3n natural proposional para la l\u00f3gica de primer orden demostrando algunas equivalencias notables y presentando las reglas de la igualdad La clase se ha dado mediante videoconferencia y el correspondiente v\u00eddeo es Las transparencias de esta&#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":[334],"tags":[],"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\/7103"}],"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=7103"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7103\/revisions"}],"predecessor-version":[{"id":7116,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7103\/revisions\/7116"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7103"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7103"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7103"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}