{"id":1172,"date":"2011-02-03T07:21:15","date_gmt":"2011-02-03T07:21:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1172"},"modified":"2013-03-08T05:50:03","modified_gmt":"2013-03-08T05:50:03","slug":"deduccion-natural-en-logica-proposicional-con-isabelleisar","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/deduccion-natural-en-logica-proposicional-con-isabelleisar\/","title":{"rendered":"Deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/Isar"},"content":{"rendered":"<p>En esta teor\u00eda se presentan los ejemplos del tema de deducci\u00f3n natural proposicional siguiendo la presentaci\u00f3n de Huth y Ryan en su libro <a href=\"http:\/\/www.cs.bham.ac.uk\/research\/projects\/lics\">Logic in Computer Science<\/a> y, m\u00e1s concretamente, a la forma como se explica en la asignatura de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-10\">L\u00f3gica inform\u00e1tica<\/a> y que puede verse en<br \/>\nlas <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-10\/temas\/tema-2.pdf\">transparencias del tema 2<\/a>.<\/p>\n<p>La p\u00e1gina al lado de cada teorema indica la p\u00e1gina de las anteriores transparencias donde se encuentra la demostraci\u00f3n.<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Deducci\u00f3n natural proposicional *}\r\n\r\ntheory LogicaProposicional\r\nimports Main \r\nbegin\r\n\r\nsection {* Reglas de la conjunci\u00f3n *}\r\n\r\ntext {*\r\n  La regla de introducci\u00f3n de la conjunci\u00f3n es\r\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\r\n  Las reglas de eliminaci\u00f3n de la conjunci\u00f3n son\r\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\r\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \r\n*}\r\n\r\nlemma -- \"p. 4\" \r\n  assumes 1: \"p \u2227 q\" and \r\n          2: \"r\" \r\n  shows \"q \u2227 r\"     \r\nproof -\r\n  have 3: \"q\" using 1 by (rule conjunct2)\r\n  show \"q \u2227 r\" using 3 2 by (rule conjI)\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"(p \u2227 q) \u2227 r\" and \r\n          2: \"s \u2227 t\" \r\n  shows \"q \u2227 s\"\r\nproof -\r\n  have 3: \"p \u2227 q\" using 1 by (rule conjunct1)\r\n  have 4: \"q\" using 3 by (rule conjunct2)\r\n  have 5: \"s\" using 2 by (rule conjunct1)\r\n  show \"q \u2227 s\" using 4 5 by (rule conjI)\r\nqed\r\n\r\nsection {* Reglas de la doble negaci\u00f3n *}\r\n\r\ntext {*\r\n  La regla de eliminaci\u00f3n de la doble negaci\u00f3n es\r\n  \u00b7 notnotD: \u00ac\u00ac P \u27f9 P\r\n  Para ajustarnos al tema de LI vamos a introducir la siguiente regla de\r\n  introducci\u00f3n de la doble negaci\u00f3n\r\n  . notnotI: P \u27f9 \u00ac\u00ac P\r\n  que, de momento, no detallamos su demostraci\u00f3n.\r\n*}\r\n\r\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\r\nby auto\r\n\r\nlemma -- \"p. 5\" \r\n  assumes 1: \"p\" and \r\n          2: \"\u00ac\u00ac(q \u2227 r)\" \r\n  shows \"\u00ac\u00acp \u2227 r\"\r\nproof -\r\n  have 3: \"\u00ac\u00acp\" using 1 by (rule notnotI)\r\n  have 4: \"q \u2227 r\" using 2 by (rule notnotD)\r\n  have 5: \"r\" using 4 by (rule conjunct2)\r\n  show \"\u00ac\u00acp \u2227 r\" using 3 5 by (rule conjI)\r\nqed        \r\n\r\nsection {* Regla de eliminaci\u00f3n del condicional *}\r\n\r\ntext {*\r\n  La regla de eliminaci\u00f3n del condicional es la regla del modus ponens\r\n  \u00b7 mp: \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \r\n*}\r\n\r\nlemma -- \"p. 6\"\r\n  assumes 1: \"\u00acp \u2227 q\" and \r\n          2: \"\u00acp \u2227 q \u27f6 r \u2228 \u00acp\" \r\n  shows \"r \u2228 \u00acp\"\r\nproof -\r\n  show \"r \u2228 \u00acp\" using 2 1 by (rule mp)\r\nqed    \r\n\r\nlemma -- \"p. 6\"\r\n  assumes 1: \"p\" and \r\n          2: \"p \u27f6 q\" and \r\n          3: \"p \u27f6 (q \u27f6 r)\" \r\n  shows \"r\"\r\nproof -\r\n  have 4: \"q\" using 2 1 by (rule mp)\r\n  have 5: \"q \u27f6 r\" using 3 1 by (rule mp)\r\n  show \"r\" using 5 4 by (rule mp)\r\nqed\r\n\r\nsection {* Regla derivada del modus tollens *}\r\n\r\ntext {*\r\n  Para ajustarnos al tema de LI vamos a introducir la regla del modus\r\n  tollens\r\n  \u00b7 mt: \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \r\n  sin, de momento, detallar su demostraci\u00f3n.\r\n*}\r\n\r\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\r\nby auto\r\n\r\nlemma -- \"p. 7\"\r\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" and \r\n          2: \"p\" and \r\n          3: \"\u00acr\" \r\n  shows \"\u00acq\"\r\nproof -\r\n  have 4: \"q \u27f6 r\" using 1 2 by (rule mp)\r\n  show \"\u00acq\" using 4 3 by (rule mt)\r\nqed    \r\n\r\nlemma -- \"p. 7\"\r\n  assumes 1: \"\u00acp \u27f6 q\" and \r\n          2: \"\u00acq\" \r\n  shows \"p\"\r\nproof -\r\n  have 3: \"\u00ac\u00acp\" using 1 2 by (rule mt)\r\n  show \"p\" using 3 by (rule notnotD)\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"p \u27f6 \u00acq\" and \r\n          2: \"q\" \r\n  shows \"\u00acp\"\r\nproof -\r\n  have 3: \"\u00ac\u00acq\" using 2 by (rule notnotI)\r\n  show \"\u00acp\" using 1 3 by (rule mt)\r\nqed\r\n\r\nsection {* Regla de introducci\u00f3n del condicional *}\r\n\r\ntext {*\r\n  La regla de introducci\u00f3n del condicional es\r\n  \u00b7 impI: (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n*}\r\n\r\nlemma -- \"p. 8\"\r\n  assumes 1: \"p \u27f6 q\" \r\n  shows \"\u00acq \u27f6 \u00acp\"\r\nproof -\r\n  { assume 3: \"\u00acq\"\r\n    have \"\u00acp\" using 1 3 by (rule mt)\r\n  } thus \"\u00acq \u27f6 \u00acp\" by (rule impI)\r\nqed    \r\n\r\nlemma -- \"p. 8\"\r\n  assumes 1: \"p \u27f6 q\" \r\n  shows \"\u00acq \u27f6 \u00acp\"\r\nproof (rule impI)\r\n  assume 3: \"\u00acq\"\r\n  show \"\u00acp\" using 1 3 by (rule mt)\r\nqed    \r\n\r\nlemma -- \"p. 8\"\r\n  assumes 1: \"p \u27f6 q\" \r\n  shows \"\u00acq \u27f6 \u00acp\"\r\nproof\r\n  assume 3: \"\u00acq\"\r\n  show \"\u00acp\" using 1 3 by (rule mt)\r\nqed    \r\n\r\nlemma -- \"p. 9\"\r\n  assumes 1: \"\u00acq \u27f6 \u00acp\" \r\n  shows \"p \u27f6 \u00ac\u00acq\"   \r\nproof -\r\n  { assume 2: \"p\"\r\n    have 3: \"\u00ac\u00acp\" using 2 by (rule notnotI)\r\n    have \"\u00ac\u00acq\" using 1 3 by (rule mt)\r\n  } thus \"p \u27f6 \u00ac\u00acq\" by (rule impI)\r\nqed\r\n\r\n\r\nlemma -- \"p. 9\"\r\n  assumes 1: \"\u00acq \u27f6 \u00acp\" \r\n  shows \"p \u27f6 \u00ac\u00acq\"   \r\nproof (rule impI)\r\n  assume 2: \"p\"\r\n  have 3: \"\u00ac\u00acp\" using 2 by (rule notnotI)\r\n  show \"\u00ac\u00acq\" using 1 3 by (rule mt)\r\nqed\r\n\r\nlemma -- \"p. 9\"\r\n  \"p \u27f6 p\"\r\nproof (rule impI)\r\nqed\r\n\r\nlemma -- \"p. 10\"\r\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\r\nproof -\r\n  { assume 1: \"q \u27f6 r\"\r\n    { assume 2: \"\u00acq \u27f6 \u00acp\"\r\n      { assume 3: \"p\"\r\n        have 4: \"\u00ac\u00acp\" using 3 by (rule notnotI)\r\n        have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\r\n        have 6: \"q\" using 5 by (rule notnotD)\r\n        have \"r\" using 1 6 by (rule mp) \r\n      } hence \"p \u27f6 r\" by (rule impI)\r\n    } hence \"(\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r\" by (rule impI)\r\n  } thus \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r)\" by (rule impI)\r\nqed\r\n\r\nlemma -- \"p. 10\"\r\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\r\nproof (rule impI)\r\n  assume 1: \"q \u27f6 r\"\r\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\r\n    proof (rule impI)\r\n      assume 2: \"\u00acq \u27f6 \u00acp\"\r\n      show \"p \u27f6 r\"\r\n        proof (rule impI)\r\n          assume 3: \"p\"\r\n          have 4: \"\u00ac\u00acp\" using 3 by (rule notnotI)\r\n          have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\r\n          have 6: \"q\" using 5 by (rule notnotD)\r\n          show \"r\" using 1 6 by (rule mp)\r\n        qed\r\n    qed\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"p \u2227 q \u27f6 r\" \r\n  shows \"p \u27f6 (q \u27f6 r)\"\r\nproof (rule impI)\r\n  assume 2: \"p\"\r\n  show \"q \u27f6 r\" \r\n    proof (rule impI)\r\n      assume 3: \"q\"\r\n      have 4: \"p \u2227 q\" using 2 3 by (rule conjI)\r\n      show \"r\" using 1 4 by (rule mp)\r\n    qed\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" \r\n  shows \"p \u2227 q \u27f6 r\"\r\nproof (rule impI)\r\n  assume 2: \"p \u2227 q\"\r\n  have 3: \"p\" using 2 by (rule conjunct1)\r\n  have 4: \"q \u27f6 r\" using 1 3 by (rule mp)\r\n  have 5: \"q\" using 2 by (rule conjunct2)\r\n  show \"r\" using 4 5 by (rule mp)\r\nqed    \r\n\r\nlemma \r\n  assumes 1: \"p \u27f6 q\" \r\n  shows \"p \u2227 r \u27f6 q \u2227 r\"\r\nproof (rule impI)\r\n  assume 2: \"p \u2227 r\"\r\n  have 3: \"p\" using 2 by (rule conjunct1)\r\n  have 4: \"q\" using 1 3 by (rule mp)\r\n  have 5: \"r\" using 2 by (rule conjunct2)\r\n  show \"q \u2227 r\" using 4 5 by (rule conjI)\r\nqed\r\n\r\nsection {* 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\nlemma -- \"p. 11\"\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\nlemma -- \"p. 12\"\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\nlemma \r\n  assumes 1: \"(p \u2228 q) \u2228 r\" \r\n  shows \"p \u2228 (q \u2228 r)\"\r\nusing 1\r\nproof (rule disjE)\r\n  { assume 2: \"p \u2228 q\"\r\n    thus \"p \u2228 (q \u2228 r)\"\r\n    proof (rule disjE)\r\n      { assume 3: \"p\"\r\n        show \"p \u2228 (q \u2228 r)\" using 3 by (rule disjI1) }\r\n    next\r\n      { assume 4: \"q\"\r\n        have 5: \"q \u2228 r\" using 4 by (rule disjI1)\r\n        show \"p \u2228 (q \u2228 r)\" using 5 by (rule disjI2) }\r\n    qed }\r\nnext\r\n  { assume 6: \"r\"\r\n    have 7: \"q \u2228 r\" using 6 by (rule disjI2)\r\n    show \"p \u2228 (q \u2228 r)\" using 7 by (rule disjI2) }\r\nqed    \r\n\r\nlemma \r\n  assumes 1: \"p \u2227 (q \u2228 r)\" \r\n  shows \"(p \u2227 q) \u2228 (p \u2227 r)\"\r\nproof -\r\n  have 2: \"p\" using 1 ..\r\n  have \"q \u2228 r\" using 1 ..\r\n  thus \"(p \u2227 q) \u2228 (p \u2227 r)\"\r\n  proof (rule disjE)\r\n    { assume 3: \"q\"\r\n      have \"p \u2227 q\" using 2 3 by (rule conjI)\r\n      thus \"(p \u2227 q) \u2228 (p \u2227 r)\" by (rule disjI1) }\r\n  next\r\n    { assume 4: \"r\"\r\n      have \"p \u2227 r\" using 2 4 by (rule conjI)\r\n      thus \"(p \u2227 q) \u2228 (p \u2227 r)\" by (rule disjI2) }\r\n  qed\r\nqed    \r\n\r\nsection {* Regla de copia *}\r\n\r\nlemma -- \"p. 13\"\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\r\n    assume \"q\"\r\n    show \"p\" using 1 by this\r\n  qed\r\nqed\r\n\r\nlemma -- \"p. 13\"\r\n  \"p \u27f6 (q \u27f6 p)\"\r\nproof \r\n  assume \"p\"\r\n  thus \"q \u27f6 p\" by (rule impI)\r\nqed\r\n\r\nsection {* 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\nlemma -- \"p. 15\"\r\n  assumes 1: \"\u00acp \u2228 q\" \r\n  shows \"p \u27f6 q\"\r\nproof\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 \"q\"\r\n      thus \"q\" by this}\r\n  qed\r\nqed    \r\n\r\nlemma -- \"p. 16\"\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\nlemma  \r\n  assumes 1: \"p \u27f6 \u00acp\" \r\n  shows \"\u00acp\"\r\nproof (rule notI)\r\n  assume 2: \"p\"\r\n  have 3: \"\u00acp\" using 1 2 by (rule mp)\r\n  show False using 3 2 by (rule notE)\r\nqed   \r\n\r\nlemma \r\n  assumes 1: \"p \u2227 \u00acq \u27f6 r\" and \r\n          2: \"\u00acr\" and \r\n          3: \"p\" \r\n  shows \"q\"    \r\nproof -\r\n  have \"\u00ac\u00acq\"\r\n  proof (rule notI)\r\n    assume 4: \"\u00acq\"\r\n    have 5: \"p \u2227 \u00acq\" using 3 4 by (rule conjI)\r\n    have 6: \"r\" using 1 5 by (rule mp)\r\n    show False using 2 6 by (rule notE)\r\n  qed\r\n  thus \"q\" by (rule notnotD)\r\nqed\r\n\r\nlemma \r\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" and \r\n          2: \"p\" and \r\n          3: \"\u00acr\" \r\n  shows \"\u00acq\"\r\nproof (rule notI)\r\n  assume 4: \"q\"\r\n  have 5: \"q \u27f6 r\" using 1 2 by (rule mp)\r\n  have 6: \"r\" using 5 4 by (rule mp)\r\n  show False using 3 6 by (rule notE)\r\nqed   \r\n\r\nsection {* 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 = Q\r\n  Las reglas de eliminaci\u00f3n del bicondicional son\r\n  \u00b7 iffD1: \u27e6Q = P; Q\u27e7 \u27f9 P \r\n  \u00b7 iffD2: \u27e6P = Q; Q\u27e7 \u27f9 P\r\n*}\r\n\r\nlemma -- \"p. 17\"\r\n  \"(p \u2227 q) = (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\nlemma -- \"p. 18\"\r\n  assumes 1: \"p = 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\nsection {* Reglas derivadas *}\r\n\r\nsubsection {* Regla del modus tollens *}\r\n\r\nlemma -- \"p. 20\"\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\nsubsection {* Regla de la introducci\u00f3n de la doble negaci\u00f3n *}\r\n\r\nlemma -- \"p. 21\"\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\nsubsection {* Regla de reducci\u00f3n al absurdo *}\r\n\r\nlemma -- \"p. 22\" \r\n  assumes 1: \"\u00acF \u27f6 False\" \r\n  shows \"F\"\r\nproof -\r\n  have 2: \"\u00ac\u00acF\"\r\n  proof (rule notI)\r\n    assume 3: \"\u00acF\"\r\n    show False using 1 3 by (rule mp)\r\n  qed\r\n  show \"F\" using 2 by (rule notnotD)\r\nqed   \r\n\r\ntext {*\r\n  La regla de reducci\u00f3n al absurdo en Isabelle se correponde con la\r\n  regla de contradicci\u00f3n \r\n  \u00b7 ccontr: (\u00acP \u27f9 False) \u27f9 P\r\n*}\r\n\r\nsubsection {* 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  Puede demostrarse como se muestra a continuaci\u00f3n.\r\n*}\r\n\r\nlemma -- \"p. 23\"\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\nlemma -- \"p. 24\"\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\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En esta teor\u00eda se presentan los ejemplos del tema de deducci\u00f3n natural proposicional siguiendo la presentaci\u00f3n de Huth y Ryan en su libro Logic in Computer Science y, m\u00e1s concretamente, a la forma como se explica en la asignatura de L\u00f3gica inform\u00e1tica y que puede verse en las transparencias del tema 2. La p\u00e1gina al&#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":[170],"tags":[85,148],"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\/1172"}],"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=1172"}],"version-history":[{"count":12,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1172\/revisions"}],"predecessor-version":[{"id":2938,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1172\/revisions\/2938"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1172"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1172"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1172"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}