{"id":4835,"date":"2015-03-23T17:30:00","date_gmt":"2015-03-23T16:30:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4835"},"modified":"2015-03-26T17:34:36","modified_gmt":"2015-03-26T16:34:36","slug":"lmf2015-ejercicios-de-deduccion-natural-en-logicade-primer-orden-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2015-ejercicios-de-deduccion-natural-en-logicade-primer-orden-con-isabellehol\/","title":{"rendered":"LMF2015: Ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-14\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se han comentado soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL.<\/p>\n<p>Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la autom\u00e1tica.<\/p>\n<p>La teor\u00eda con la relaci\u00f3n de ejercicios y sus soluciones es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* R4: Deducci\u00f3n natural de primer orden *}\n\ntheory R4\nimports Main \nbegin\n\ntext {*\n  Demostrar o refutar los siguientes lemas usando s\u00f3lo las reglas\n  b\u00e1sicas de deducci\u00f3n natural de la l\u00f3gica proposicional, de los\n  cuantificadores y de la igualdad: \n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \n  \u00b7 notnotD:    \u00ac\u00ac P \u27f9 P\n  \u00b7 mp:         \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \n  \u00b7 impI:       (P \u27f9 Q) \u27f9 P \u27f6 Q\n  \u00b7 disjI1:     P \u27f9 P \u2228 Q\n  \u00b7 disjI2:     Q \u27f9 P \u2228 Q\n  \u00b7 disjE:      \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \n  \u00b7 FalseE:     False \u27f9 P\n  \u00b7 notE:       \u27e6\u00acP; P\u27e7 \u27f9 R\n  \u00b7 notI:       (P \u27f9 False) \u27f9 \u00acP\n  \u00b7 iffI:       \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\n  \u00b7 iffD1:      \u27e6Q = P; Q\u27e7 \u27f9 P \n  \u00b7 iffD2:      \u27e6P = Q; Q\u27e7 \u27f9 P\n  \u00b7 ccontr:     (\u00acP \u27f9 False) \u27f9 P\n\n  \u00b7 allI:       \u27e6\u2200x. P x; P x \u27f9 R\u27e7 \u27f9 R\n  \u00b7 allE:       (\u22c0x. P x) \u27f9 \u2200x. P x\n  \u00b7 exI:        P x \u27f9 \u2203x. P x\n  \u00b7 exE:        \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q\n\n  \u00b7 refl:       t = t\n  \u00b7 subst:      \u27e6s = t; P s\u27e7 \u27f9 P t\n  \u00b7 trans:      \u27e6r = s; s = t\u27e7 \u27f9 r = t\n  \u00b7 sym:        s = t \u27f9 t = s\n  \u00b7 not_sym:    t \u2260 s \u27f9 s \u2260 t\n  \u00b7 ssubst:     \u27e6t = s; P s\u27e7 \u27f9 P t\n  \u00b7 box_equals: \u27e6a = b; a = c; b = d\u27e7 \u27f9 a: = d\n  \u00b7 arg_cong:   x = y \u27f9 f x = f y\n  \u00b7 fun_cong:   f = g \u27f9 f x = g x\n  \u00b7 cong:       \u27e6f = g; x = y\u27e7 \u27f9 f x = g y\n*}\n\ntext {*\n  Se usar\u00e1n las reglas notnotI y mt que demostramos a continuaci\u00f3n.\n  *}\n\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\nby auto\n\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 1. Demostrar\n       \u2200x. P x \u27f6 Q x \u22a2 (\u2200x. P x) \u27f6 (\u2200x. Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_1a: \n  \"\u2200x. P x \u27f6 Q x \u27f9 (\u2200x. P x) \u27f6 (\u2200x. Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_1b: \n  assumes \"\u2200x. P x \u27f6 Q x\"\n  shows   \"(\u2200x. P x) \u27f6 (\u2200x. Q x)\"\nproof\n  assume \"\u2200x. P x\"\n  show \"\u2200x. Q x\"\n  proof\n    fix a\n    have \"P a\" using `\u2200x. P x` ..\n    have \"P a \u27f6 Q a\" using assms(1) ..\n    thus \"Q a\" using `P a` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_1c: \n  assumes \"\u2200x. P x \u27f6 Q x\"\n  shows   \"(\u2200x. P x) \u27f6 (\u2200x. Q x)\"\nproof (rule impI)\n  assume \"\u2200x. P x\"\n  show \"\u2200x. Q x\"\n  proof (rule allI)\n    fix a\n    have \"P a\" using `\u2200x. P x` by (rule allE)\n    have \"P a \u27f6 Q a\" using assms(1) by (rule allE)\n    thus \"Q a\" using `P a` by (rule mp)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 2. Demostrar\n       \u2203x. \u00ac(P x) \u22a2 \u00ac(\u2200x. P x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_2a: \"\u2203x. \u00ac(P x) \u27f9 \u00ac(\u2200x. P x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_2b: \n  assumes \"\u2203x. \u00ac(P x)\"\n  shows   \"\u00ac(\u2200x. P x)\"\nproof\n  assume \"\u2200x. P x\"\n  obtain a where \"\u00ac(P a)\" using assms(1) .. \n  have \"P a\" using `\u2200x. P x` ..\n  with `\u00ac(P a)` show False ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_2c: \n  assumes \"\u2203x. \u00ac(P x)\"\n  shows   \"\u00ac(\u2200x. P x)\"\nproof (rule notI)\n  assume \"\u2200x. P x\"\n  obtain a where \"\u00ac(P a)\" using assms(1) by (rule exE)\n  have \"P a\" using `\u2200x. P x` by (rule allE)\n  with `\u00ac(P a)` show False by (rule notE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 3. Demostrar\n       \u2200x. P x \u22a2 \u2200y. P y\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_3a: \"\u2200x. P x  \u27f9 \u2200y. P y\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_3b: \n  assumes \"\u2200x. P x\"\n  shows   \"\u2200y. P y\"\nproof\n  fix a\n  show \"P a\" using assms ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_3c: \n  assumes \"\u2200x. P x\"\n  shows   \"\u2200y. P y\"\nproof (rule allI)\n  fix a\n  show \"P a\" using assms by (rule allE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 4. Demostrar\n       \u2200x. P x \u27f6 Q x \u22a2 (\u2200x. \u00ac(Q x)) \u27f6 (\u2200x. \u00ac (P x))\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_4a: \n  \"\u2200x. P x \u27f6 Q x \u27f9 (\u2200x. \u00ac(Q x)) \u27f6 (\u2200x. \u00ac (P x))\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_4b: \n  assumes \"\u2200x. P x \u27f6 Q x\"\n  shows   \"(\u2200x. \u00ac(Q x)) \u27f6 (\u2200x. \u00ac (P x))\"\nproof\n  assume \"\u2200x. \u00ac(Q x)\"\n  show \"\u2200x. \u00ac(P x)\"\n  proof\n    fix a\n    show \"\u00ac(P a)\"\n    proof\n      assume \"P a\"\n      have \"P a \u27f6 Q a\" using assms ..\n      hence \"Q a\" using `P a` ..\n      have \"\u00ac(Q a)\" using `\u2200x. \u00ac(Q x)` ..\n      thus False using `Q a` ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_4c: \n  assumes \"\u2200x. P x \u27f6 Q x\"\n  shows   \"(\u2200x. \u00ac(Q x)) \u27f6 (\u2200x. \u00ac (P x))\"\nproof (rule impI)\n  assume \"\u2200x. \u00ac(Q x)\"\n  show \"\u2200x. \u00ac(P x)\"\n  proof (rule allI)\n    fix a\n    show \"\u00ac(P a)\"\n    proof\n      assume \"P a\"\n      have \"P a \u27f6 Q a\" using assms by (rule allE)\n      hence \"Q a\" using `P a` by (rule mp)\n      have \"\u00ac(Q a)\" using `\u2200x. \u00ac(Q x)` by (rule allE) \n      thus False using `Q a` by (rule notE)\n    qed\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 5. Demostrar\n       \u2200x. P x  \u27f6 \u00ac(Q x) \u22a2 \u00ac(\u2203x. P x \u2227 Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_5a: \n  \"\u2200x. P x  \u27f6 \u00ac(Q x) \u27f9 \u00ac(\u2203x. P x \u2227 Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_5b: \n  assumes \"\u2200x. P x  \u27f6 \u00ac(Q x)\"\n  shows   \"\u00ac(\u2203x. P x \u2227 Q x)\"\nproof\n  assume \"\u2203x. P x \u2227 Q x\"\n  then obtain a where \"P a \u2227 Q a\" ..\n  hence \"P a\" ..\n  have \"P a \u27f6 \u00ac(Q a)\" using assms ..\n  hence \"\u00ac(Q a)\" using `P a` ..\n  have \"Q a\" using `P a \u2227 Q a` ..\n  with `\u00ac(Q a)` show False ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_5c: \n  assumes \"\u2200x. P x  \u27f6 \u00ac(Q x)\"\n  shows   \"\u00ac(\u2203x. P x \u2227 Q x)\"\nproof (rule notI)\n  assume \"\u2203x. P x \u2227 Q x\"\n  then obtain a where \"P a \u2227 Q a\" by (rule exE)\n  hence \"P a\" by (rule conjunct1)\n  have \"P a \u27f6 \u00ac(Q a)\" using assms by (rule allE)\n  hence \"\u00ac(Q a)\" using `P a` by (rule mp)\n  have \"Q a\" using `P a \u2227 Q a` by (rule conjunct2)\n  with `\u00ac(Q a)` show False by (rule notE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 6. Demostrar\n       \u2200x y. P x y \u22a2 \u2200u v. P u v\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_6a: \n  \"\u2200x y. P x y \u27f9 \u2200u v. P u v\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_6b: \n  assumes \"\u2200x y. P x y\"\n  shows   \"\u2200u v. P u v\"\nproof \n  fix a \n  show \"\u2200v. P a v\"\n  proof\n    fix b\n    have \"\u2200y. P a y\" using assms .. \n    thus \"P a b\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada simplificada es\"\nlemma ejercicio_6b2: \n  assumes \"\u2200x y. P x y\"\n  shows   \"\u2200u v. P u v\"\nproof (rule allI)+\n  fix a b\n  have \"\u2200y. P a y\" using assms .. \n  thus \"P a b\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_6c: \n  assumes \"\u2200x y. P x y\"\n  shows   \"\u2200u v. P u v\"\nproof (rule allI)+\n  fix a b\n  have \"\u2200y. P a y\" using assms by (rule allE) \n  thus \"P a b\" by (rule allE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 7. Demostrar\n       \u2203x y. P x y \u27f9 \u2203u v. P u v\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_7a: \n  \"\u2203x y. P x y \u27f9 \u2203u v. P u v\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_7b: \n  assumes \"\u2203x y. P x y\"\n  shows   \"\u2203u v. P u v\"\nproof -\n  obtain a where \"\u2203y. P a y\" using assms ..\n  then obtain b where \"P a b\" ..\n  hence \"\u2203v. P a v\" ..\n  thus \"\u2203u v. P u v\" ..\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 8. Demostrar\n       \u2203x. \u2200y. P x y \u22a2 \u2200y. \u2203x. P x y\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_8a: \n  \"\u2203x. \u2200y. P x y \u27f9 \u2200y. \u2203x. P x y\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_8b: \n  assumes \"\u2203x. \u2200y. P x y\"\n  shows   \"\u2200y. \u2203x. P x y\"\nproof\n  fix b\n  obtain a where \"\u2200y. P a y\" using assms ..\n  hence \"P a b\" ..\n  thus \"\u2203x. P x b\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_8c: \n  assumes \"\u2203x. \u2200y. P x y\"\n  shows   \"\u2200y. \u2203x. P x y\"\nproof (rule allI)\n  fix b\n  obtain a where \"\u2200y. P a y\" using assms by (rule exE)\n  hence \"P a b\" by (rule allE)\n  thus \"\u2203x. P x b\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 9. Demostrar\n       \u2203x. P a \u27f6 Q x \u22a2 P a \u27f6 (\u2203x. Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_9a: \n  \"\u2203x. P a \u27f6 Q x \u27f9 P a \u27f6 (\u2203x. Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_9b: \n  assumes \"\u2203x. P a \u27f6 Q x\"\n  shows   \"P a \u27f6 (\u2203x. Q x)\"\nproof\n  assume \"P a\"\n  obtain b where \"P a \u27f6 Q b\" using assms ..\n  hence \"Q b\" using `P a` ..\n  thus \"\u2203x. Q x\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_9c: \n  assumes \"\u2203x. P a \u27f6 Q x\"\n  shows   \"P a \u27f6 (\u2203x. Q x)\"\nproof (rule impI)\n  assume \"P a\"\n  obtain b where \"P a \u27f6 Q b\" using assms by (rule exE)\n  hence \"Q b\" using `P a` by (rule mp)\n  thus \"\u2203x. Q x\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 10. Demostrar\n       P a \u27f6 (\u2203x. Q x) \u22a2 \u2203x. P a \u27f6 Q x \n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_10a: \n  \"P a \u27f6 (\u2203x. Q x) \u27f9 \u2203x. P a \u27f6 Q x\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_10b: \n  fixes P Q :: \"'b \u21d2 bool\" \n  assumes \"P a \u27f6 (\u2203x. Q x)\"\n  shows   \"\u2203x. P a \u27f6 Q x\"\nproof -\n  have \"\u00ac(P a) \u2228 P a\" ..\n  thus \"\u2203x. P a \u27f6 Q x\"\n  proof \n    assume \"\u00ac(P a)\"\n    have \"P a \u27f6 Q a\"\n    proof\n      assume \"P a\"\n      with `\u00ac(P a)` show \"Q a\" ..\n    qed\n    thus \"\u2203x. P a \u27f6 Q x\" ..\n  next\n    assume \"P a\"\n    with assms have \"\u2203x. Q x\" by (rule mp)\n    then obtain b where \"Q b\" .. \n    have \"P a \u27f6 Q b\"\n    proof\n      assume \"P a\"\n      note `Q b` \n      thus \"Q b\" .\n    qed\n    thus \"\u2203x. P a \u27f6 Q x\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_10c: \n  fixes P Q :: \"'b \u21d2 bool\" \n  assumes \"P a \u27f6 (\u2203x. Q x)\"\n  shows   \"\u2203x. P a \u27f6 Q x\"\nproof -\n  have \"\u00ac(P a) \u2228 P a\" by (rule excluded_middle)\n  thus \"\u2203x. P a \u27f6 Q x\"\n  proof (rule disjE)\n    assume \"\u00ac(P a)\"\n    have \"P a \u27f6 Q a\"\n    proof (rule impI)\n      assume \"P a\"\n      with `\u00ac(P a)` show \"Q a\" by (rule notE)\n    qed\n    thus \"\u2203x. P a \u27f6 Q x\" by (rule exI)\n  next\n    assume \"P a\"\n    with assms have \"\u2203x. Q x\" by (rule mp)\n    then obtain b where \"Q b\" by (rule exE)\n    have \"P a \u27f6 Q b\"\n    proof (rule impI)\n      assume \"P a\"\n      note `Q b` \n      thus \"Q b\" by this\n    qed\n    thus \"\u2203x. P a \u27f6 Q x\" by (rule exI)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 11. Demostrar\n       (\u2203x. P x) \u27f6 Q a \u22a2 \u2200x. P x \u27f6 Q a\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_11a: \n  \"(\u2203x. P x) \u27f6 Q a \u27f9 \u2200x. P x \u27f6 Q a\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_11b: \n  assumes \"(\u2203x. P x) \u27f6 Q a\"\n  shows   \"\u2200x. P x \u27f6 Q a\"\nproof\n  fix b\n  show \"P b \u27f6 Q a\"\n  proof\n    assume \"P b\"\n    hence \"\u2203x. P x\" ..\n    with assms show \"Q a\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_11c: \n  assumes \"(\u2203x. P x) \u27f6 Q a\"\n  shows   \"\u2200x. P x \u27f6 Q a\"\nproof (rule allI)\n  fix b\n  show \"P b \u27f6 Q a\"\n  proof (rule impI)\n    assume \"P b\"\n    hence \"\u2203x. P x\" by (rule exI)\n    with assms show \"Q a\" by (rule mp)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 12. Demostrar\n       \u2200x. P x \u27f6 Q a \u22a2 \u2203 x. P x \u27f6 Q a\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_12a: \n  \"\u2200x. P x \u27f6 Q a \u27f9 \u2203x. P x \u27f6 Q a\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_12b: \n  assumes \"\u2200x. P x \u27f6 Q a\"\n  shows   \"\u2203x. P x \u27f6 Q a\"\nproof -\n  have \"P b \u27f6 Q a\" using assms ..\n  thus \"\u2203x. P x \u27f6 Q a\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_12c: \n  assumes \"\u2200x. P x \u27f6 Q a\"\n  shows   \"\u2203x. P x \u27f6 Q a\"\nproof -\n  have \"P b \u27f6 Q a\" using assms by (rule allE)\n  thus \"\u2203x. P x \u27f6 Q a\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 13. Demostrar\n       (\u2200x. P x) \u2228 (\u2200x. Q x) \u22a2 \u2200x. P x \u2228 Q x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_13a: \n  \"(\u2200x. P x) \u2228 (\u2200x. Q x) \u27f9 \u2200x. P x \u2228 Q x\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_13b: \n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\"\n  shows   \"\u2200x. P x \u2228 Q x\"\nproof\n  fix a\n  note assms\n  thus \"P a \u2228 Q a\"\n  proof\n    assume \"\u2200x. P x\"\n    hence \"P a\" ..\n    thus \"P a \u2228 Q a\" ..\n  next\n    assume \"\u2200x. Q x\"\n    hence \"Q a\" ..\n    thus \"P a \u2228 Q a\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_13c: \n  assumes \"(\u2200x. P x) \u2228 (\u2200x. Q x)\"\n  shows   \"\u2200x. P x \u2228 Q x\"\nproof (rule  allI)\n  fix a\n  note assms\n  thus \"P a \u2228 Q a\"\n  proof (rule disjE)\n    assume \"\u2200x. P x\"\n    hence \"P a\" by (rule allE)\n    thus \"P a \u2228 Q a\" by (rule disjI1)\n  next\n    assume \"\u2200x. Q x\"\n    hence \"Q a\" by (rule allE)\n    thus \"P a \u2228 Q a\" by (rule disjI2)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 14. Demostrar\n       \u2203x. P x \u2227 Q x \u22a2 (\u2203x. P x) \u2227 (\u2203x. Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_14a: \n  \"\u2203x. P x \u2227 Q x \u27f9 (\u2203x. P x) \u2227 (\u2203x. Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_14b: \n  assumes \"\u2203x. P x \u2227 Q x\"\n  shows   \"(\u2203x. P x) \u2227 (\u2203x. Q x)\"\nproof\n  obtain a where \"P a \u2227 Q a\" using assms ..\n  hence \"P a\" ..\n  thus \"\u2203x. P x\" ..\nnext\n  obtain a where \"P a \u2227 Q a\" using assms ..\n  hence \"Q a\" ..\n  thus \"\u2203x. Q x\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_14c: \n  assumes \"\u2203x. P x \u2227 Q x\"\n  shows   \"(\u2203x. P x) \u2227 (\u2203x. Q x)\"\nproof (rule conjI)\n  obtain a where \"P a \u2227 Q a\" using assms by (rule exE)\n  hence \"P a\" by (rule conjunct1)\n  thus \"\u2203x. P x\" by (rule exI)\nnext\n  obtain a where \"P a \u2227 Q a\" using assms by (rule exE)\n  hence \"Q a\" by (rule conjunct2)\n  thus \"\u2203x. Q x\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 15. Demostrar\n       \u2200x y. P y \u27f6 Q x \u22a2 (\u2203y. P y) \u27f6 (\u2200x. Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_15a: \n  \"\u2200x y. P y \u27f6 Q x \u27f9 (\u2203y. P y) \u27f6 (\u2200x. Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_15b: \n  assumes \"\u2200x y. P y \u27f6 Q x\"\n  shows   \"(\u2203y. P y) \u27f6 (\u2200x. Q x)\"\nproof\n  assume \"\u2203y. P y\"\n  then obtain b where \"P b\" ..\n  show \"\u2200x. Q x\"\n  proof\n    fix a\n    have \"\u2200y. P y \u27f6 Q a\" using assms ..\n    hence \"P b \u27f6 Q a\" ..\n    thus \"Q a\" using `P b` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_15c: \n  assumes \"\u2200x y. P y \u27f6 Q x\"\n  shows   \"(\u2203y. P y) \u27f6 (\u2200x. Q x)\"\nproof (rule impI)\n  assume \"\u2203y. P y\"\n  then obtain b where \"P b\" by (rule exE)\n  show \"\u2200x. Q x\"\n  proof (rule allI)\n    fix a\n    have \"\u2200y. P y \u27f6 Q a\" using assms by (rule allE)\n    hence \"P b \u27f6 Q a\" by (rule allE)\n    thus \"Q a\" using `P b` by (rule mp)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 16. Demostrar\n       \u00ac(\u2200x. \u00ac(P x)) \u22a2 \u2203x. P x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_16a: \n  \"\u00ac(\u2200x. \u00ac(P x)) \u27f9 \u2203x. P x\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_16b: \n  assumes \"\u00ac(\u2200x. \u00ac(P x))\"\n  shows   \"\u2203x. P x\"\nproof (rule ccontr)\n  assume \"\u00ac(\u2203x. P x)\"\n  have \"\u2200x. \u00ac(P x)\"\n  proof\n    fix a\n    show \"\u00ac(P a)\"\n    proof\n      assume \"P a\"\n      hence \"\u2203x. P x\" ..\n      with `\u00ac(\u2203x. P x)` show False ..\n    qed\n  qed\n  with assms show False ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_16c: \n  assumes \"\u00ac(\u2200x. \u00ac(P x))\"\n  shows   \"\u2203x. P x\"\nproof (rule ccontr)\n  assume \"\u00ac(\u2203x. P x)\"\n  have \"\u2200x. \u00ac(P x)\"\n  proof (rule allI)\n    fix a\n    show \"\u00ac(P a)\"\n    proof\n      assume \"P a\"\n      hence \"\u2203x. P x\" by (rule exI)\n      with `\u00ac(\u2203x. P x)` show False by (rule notE)\n    qed\n  qed\n  with assms show False by (rule notE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 17. Demostrar\n       \u2200x. \u00ac(P x) \u22a2 \u00ac(\u2203x. P x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_17a: \n  \"\u2200x. \u00ac(P x) \u27f9 \u00ac(\u2203x. P x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_17b: \n  assumes \"\u2200x. \u00ac(P x)\"\n  shows   \"\u00ac(\u2203x. P x)\"\nproof\n  assume \"\u2203x. P x\"\n  then obtain a where \"P a\" ..\n  have \"\u00ac(P a)\" using assms ..\n  thus False using `P a` ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_17c: \n  assumes \"\u2200x. \u00ac(P x)\"\n  shows   \"\u00ac(\u2203x. P x)\"\nproof (rule notI)\n  assume \"\u2203x. P x\"\n  then obtain a where \"P a\" by (rule exE)\n  have \"\u00ac(P a)\" using assms by (rule allE)\n  thus False using `P a` by (rule notE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 18. Demostrar\n       \u2203x. P x \u22a2 \u00ac(\u2200x. \u00ac(P x))\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_18a: \n  \"\u2203x. P x \u27f9 \u00ac(\u2200x. \u00ac(P x))\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_18b: \n  assumes \"\u2203x. P x\"\n  shows   \"\u00ac(\u2200x. \u00ac(P x))\"\nproof\n  assume \"\u2200x. \u00ac(P x)\"\n  obtain a where \"P a\" using assms ..\n  have \"\u00ac(P a)\" using `\u2200x. \u00ac(P x)` ..\n  thus False using `P a` ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_18c: \n  assumes \"\u2203x. P x\"\n  shows   \"\u00ac(\u2200x. \u00ac(P x))\"\nproof (rule notI)\n  assume \"\u2200x. \u00ac(P x)\"\n  obtain a where \"P a\" using assms by (rule exE)\n  have \"\u00ac(P a)\" using `\u2200x. \u00ac(P x)` by (rule allE)\n  thus False using `P a` by (rule notE)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 19. Demostrar\n       P a \u27f6 (\u2200x. Q x) \u22a2 \u2200x. P a \u27f6 Q x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_19a:\n  \"P a \u27f6 (\u2200x. Q x) \u27f9 \u2200x. P a \u27f6 Q x\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_19b: \n  assumes \"P a \u27f6 (\u2200x. Q x)\"\n  shows   \"\u2200x. P a \u27f6 Q x\"\nproof\n  fix b\n  show \"P a \u27f6 Q b\"\n  proof\n    assume \"P a\"\n    with assms have \"\u2200x. Q x\" ..\n    thus \"Q b\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_19c: \n  assumes \"P a \u27f6 (\u2200x. Q x)\"\n  shows   \"\u2200x. P a \u27f6 Q x\"\nproof (rule allI)\n  fix b\n  show \"P a \u27f6 Q b\"\n  proof (rule impI)\n    assume \"P a\"\n    with assms have \"\u2200x. Q x\" by (rule mp)\n    thus \"Q b\" by (rule allE)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 20. Demostrar\n       {\u2200x y z. R x y \u2227 R y z \u27f6 R x z, \n        \u2200x. \u00ac(R x x)}\n       \u22a2 \u2200x y. R x y \u27f6 \u00ac(R y x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_20a: \n  \"\u27e6\u2200x y z. R x y \u2227 R y z \u27f6 R x z; \u2200x. \u00ac(R x x)\u27e7 \u27f9 \u2200x y. R x y \u27f6 \u00ac(R y x)\"\nby metis\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_20b: \n  assumes \"\u2200x y z. R x y \u2227 R y z \u27f6 R x z\"\n          \"\u2200x. \u00ac(R x x)\" \n  shows   \"\u2200x y. R x y \u27f6 \u00ac(R y x)\"\nproof (rule allI)+\n  fix a b\n  show \"R a b \u27f6 \u00ac(R b a)\"\n  proof\n    assume \"R a b\"\n    show \"\u00ac(R b a)\"\n    proof \n      assume \"R b a\"\n      show False\n      proof -\n        have \"R a b \u2227 R b a\" using `R a b` `R b a` ..\n        have \"\u2200y z. R a y \u2227 R y z \u27f6 R a z\" using assms(1) ..\n        hence \"\u2200z. R a b \u2227 R b z \u27f6 R a z\" ..\n        hence \"R a b \u2227 R b a \u27f6 R a a\" ..\n        hence \"R a a\" using `R a b \u2227 R b a` ..\n        have \"\u00ac(R a a)\" using assms(2) ..\n        thus False using `R a a` ..\n      qed\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_20c: \n  assumes \"\u2200x y z. R x y \u2227 R y z \u27f6 R x z\"\n          \"\u2200x. \u00ac(R x x)\" \n  shows   \"\u2200x y. R x y \u27f6 \u00ac(R y x)\"\nproof (rule allI)+\n  fix a b\n  show \"R a b \u27f6 \u00ac(R b a)\"\n  proof (rule impI)\n    assume \"R a b\"\n    show \"\u00ac(R b a)\"\n    proof (rule notI)\n      assume \"R b a\"\n      show False\n      proof -\n        have \"R a b \u2227 R b a\" using `R a b` `R b a` by (rule conjI)\n        have \"\u2200y z. R a y \u2227 R y z \u27f6 R a z\" using assms(1) by (rule allE)\n        hence \"\u2200z. R a b \u2227 R b z \u27f6 R a z\" by (rule allE)\n        hence \"R a b \u2227 R b a \u27f6 R a a\" by (rule allE)\n        hence \"R a a\" using `R a b \u2227 R b a` by (rule mp)\n        have \"\u00ac(R a a)\" using assms(2) by (rule allE)\n        thus False using `R a a` by (rule notE)\n      qed\n    qed\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 21. Demostrar\n     {\u2200x. P x \u2228 Q x, \u2203x. \u00ac(Q x), \u2200x. R x \u27f6 \u00ac(P x)} \u22a2 \u2203x. \u00ac(R x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_21a:\n  \"\u27e6\u2200x. P x \u2228 Q x; \u2203x. \u00ac(Q x); \u2200x. R x \u27f6 \u00ac(P x)\u27e7 \u27f9 \u2203x. \u00ac(R x)\" \nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_21b:\n  assumes \"\u2200x. P x \u2228 Q x\" \n          \"\u2203x. \u00ac(Q x)\" \n          \"\u2200x. R x \u27f6 \u00ac(P x)\"\n  shows   \"\u2203x. \u00ac(R x)\" \nproof -\n  obtain a where \"\u00ac(Q a)\" using assms(2) ..\n  have \"P a \u2228 Q a\" using assms(1) ..\n  hence \"P a\"\n  proof\n    assume \"P a\"\n    thus \"P a\" .\n  next\n    assume \"Q a\"\n    with `\u00ac(Q a)` show \"P a\" ..\n  qed\n  hence \"\u00ac\u00ac(P a)\" by (rule notnotI)\n  have \"R a \u27f6 \u00ac(P a)\" using assms(3) ..\n  hence \"\u00ac(R a)\" using `\u00ac\u00ac(P a)` by (rule mt)\n  thus \"\u2203x. \u00ac(R x)\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_21c:\n  assumes \"\u2200x. P x \u2228 Q x\" \n          \"\u2203x. \u00ac(Q x)\" \n          \"\u2200x. R x \u27f6 \u00ac(P x)\"\n  shows   \"\u2203x. \u00ac(R x)\" \nproof -\n  obtain a where \"\u00ac(Q a)\" using assms(2) by (rule exE)\n  have \"P a \u2228 Q a\" using assms(1) by (rule allE)\n  hence \"P a\"\n  proof (rule disjE)\n    assume \"P a\"\n    thus \"P a\" by this\n  next\n    assume \"Q a\"\n    with `\u00ac(Q a)` show \"P a\" by (rule notE)\n  qed\n  hence \"\u00ac\u00ac(P a)\" by (rule notnotI)\n  have \"R a \u27f6 \u00ac(P a)\" using assms(3) by (rule allE)\n  hence \"\u00ac(R a)\" using `\u00ac\u00ac(P a)` by (rule mt)\n  thus \"\u2203x. \u00ac(R x)\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 22. Demostrar\n     {\u2200x. P x \u27f6 Q x \u2228 R x, \u00ac(\u2203x. P x \u2227 R x)} \u22a2 \u2200x. P x \u27f6 Q x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_22a:\n  \"\u27e6\u2200x. P x \u27f6 Q x \u2228 R x; \u00ac(\u2203x. P x \u2227 R x)\u27e7 \u27f9 \u2200x. P x \u27f6 Q x\"\nby auto \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_22b:\n  assumes \"\u2200x. P x \u27f6 Q x \u2228 R x\" \n          \"\u00ac(\u2203x. P x \u2227 R x)\"\n  shows   \"\u2200x. P x \u27f6 Q x\"\nproof\n  fix a\n  show \"P a \u27f6 Q a\"\n  proof\n    assume \"P a\"\n    have \"P a \u27f6 Q a \u2228 R a\" using assms(1) ..\n    hence \"Q a \u2228 R a\" using `P a` ..\n    thus \"Q a\"\n    proof\n      assume \"Q a\"\n      thus \"Q a\" .\n    next\n      assume \"R a\"\n      with `P a` have \"P a \u2227 R a\" ..\n      hence \"\u2203x. P x \u2227 R x\" ..\n      with assms(2) show \"Q a\" ..\n    qed\n  qed \nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_22c:\n  assumes \"\u2200x. P x \u27f6 Q x \u2228 R x\" \n          \"\u00ac(\u2203x. P x \u2227 R x)\"\n  shows   \"\u2200x. P x \u27f6 Q x\"\nproof (rule allI)\n  fix a\n  show \"P a \u27f6 Q a\"\n  proof (rule impI)\n    assume \"P a\"\n    have \"P a \u27f6 Q a \u2228 R a\" using assms(1) by (rule allE)\n    hence \"Q a \u2228 R a\" using `P a` by (rule mp)\n    thus \"Q a\"\n    proof (rule disjE)\n      assume \"Q a\"\n      thus \"Q a\" by this\n    next\n      assume \"R a\"\n      with `P a` have \"P a \u2227 R a\" by (rule conjI)\n      hence \"\u2203x. P x \u2227 R x\" by (rule exI)\n      with assms(2) show \"Q a\" by (rule notE)\n    qed\n  qed \nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 23. Demostrar\n     \u2203x y. R x y \u2228 R y x \u22a2 \u2203x y. R x y\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_23a:\n  \"\u2203x y. R x y \u2228 R y x \u27f9 \u2203x y. R x y\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_23b:\n  assumes \"\u2203x y. R x y \u2228 R y x\"\n  shows   \"\u2203x y. R x y\"\nproof -\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms ..\n  then obtain b where \"R a b \u2228 R b a\" ..\n  thus \"\u2203x y. R x y\"\n  proof\n    assume \"R a b\"\n    hence \"\u2203y. R a y\" ..\n    thus \"\u2203 x y. R x y\" ..\n  next\n    assume \"R b a\"\n    hence \"\u2203y. R b y\" ..\n    thus \"\u2203 x y. R x y\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_23c:\n  assumes \"\u2203x y. R x y \u2228 R y x\"\n  shows   \"\u2203x y. R x y\"\nproof -\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms by (rule exE)\n  then obtain b where \"R a b \u2228 R b a\" by (rule exE)\n  thus \"\u2203x y. R x y\"\n  proof (rule disjE)\n    assume \"R a b\"\n    hence \"\u2203y. R a y\" by (rule exI)\n    thus \"\u2203 x y. R x y\" by (rule exI)\n  next\n    assume \"R b a\"\n    hence \"\u2203y. R b y\" by (rule exI)\n    thus \"\u2203 x y. R x y\" by (rule exI)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 24. Demostrar\n       (\u2203x. \u2200y. P x y) \u27f6 (\u2200y. \u2203x. P x y)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_24a: \"(\u2203x. \u2200y. P x y) \u27f6 (\u2200y. \u2203x. P x y)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_24b: \"(\u2203x. \u2200y. P x y) \u27f6 (\u2200y. \u2203x. P x y)\"\nproof \n  assume \"\u2203x. \u2200y. P x y\"\n  then obtain a where \"\u2200y. P a y\" ..\n  show \"\u2200y. \u2203x. P x y\"\n  proof\n    fix b\n    have \"P a b\" using `\u2200y. P a y` ..\n    thus \"\u2203x. P x b\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_24c: \"(\u2203x. \u2200y. P x y) \u27f6 (\u2200y. \u2203x. P x y)\"\nproof (rule impI)\n  assume \"\u2203x. \u2200y. P x y\"\n  then obtain a where \"\u2200y. P a y\" by (rule exE)\n  show \"\u2200y. \u2203x. P x y\"\n  proof (rule allI)\n    fix b\n    have \"P a b\" using `\u2200y. P a y` by (rule allE)\n    thus \"\u2203x. P x b\" by (rule exI)\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 25. Demostrar\n       (\u2200x. P x \u27f6 Q) \u27f7 ((\u2203x. P x) \u27f6 Q)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_25a: \"(\u2200x. P x \u27f6 Q) \u27f7 ((\u2203x. P x) \u27f6 Q)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_25b: \"(\u2200x. P x \u27f6 Q) \u27f7 ((\u2203x. P x) \u27f6 Q)\"\nproof\n  assume \"\u2200x. P x \u27f6 Q\"\n  show \"(\u2203x. P x) \u27f6 Q\"\n  proof\n    assume \"\u2203x. P x\"\n    then obtain a where \"P a\" ..\n    have \"P a \u27f6 Q\" using `\u2200x. P x \u27f6 Q` ..\n    thus \"Q\" using `P a` ..\n  qed\nnext\n  assume \"(\u2203x. P x) \u27f6 Q\"\n  show \"\u2200x. P x \u27f6 Q\"\n  proof\n    fix b\n    show \"P b \u27f6 Q\"\n    proof\n      assume \"P b\"\n      hence \"\u2203x. P x\" ..\n      with `(\u2203x. P x) \u27f6 Q` show \"Q\" ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_25c: \"(\u2200x. P x \u27f6 Q) \u27f7 ((\u2203x. P x) \u27f6 Q)\"\nproof (rule iffI)\n  assume \"\u2200x. P x \u27f6 Q\"\n  show \"(\u2203x. P x) \u27f6 Q\"\n  proof (rule impI)\n    assume \"\u2203x. P x\"\n    then obtain a where \"P a\" by (rule exE)\n    have \"P a \u27f6 Q\" using `\u2200x. P x \u27f6 Q` by (rule allE)\n    thus \"Q\" using `P a` by (rule mp)\n  qed\nnext\n  assume \"(\u2203x. P x) \u27f6 Q\"\n  show \"\u2200x. P x \u27f6 Q\"\n  proof (rule allI)\n    fix b\n    show \"P b \u27f6 Q\"\n    proof (rule impI)\n      assume \"P b\"\n      hence \"\u2203x. P x\" by (rule exI)\n      with `(\u2203x. P x) \u27f6 Q` show \"Q\" by (rule mp)\n    qed\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 26. Demostrar\n       ((\u2200x. P x) \u2227 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2227 Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_26a: \"((\u2200x. P x) \u2227 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2227 Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_26b: \"((\u2200x. P x) \u2227 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2227 Q x)\"\nproof\n  assume \"(\u2200x. P x) \u2227 (\u2200x. Q x)\"\n  show \"\u2200x. P x \u2227 Q x\"\n  proof\n    fix a\n    have \"\u2200x. P x\" using `(\u2200x. P x) \u2227 (\u2200x. Q x)` ..\n    have \"\u2200x. Q x\" using `(\u2200x. P x) \u2227 (\u2200x. Q x)` ..\n    hence \"Q a\" .. \n    have \"P a\" using `\u2200x. P x` ..\n    thus \"P a \u2227 Q a\" using `Q a` ..\n  qed\nnext\n  assume \"\u2200x. P x \u2227 Q x\"\n  have \"\u2200x. P x\"\n  proof\n    fix a\n    have \"P a \u2227 Q a\" using `\u2200x. P x \u2227 Q x` .. \n    thus \"P a\" ..\n  qed\n  moreover have \"\u2200x. Q x\"\n  proof\n    fix a\n    have \"P a \u2227 Q a\" using `\u2200x. P x \u2227 Q x` .. \n    thus \"Q a\" ..\n  qed\n  ultimately show \"(\u2200x. P x) \u2227 (\u2200x. Q x)\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_26c: \"((\u2200x. P x) \u2227 (\u2200x. Q x)) = (\u2200x. P x \u2227 Q x)\"\nproof (rule iffI)\n  assume \"(\u2200x. P x) \u2227 (\u2200x. Q x)\"\n  show \"\u2200x. P x \u2227 Q x\"\n  proof (rule allI)\n    fix a\n    have \"\u2200x. P x\" using `(\u2200x. P x) \u2227 (\u2200x. Q x)` by (rule conjunct1)\n    have \"\u2200x. Q x\" using `(\u2200x. P x) \u2227 (\u2200x. Q x)` by (rule conjunct2)\n    hence \"Q a\" by (rule allE)\n    have \"P a\" using `\u2200x. P x` by (rule allE)\n    thus \"P a \u2227 Q a\" using `Q a` by (rule conjI)\n  qed\nnext\n  assume \"\u2200x. P x \u2227 Q x\"\n  have \"\u2200x. P x\"\n  proof (rule allI)\n    fix a\n    have \"P a \u2227 Q a\" using `\u2200x. P x \u2227 Q x` by (rule allE) \n    thus \"P a\" by (rule conjunct1)\n  qed\n  moreover have \"\u2200x. Q x\"\n  proof (rule allI)\n    fix a\n    have \"P a \u2227 Q a\" using `\u2200x. P x \u2227 Q x` by (rule allE) \n    thus \"Q a\" by (rule conjunct2)\n  qed\n  ultimately show \"(\u2200x. P x) \u2227 (\u2200x. Q x)\" by (rule conjI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 27. Demostrar o refutar\n       ((\u2200x. P x) \u2228 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2228 Q x)\n  ------------------------------------------------------------------ *}\n\nlemma ejercicio_27: \"((\u2200x. P x) \u2228 (\u2200x. Q x)) \u27f7 (\u2200x. P x \u2228 Q x)\"\noops\n\n(*\nAuto Quickcheck found a counterexample:\nP = {a\\<^isub>1}\nQ = {a\\<^isub>2}\n*)\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 28. Demostrar o refutar\n       ((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_28a: \n  \"((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_28b: \n  \"((\u2203x. P x) \u2228 (\u2203x. Q x)) \u27f7 (\u2203x. P x \u2228 Q x)\"\nproof\n  assume \"(\u2203x. P x) \u2228 (\u2203x. Q x)\"\n  thus \"\u2203x. P x \u2228 Q x\"\n  proof\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\" ..\n  next\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\" ..\n  qed\nnext\n  assume \"\u2203x. P x \u2228 Q x\"\n  then obtain a where \"P a \u2228 Q a\" ..\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 detallada es\"\nlemma ejercicio_28c: \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\"\n  proof (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)\n  next\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)\n  qed\nnext\n  assume \"\u2203x. P x \u2228 Q x\"\n  then obtain a where \"P a \u2228 Q a\" 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\ntext {* --------------------------------------------------------------- \n  Ejercicio 29. Demostrar o refutar\n       (\u2200x. \u2203y. P x y) \u27f6 (\u2203y. \u2200x. P x y)\n  ------------------------------------------------------------------ *}\n\nlemma ejercicio_29: \n  \"(\u2200x. \u2203y. P x y) \u27f6 (\u2203y. \u2200x. P x y)\"\nquickcheck\n(*\nQuickcheck found a counterexample:\n\nP = (\u03bbx. undefined)(a\\<^isub> := {b}, b := {a})\n*)\noops\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 30. Demostrar o refutar\n       (\u00ac(\u2200x. P x)) \u27f7 (\u2203x. \u00acP x)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_30a: \n  \"(\u00ac(\u2200x. P x)) \u27f7 (\u2203x. \u00acP x)\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_30b: \n  \"(\u00ac(\u2200x. P x)) \u27f7 (\u2203x. \u00acP x)\"\nproof\n  assume \"\u00ac(\u2200x. P x)\"\n  show \"\u2203x. \u00acP x\"\n  proof (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 `\u00ac(\u2200x. P x)` show False ..\n  qed\nnext\n  assume \"\u2203x. \u00acP x\"\n  then obtain a where \"\u00acP a\" ..\n  show \"\u00ac(\u2200x. P x)\"\n  proof\n    assume \"\u2200x. P x\"\n    hence \"P a\" ..\n    with `\u00acP a` show False ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_30c: \n  \"(\u00ac(\u2200x. P x)) \u27f7 (\u2203x. \u00acP x)\"\nproof (rule iffI)\n  assume \"\u00ac(\u2200x. P x)\"\n  show \"\u2203x. \u00acP x\"\n  proof (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 `\u00ac(\u2200x. P x)` show False by (rule notE)\n  qed\nnext\n  assume \"\u2203x. \u00acP x\"\n  then obtain a where \"\u00acP a\" by (rule exE)\n  show \"\u00ac(\u2200x. P x)\"\n  proof (rule notI)\n    assume \"\u2200x. P x\"\n    hence \"P a\" by (rule allE)\n    show False using `\u00acP a` `P a` by (rule notE)\n  qed\nqed\n\nsection {* Ejercicios sobre igualdad *}\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 31. Demostrar o refutar\n       P a \u27f9 \u2200x. x = a \u27f6 P x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_31a:\n  \"P a \u27f9 \u2200x. x = a \u27f6 P x\"\nby auto\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_31b:\n  assumes \"P a\"\n  shows   \"\u2200x. x = a \u27f6 P x\"\nproof\n  fix b\n  show \"b = a \u27f6 P b\"\n  proof\n    assume \"b = a\"\n    thus \"P b\" using assms by (rule ssubst)\n  qed \nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_31c:\n  assumes \"P a\"\n  shows   \"\u2200x. x = a \u27f6 P x\"\nproof (rule allI)\n  fix b\n  show \"b = a \u27f6 P b\"\n  proof (rule impI)\n    assume \"b = a\"\n    thus \"P b\" using assms by (rule ssubst)\n  qed \nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 32. Demostrar o refutar\n       \u2203x y. R x y \u2228 R y x; \u00ac(\u2203x. R x x)\u27e7 \u27f9 \u2203x y. x \u2260 y\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_32a:\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\n  assumes \"\u2203x y. R x y \u2228 R y x\"\n          \"\u00ac(\u2203x. R x x)\"\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\nusing assms\nby metis\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_32b:\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\n  assumes \"\u2203x y. R x y \u2228 R y x\"\n          \"\u00ac(\u2203x. R x x)\"\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\nproof -\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms(1) ..\n  then obtain b where \"R a b \u2228 R b a\" ..\n  hence \"a \u2260 b\"\n  proof\n    assume \"R a b\"\n    show \"a \u2260 b\"\n    proof\n      assume \"a = b\"\n      hence \"R b b\" using `R a b` by (rule subst)\n      hence \"\u2203x. R x x\" ..\n      with assms(2) show False ..\n    qed\n  next\n    assume \"R b a\"\n    show \"a \u2260 b\"\n    proof\n      assume \"a = b\"\n      hence \"R a a\" using `R b a` by (rule ssubst)\n      hence \"\u2203x. R x x\" ..\n      with assms(2) show False ..\n    qed\n  qed\n  hence \"\u2203y. a \u2260 y\" ..\n  thus \"\u2203(x::'c) y. x \u2260 y\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_32c:\n  fixes R :: \"'c \u21d2 'c \u21d2 bool\"\n  assumes \"\u2203x y. R x y \u2228 R y x\"\n          \"\u00ac(\u2203x. R x x)\"\n  shows   \"\u2203(x::'c) y. x \u2260 y\"\nproof -\n  obtain a where \"\u2203y. R a y \u2228 R y a\" using assms(1) by (rule exE)\n  then obtain b where \"R a b \u2228 R b a\" by (rule exE)\n  hence \"a \u2260 b\"\n  proof (rule disjE)\n    assume \"R a b\"\n    show \"a \u2260 b\"\n    proof (rule notI)\n      assume \"a = b\"\n      hence \"R b b\" using `R a b` by (rule subst)\n      hence \"\u2203x. R x x\" by (rule exI)\n      with assms(2) show False by (rule notE)\n    qed\n  next\n    assume \"R b a\"\n    show \"a \u2260 b\"\n    proof (rule notI)\n      assume \"a = b\"\n      hence \"R a a\" using `R b a` by (rule ssubst)\n      hence \"\u2203x. R x x\" by (rule exI)\n      with assms(2) show False by (rule notE)\n    qed\n  qed\n  hence \"\u2203y. a \u2260 y\" by (rule exI)\n  thus \"\u2203(x::'c) y. x \u2260 y\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 33. Demostrar o refutar\n     {\u2200x. P a x x, \n      \u2200x y z. P x y z \u27f6 P (f x) y (f z)} \n     \u22a2 P (f a) a (f a)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_33a:\n  \"\u27e6\u2200x. P a x x; \u2200x y z. P x y z \u27f6 P (f x) y (f z)\u27e7 \u27f9 P (f a) a (f a)\"\nby auto\n\n-- \"La demostraci\u00f3n estructura es\"\nlemma ejercicio_33b:\n  assumes \"\u2200x. P a x x\"\n          \"\u2200x y z. P x y z \u27f6 P (f x) y (f z)\"\n  shows   \"P (f a) a (f a)\"\nproof -\n  have \"P a a a\" using assms(1) ..\n  have \"\u2200y z. P a y z \u27f6 P (f a) y (f z)\" using assms(2) ..\n  hence \"\u2200z. P a a z \u27f6 P (f a) a (f z)\" ..\n  hence \"P a a a \u27f6 P (f a) a (f a)\" ..\n  thus \"P (f a) a (f a)\" using `P a a a` ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_33c:\n  assumes \"\u2200x. P a x x\"\n          \"\u2200x y z. P x y z \u27f6 P (f x) y (f z)\"\n  shows   \"P (f a) a (f a)\"\nproof -\n  have \"P a a a\" using assms(1) by (rule allE)\n  have \"\u2200y z. P a y z \u27f6 P (f a) y (f z)\" using assms(2) by (rule allE)\n  hence \"\u2200z. P a a z \u27f6 P (f a) a (f z)\" by (rule allE)\n  hence \"P a a a \u27f6 P (f a) a (f a)\" by (rule allE)\n  thus \"P (f a) a (f a)\" using `P a a a` by (rule mp)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 34. Demostrar o refutar\n     {\u2200x. P a x x, \n      \u2200x y z. P x y z \u27f6 P (f x) y (f z)\u27e7\n     \u22a2 \u2203z. P (f a) z (f (f a))\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_34a:\n  \"\u27e6\u2200x. P a x x; \u2200x y z. P x y z \u27f6 P (f x) y (f z)\u27e7\n   \u27f9 \u2203z. P (f a) z (f (f a))\"\nby metis\n\n-- \"La demostraci\u00f3n estructura es\"\nlemma ejercicio_34b:\n  assumes \"\u2200x. P a x x\" \n          \"\u2200x y z. P x y z \u27f6 P (f x) y (f z)\"\n  shows   \"\u2203z. P (f a) z (f (f a))\"\nproof -\n  have \"P a (f a) (f a)\" using assms(1) ..\n  have \"\u2200y z. P a y z \u27f6 P (f a) y (f z)\" using assms(2) ..\n  hence \"\u2200z. P a (f a) z \u27f6 P (f a) (f a) (f z)\" ..\n  hence \"P a (f a) (f a) \u27f6 P (f a) (f a) (f (f a))\" ..\n  hence \"P (f a) (f a) (f (f a))\" using `P a (f a) (f a)` ..\n  thus \"\u2203z. P (f a) z (f (f a))\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_34c:\n  assumes \"\u2200x. P a x x\" \n          \"\u2200x y z. P x y z \u27f6 P (f x) y (f z)\"\n  shows   \"\u2203z. P (f a) z (f (f a))\"\nproof -\n  have \"P a (f a) (f a)\" using assms(1) by (rule allE)\n  have \"\u2200y z. P a y z \u27f6 P (f a) y (f z)\" using assms(2) by (rule allE)\n  hence \"\u2200z. P a (f a) z \u27f6 P (f a) (f a) (f z)\" by (rule allE)\n  hence \"P a (f a) (f a) \u27f6 P (f a) (f a) (f (f a))\" by (rule allE)\n  hence \"P (f a) (f a) (f (f a))\" using `P a (f a) (f a)` by (rule mp)\n  thus \"\u2203z. P (f a) z (f (f a))\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 35. Demostrar o refutar\n     {\u2200y. Q a y, \n      \u2200x y. Q x y \u27f6 Q (s x) (s y)} \n     \u22a2 \u2203z. Qa z \u2227 Q z (s (s a))\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_35a:\n  \"\u27e6\u2200y. Q a y; \u2200x y. Q x y \u27f6 Q (s x) (s y)\u27e7 \u27f9 \u2203z. Q a z \u2227 Q z (s (s a))\"\nby auto\n\n-- \"La demostraci\u00f3n estructura es\"\nlemma ejercicio_35b:\n  assumes \"\u2200y. Q a y\" \n          \"\u2200x y. Q x y \u27f6 Q (s x) (s y)\" \n  shows   \"\u2203z. Q a z \u2227 Q z (s (s a))\"\nproof - \n  have \"Q a (s a)\" using assms(1) ..\n  have \"\u2200y. Q a y \u27f6 Q (s a) (s y)\" using assms(2) ..\n  hence \"Q a (s a) \u27f6 Q (s a) (s (s a))\" ..\n  hence \"Q (s a) (s (s a))\" using `Q a (s a)` ..\n  with `Q a (s a)` have \"Q a (s a) \u2227 Q (s a) (s (s a))\" ..\n  thus \"\u2203z. Q a z \u2227 Q z (s (s a))\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_35c:\n  assumes \"\u2200y. Q a y\" \n          \"\u2200x y. Q x y \u27f6 Q (s x) (s y)\" \n  shows   \"\u2203z. Q a z \u2227 Q z (s (s a))\"\nproof - \n  have \"Q a (s a)\" using assms(1) by (rule allE)\n  have \"\u2200y. Q a y \u27f6 Q (s a) (s y)\" using assms(2) by (rule allE)\n  hence \"Q a (s a) \u27f6 Q (s a) (s (s a))\" by (rule allE)\n  hence \"Q (s a) (s (s a))\" using `Q a (s a)` by (rule mp)\n  with `Q a (s a)` have \"Q a (s a) \u2227 Q (s a) (s (s a))\" by (rule conjI)\n  thus \"\u2203z. Q a z \u2227 Q z (s (s a))\" by (rule exI)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 36. Demostrar o refutar\n     {x = f x, odd (f x)} \u22a2 odd x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_36a:\n  \"\u27e6x = f x; odd (f x)\u27e7 \u27f9 odd x\"\nby auto\n\n-- \"La demostraci\u00f3n semiautom\u00e1tica es\"\nlemma ejercicio_36b:\n  \"\u27e6x = f x; odd (f x)\u27e7 \u27f9 odd x\"\nby (rule ssubst)\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_36c:\n  assumes \"x = f x\" \n          \"odd (f x)\" \n  shows   \"odd x\"\nproof -\n  show \"odd x\" using assms by (rule ssubst)\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 37. Demostrar o refutar\n     {x = f x, triple (f x) (f x) x} \u22a2 triple x x x\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_37a:\n  \"\u27e6x = f x; triple (f x) (f x) x\u27e7 \u27f9 triple x x x\"\nby auto\n\n-- \"La demostraci\u00f3n semiautom\u00e1tica es\"\nlemma ejercicio_37b:\n  \"\u27e6x = f x; triple (f x) (f x) x\u27e7 \u27f9 triple x x x\"\nby (rule ssubst)\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_37c:\n  assumes \"x = f x\" \n          \"triple (f x) (f x) x\" \n  shows   \"triple x x x\"\nproof -\n  show \"triple x x x\" using assms by (rule ssubst)\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se han comentado soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL. Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la autom\u00e1tica. La&#8230;<\/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":[243],"tags":[144,308,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\/4835"}],"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=4835"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4835\/revisions"}],"predecessor-version":[{"id":4839,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4835\/revisions\/4839"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4835"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4835"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4835"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}