{"id":3114,"date":"2013-03-12T18:21:36","date_gmt":"2013-03-12T18:21:36","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3114"},"modified":"2013-03-13T12:22:32","modified_gmt":"2013-03-13T12:22:32","slug":"lmf2013-deduccion-natural-proposicional-en-isabellehol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-deduccion-natural-proposicional-en-isabellehol-2\/","title":{"rendered":"LMF2013: Deducci\u00f3n natural proposicional en Isabelle\/HOL (2)"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-11\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha completado el estudio de la formalizaci\u00f3n en Isabelle\/HOL de las demostraciones por deducci\u00f3n natural estudiadas en el <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-11\/temas\/tema-2.pdf\">tema 2<\/a> que empezamos en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-deduccion-natural-proposicional-en-isabellehol\/\">clase anterior.<\/a><\/p>\n<p>Para cada uno de los ejemplos 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 los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\ntheory T3\r\nimports Main \r\nbegin\r\n\r\nsubsection {* Reglas de la disyunci\u00f3n *}\r\n\r\ntext {*\r\n  Las reglas de la introducci\u00f3n de la disyunci\u00f3n son\r\n  \u00b7 disjI1: P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2: Q \u27f9 P \u2228 Q\r\n  La regla de elimaci\u00f3n de la disyunci\u00f3n es\r\n  \u00b7 disjE:  \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \r\n*}\r\n\r\ntext {* \r\n  Ejemplo 12 (p. 11). Demostrar\r\n     p \u2228 q \u22a2 q \u2228 p\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_12_1:\r\n  assumes \"p \u2228 q\" \r\n  shows \"q \u2228 p\"\r\nproof -\r\n  have \"p \u2228 q\" using assms by this\r\n  moreover\r\n  { assume 2: \"p\"\r\n    have \"q \u2228 p\" using 2 by (rule disjI2) }\r\n  moreover\r\n  { assume 3: \"q\"\r\n    have \"q \u2228 p\" using 3 by (rule disjI1) }\r\n  ultimately show \"q \u2228 p\" by (rule disjE) \r\nqed    \r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"moreover\" para separar los bloques y\r\n  \u00b7 \"ultimately\" para unir los resultados de los bloques. *}\r\n \r\n-- \"La demostraci\u00f3n detallada con reglas impl\u00edcitas es\"\r\nlemma ejemplo_12_2:\r\n  assumes \"p \u2228 q\" \r\n  shows \"q \u2228 p\"\r\nproof -\r\n  note `p \u2228 q`\r\n  moreover\r\n  { assume \"p\"\r\n    hence \"q \u2228 p\" .. }\r\n  moreover\r\n  { assume \"q\"\r\n    hence \"q \u2228 p\" .. }\r\n  ultimately show \"q \u2228 p\" ..\r\nqed    \r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"note\" para copiar un hecho. *}\r\n\r\n-- \"La demostraci\u00f3n hacia atr\u00e1s es\"\r\nlemma ejemplo_12_3:\r\n  assumes 1: \"p \u2228 q\" \r\n  shows \"q \u2228 p\"\r\nusing 1\r\nproof (rule disjE)\r\n  { assume 2: \"p\"\r\n    show \"q \u2228 p\" using 2 by (rule disjI2) }\r\nnext\r\n  { assume 3: \"q\"\r\n    show \"q \u2228 p\" using 3 by (rule disjI1) }\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n hacia atr\u00e1s con reglas impl\u00edcitas es\"\r\nlemma ejemplo_12_4:\r\n  assumes \"p \u2228 q\" \r\n  shows \"q \u2228 p\"\r\nusing assms\r\nproof \r\n  { assume  \"p\"\r\n    thus \"q \u2228 p\" .. }\r\nnext\r\n  { assume \"q\"\r\n    thus \"q \u2228 p\" .. }\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_12_5:\r\n  assumes \"p \u2228 q\" \r\n  shows \"q \u2228 p\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 13. (p. 12) Demostrar\r\n     q \u27f6 r \u22a2 p \u2228 q \u27f6 p \u2228 r\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\" \r\nlemma ejemplo_13_1:\r\n  assumes 1: \"q \u27f6 r\"\r\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\r\nproof (rule impI)\r\n  assume 2: \"p \u2228 q\"\r\n  thus \"p \u2228 r\"\r\n  proof (rule disjE)\r\n    { assume 3: \"p\"\r\n      show \"p \u2228 r\" using 3 by (rule disjI1) }\r\n  next\r\n    { assume 4: \"q\"\r\n      have 5: \"r\" using 1 4 by (rule mp)\r\n      show \"p \u2228 r\" using 5 by (rule disjI2) }\r\n  qed\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n estructurada es\" \r\nlemma ejemplo_13_2:\r\n  assumes \"q \u27f6 r\"\r\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\r\nproof \r\n  assume \"p \u2228 q\"\r\n  thus \"p \u2228 r\"\r\n  proof \r\n    { assume \"p\"\r\n      thus \"p \u2228 r\" .. }\r\n  next\r\n    { assume \"q\"\r\n      have \"r\" using assms `q` ..\r\n      thus \"p \u2228 r\" .. }\r\n  qed\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\" \r\nlemma ejemplo_13_3:\r\n  assumes \"q \u27f6 r\"\r\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\r\nusing assms\r\nby auto\r\n\r\nsubsection {* Regla de copia *}\r\n\r\ntext {* \r\n  Ejemplo 14 (p. 13). Demostrar\r\n     \u22a2 p \u27f6 (q \u27f6 p)\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_14_1:\r\n  \"p \u27f6 (q \u27f6 p)\"\r\nproof (rule impI)\r\n  assume 1: \"p\"\r\n  show \"q \u27f6 p\" \r\n  proof (rule impI)\r\n    assume \"q\"\r\n    show \"p\" using 1 by this\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_14_2:\r\n  \"p \u27f6 (q \u27f6 p)\"\r\nproof \r\n  assume \"p\"\r\n  thus \"q \u27f6 p\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_14_3:\r\n  \"p \u27f6 (q \u27f6 p)\"\r\nby auto\r\n\r\nsubsection {* Reglas de la negaci\u00f3n *}\r\n\r\ntext {*\r\n  La regla de eliminaci\u00f3n de lo falso es\r\n  \u00b7 FalseE: False \u27f9 P\r\n  La regla de eliminaci\u00f3n de la negaci\u00f3n es\r\n  \u00b7 notE: \u27e6\u00acP; P\u27e7 \u27f9 R\r\n  La regla de introducci\u00f3n de la negaci\u00f3n es\r\n  \u00b7 notI: (P \u27f9 False) \u27f9 \u00acP\r\n*}\r\n\r\ntext {*\r\n  Ejemplo 15 (p. 15). Demostrar\r\n     \u00acp \u2228 q \u22a2 p \u27f6 q\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_15_1:\r\n  assumes 1: \"\u00acp \u2228 q\" \r\n  shows \"p \u27f6 q\"\r\nproof (rule impI)\r\n  assume 2: \"p\"\r\n  note 1\r\n  thus \"q\"\r\n  proof (rule disjE)\r\n    { assume 3: \"\u00acp\"\r\n      show \"q\" using 3 2 by (rule notE) }\r\n  next\r\n    { assume 4: \"q\"\r\n      show \"q\" using 4 by this}\r\n  qed\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_15_2:\r\n  assumes \"\u00acp \u2228 q\" \r\n  shows \"p \u27f6 q\"\r\nproof \r\n  assume \"p\"\r\n  note `\u00acp \u2228 q`\r\n  thus \"q\"\r\n  proof\r\n    { assume \"\u00acp\"\r\n      thus \"q\" using `p` .. }\r\n  next\r\n    { assume \"q\"\r\n      thus \"q\" . }\r\n  qed\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_15_3:\r\n  assumes \"\u00acp \u2228 q\" \r\n  shows \"p \u27f6 q\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 16 (p. 16). Demostrar\r\n     p \u27f6 q, p \u27f6 \u00acq \u22a2 \u00acp\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_16_1:\r\n  assumes 1: \"p \u27f6 q\" and \r\n          2: \"p \u27f6 \u00acq\" \r\n  shows \"\u00acp\"    \r\nproof (rule notI)\r\n  assume 3: \"p\"\r\n  have 4: \"q\" using 1 3 by (rule mp)\r\n  have 5: \"\u00acq\" using 2 3 by (rule mp)\r\n  show False using 5 4 by (rule notE)\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_16_2:\r\n  assumes \"p \u27f6 q\"\r\n          \"p \u27f6 \u00acq\" \r\n  shows \"\u00acp\"    \r\nproof \r\n  assume \"p\"\r\n  have \"q\" using assms(1) `p` ..\r\n  have \"\u00acq\" using assms(2) `p` ..\r\n  thus False using `q` ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_16_3:\r\n  assumes \"p \u27f6 q\"\r\n          \"p \u27f6 \u00acq\" \r\n  shows \"\u00acp\"    \r\nusing assms\r\nby auto\r\n\r\nsubsection {* Reglas del bicondicional *}\r\n\r\ntext {*\r\n  La regla de introducci\u00f3n del bicondicional es\r\n  \u00b7 iffI: \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P \u27f7 Q\r\n  Las reglas de eliminaci\u00f3n del bicondicional son\r\n  \u00b7 iffD1: \u27e6Q \u27f7 P; Q\u27e7 \u27f9 P \r\n  \u00b7 iffD2: \u27e6P \u27f7 Q; Q\u27e7 \u27f9 P\r\n*}\r\n\r\ntext {* \r\n  Ejemplo 17 (p. 17) Demostrar\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_17_1:\r\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\r\nproof (rule iffI)\r\n  { assume 1: \"p \u2227 q\"\r\n    have 2: \"p\" using 1 by (rule conjunct1)\r\n    have 3: \"q\" using 1 by (rule conjunct2)\r\n    show \"q \u2227 p\" using 3 2 by (rule conjI) }\r\nnext\r\n  { assume 4: \"q \u2227 p\"\r\n    have 5: \"q\" using 4 by (rule conjunct1)\r\n    have 6: \"p\" using 4 by (rule conjunct2)\r\n    show \"p \u2227 q\" using 6 5 by (rule conjI) }\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_17_2:\r\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\r\nproof \r\n  { assume 1: \"p \u2227 q\"\r\n    have \"p\" using 1 ..\r\n    have \"q\" using 1 ..\r\n    show \"q \u2227 p\" using `q` `p` .. }\r\nnext\r\n  { assume 2: \"q \u2227 p\"\r\n    have \"q\" using 2 ..\r\n    have \"p\" using 2 ..\r\n    show \"p \u2227 q\" using `p` `q`  .. }\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_17_3:\r\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\r\nby auto\r\n\r\ntext {*\r\n  Ejemplo 18 (p. 18). Demostrar\r\n     p \u27f7 q, p \u2228 q \u22a2 p \u2227 q\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_18_1:\r\n  assumes 1: \"p \u27f7 q\" and \r\n          2: \"p \u2228 q\"  \r\n  shows \"p \u2227 q\"\r\nusing 2\r\nproof (rule disjE)\r\n  { assume 3: \"p\"\r\n    have 4: \"q\" using 1 3 by (rule iffD1)\r\n    show \"p \u2227 q\" using 3 4 by (rule conjI) }\r\nnext\r\n  { assume 5: \"q\"\r\n    have 6: \"p\" using 1 5 by (rule iffD2)\r\n    show \"p \u2227 q\" using 6 5 by (rule conjI) }\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_18_2:\r\n  assumes \"p \u27f7 q\"\r\n          \"p \u2228 q\"  \r\n  shows  \"p \u2227 q\"\r\nusing assms(2)\r\nproof\r\n  { assume \"p\"\r\n    with assms(1) have \"q\" ..\r\n    with `p` show \"p \u2227 q\" .. }\r\nnext\r\n  { assume \"q\"\r\n    with assms(1) have \"p\" ..\r\n    thus \"p \u2227 q\" using `q` .. }\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_18_3:\r\n  assumes \"p \u27f7 q\"\r\n          \"p \u2228 q\"  \r\n  shows \"p \u2227 q\"\r\nusing assms\r\nby auto\r\n\r\nsubsection {* Reglas derivadas *}\r\n\r\nsubsubsection {* Regla del modus tollens *}\r\n\r\ntext {* \r\n  Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir de\r\n  las reglas b\u00e1sicas. \r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_20_1:\r\n  assumes 1: \"F \u27f6 G\" and \r\n          2: \"\u00acG\" \r\n  shows \"\u00acF\"\r\nproof (rule notI)\r\n  assume 3: \"F\"\r\n  have 4: \"G\" using 1 3 by (rule mp)\r\n  show False using 2 4 by (rule notE)\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_20_2:\r\n  assumes \"F \u27f6 G\"\r\n          \"\u00acG\" \r\n  shows   \"\u00acF\"\r\nproof \r\n  assume \"F\"\r\n  with assms(1) have \"G\" ..\r\n  with assms(2) show False ..\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_20_3:\r\n  assumes \"F \u27f6 G\"\r\n          \"\u00acG\" \r\n  shows \"\u00acF\"\r\nusing assms\r\nby auto\r\n\r\nsubsubsection {* Regla de la introducci\u00f3n de la doble negaci\u00f3n *}\r\n\r\ntext {*\r\n  Ejemplo 21 (p. 21) Demostrar la regla de introducci\u00f3n de la doble\r\n  negaci\u00f3n a partir de las reglas b\u00e1sicas.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_21_1:\r\n  assumes 1: \"F\" \r\n  shows \"\u00ac\u00acF\"\r\nproof (rule notI)\r\n  assume 2: \"\u00acF\"\r\n  show False using 2 1 by (rule notE)\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_21_2:\r\n  assumes \"F\" \r\n  shows \"\u00ac\u00acF\"\r\nproof \r\n  assume \"\u00acF\"\r\n  thus False using assms ..\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_21_3:\r\n  assumes \"F\" \r\n  shows \"\u00ac\u00acF\"\r\nusing assms\r\nby auto\r\n\r\nsubsubsection {* Regla de reducci\u00f3n al absurdo *}\r\n\r\ntext {*\r\n  La regla de reducci\u00f3n al absurdo en Isabelle se correponde con la\r\n  regla cl\u00e1sica de contradicci\u00f3n \r\n  \u00b7 ccontr: (\u00acP \u27f9 False) \u27f9 P\r\n*}\r\n\r\nsubsubsection {* Ley del tercio excluso *}\r\n\r\ntext {*\r\n  La ley del tercio excluso es \r\n  \u00b7 excluded_middle: \u00acP \u2228 P\r\n*}\r\n\r\ntext {*\r\n  Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de\r\n  las reglas b\u00e1sicas.  \r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_22_1:\r\n  \"F \u2228 \u00acF\"\r\nproof (rule ccontr)\r\n  assume 1: \"\u00ac(F \u2228 \u00acF)\"\r\n  thus False\r\n  proof (rule notE)\r\n    show \"F \u2228 \u00acF\"\r\n    proof (rule disjI2)\r\n      show \"\u00acF\"\r\n      proof (rule notI)\r\n        assume 2: \"F\"\r\n        hence 3: \"F \u2228 \u00acF\" by (rule disjI1)\r\n        show False using 1 3 by (rule notE)\r\n      qed\r\n    qed\r\n  qed\r\nqed\r\n    \r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_22_2:\r\n  \"F \u2228 \u00acF\"\r\nproof (rule ccontr)\r\n  assume \"\u00ac(F \u2228 \u00acF)\"\r\n  thus False\r\n  proof (rule notE)\r\n    show \"F \u2228 \u00acF\"\r\n    proof (rule disjI2)\r\n      show \"\u00acF\"\r\n      proof (rule notI)\r\n        assume \"F\"\r\n        hence \"F \u2228 \u00acF\" ..\r\n        with `\u00ac(F \u2228 \u00acF)`show False ..\r\n      qed\r\n    qed\r\n  qed\r\nqed\r\n    \r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_22_3:\r\n  \"F \u2228 \u00acF\"\r\nusing assms\r\nby auto\r\n\r\ntext {* \r\n  Ejemplo 23 (p. 24). Demostrar\r\n     p \u27f6 q \u22a2 \u00acp \u2228 q\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_23_1:\r\n  assumes 1: \"p \u27f6 q\" \r\n  shows \"\u00acp \u2228 q\"\r\nproof -\r\n  have \"\u00acp \u2228 p\" by (rule excluded_middle)\r\n  thus \"\u00acp \u2228 q\"\r\n  proof (rule disjE)\r\n    { assume \"\u00acp\"\r\n      thus \"\u00acp \u2228 q\" by (rule disjI1) }\r\n  next\r\n    { assume 2: \"p\"\r\n      have \"q\" using 1 2 by (rule mp)\r\n      thus \"\u00acp \u2228 q\" by (rule disjI2) }\r\n  qed\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_23_2:\r\n  assumes \"p \u27f6 q\" \r\n  shows \"\u00acp \u2228 q\"\r\nproof -\r\n  have \"\u00acp \u2228 p\" ..\r\n  thus \"\u00acp \u2228 q\"\r\n  proof \r\n    { assume \"\u00acp\"\r\n      thus \"\u00acp \u2228 q\" .. }\r\n  next\r\n    { assume \"p\"\r\n      with assms have \"q\" ..\r\n      thus \"\u00acp \u2228 q\" .. }\r\n  qed\r\nqed    \r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_23_3:\r\n  assumes \"p \u27f6 q\" \r\n  shows \"\u00acp \u2228 q\"\r\nusing assms\r\nby auto\r\n\r\nsubsection {* Demostraciones por contradicci\u00f3n *}\r\n\r\ntext {* \r\n  Ejemplo 24. Demostrar que \r\n     \u00acp, p \u2228 q \u22a2 q\r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_24_1:\r\n  assumes \"\u00acp\"\r\n          \"p \u2228 q\"\r\n  shows   \"q\"\r\nusing `p \u2228 q`\r\nproof (rule disjE)\r\n  assume \"p\"\r\n  with assms(1) show \"q\" by contradiction \r\nnext\r\n  assume \"q\"\r\n  thus \"q\" by assumption\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejemplo_24_2:\r\n  assumes \"\u00acp\"\r\n          \"p \u2228 q\"\r\n  shows \"q\"\r\nusing `p \u2228 q`\r\nproof \r\n  assume \"p\"\r\n  with assms(1) show \"q\" ..\r\nnext\r\n  assume \"q\"\r\n  thus \"q\" .\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejemplo_24_3:\r\n  assumes \"\u00acp\"\r\n          \"p \u2228 q\"\r\n  shows \"q\"\r\nusing assms\r\nby auto\r\n\r\nend\r\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 de la formalizaci\u00f3n en Isabelle\/HOL de las demostraciones por deducci\u00f3n natural estudiadas en el tema 2 que empezamos en la clase anterior. Para cada uno de los ejemplos se ha presentado distintas demostraciones: desde la detallada (que sea parecida&#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":[1],"tags":[144,202],"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\/3114"}],"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=3114"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3114\/revisions"}],"predecessor-version":[{"id":3115,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3114\/revisions\/3115"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3114"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3114"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3114"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}