{"id":6604,"date":"2019-04-02T16:33:27","date_gmt":"2019-04-02T14:33:27","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6604"},"modified":"2019-04-02T16:33:27","modified_gmt":"2019-04-02T14:33:27","slug":"lmf2018-deduccion-natural-en-logica-de-primer-orden-con-las-tacticas-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2018-deduccion-natural-en-logica-de-primer-orden-con-las-tacticas-isabelle-hol\/","title":{"rendered":"LMF2018: Deducci\u00f3n natural en l\u00f3gica de primer orden con las t\u00e1cticas Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-18\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo construir las pruebas por deducci\u00f3n natural usando las t\u00e1cticas de Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\ntheory T4b\nimports Main\nbegin\n\nsection \"Introducci\u00f3n\"\n\nsubsection \"Reglas de primer orden en Isabelle\/HOL\"  \n\nthm spec [no_vars]\n  (* da \u2200x. P x \u27f9 P x *)  \n  \nthm allE [no_vars]\n  (* da \u27e6\u2200x. P x; P x \u27f9 R\u27e7 \u27f9 R *)  \n  \nthm allI [no_vars]\n  (* da (\u22c0x. P x) \u27f9 \u2200x. P x *)  \n  \nthm exI \n  (* da ?P ?x \u27f9 \u2203x. ?P x *)  \n  \nthm exE [no_vars]\n  (* da \u27e6\u2203x. P x; \u22c0x. P x \u27f9 Q\u27e7 \u27f9 Q *)  \n\nsubsection \"Ejemplos de demostraciones\"\n\ntext {* Ejemplo con spec y exI*}  \nlemma \"\u2200x. P x \u27f9 \u2203y. P y\"  \n  apply (drule_tac x=a in spec)  (* da P a \u27f9 \u2203y. P y *)\n  apply (rule_tac x=a in exI)    (* da P a \u27f9 P a *)\n  apply assumption               (* da  No subgoals!*)\n  done\n\ntext {* Explicaciones:\n apply (drule_tac x=a in spec)\n + Objetivo:       \"\u2200x. P x \u27f9 \u2203y. P y\"\n + spec:           \"\u2200x. ?P x \u27f9 ?P ?x\"\n + spec \"x=a\":     \"\u2200x. ?P x \u27f9 ?P a\" \n + Unificador de   \"\u2200x. P x\" con \n                   \"\u2200x. ?P x\"\n   es              ?P\/P\n + Nuevo objetivo: \"P a \u27f9 \u2203y. P y\"\n\n apply (rule_tac x=a in exI)\n + Objetivo:       \"P a \u27f9 \u2203y. P y\"\n + exI:            \"?P ?x \u27f9 \u2203x. ?P x\"\n + exI \"x=a\":      \"?P a \u27f9 \u2203x. ?P x\"\n + Unificador de   \"\u2203y. P y\" con \n                   \"\u2203x. ?P x\"\n   es              ?P\/P\n + Nuevo objetivo: \"P a \u27f9 P a\" \n*}\n\ntext {* Ejemplo con spec y exI*}  \nlemma \"\u2200x. P x \u27f9 \u2203x. P x\"\n  apply (rule exI)    (* da \u2200x. P x \u27f9 P ?x *)\n  apply (erule spec)  (* da No subgoals! *)\n  done\n\ntext {* Explicaciones\n apply (rule exI)\n + Objetivo:       \"\u2200x. P x \u27f9 \u2203x. P x\"\n + exI:            \"?P ?x \u27f9 \u2203x. ?P x\"\n + Unificador de   \"\u2203x. P x\" y\n                   \"\u2203x. ?P x\"\n   es              ?P\/P\n + Nuevo objetivo: \"\u2200x. P x \u27f9 P ?x\"\n\n apply (erule spec)\n + Objetivo:       \"\u2200x. P x \u27f9 P ?x\"\n + spec:           \"\u2200x. ?P x \u27f9 ?P ?x\"\n + Unificador de   (\"?P ?x\", \"\u2200x.  P x\") y\n                   (\"?P ?x\", \"\u2200x. ?P x\"\n   es              ?P\/P\n + Nuevo objetivo: Vac\u00edo, porque erule aplica assumption a \n                    \"P ?x \u27f9 P ?x\"\n*}\n\ntext {* Ejemplo con allE y exI*}  \nlemma \"\u2200x. P x \u27f9 \u2203x. P x\"\n  apply (erule allE)  (* da P ?x \u27f9 \u2203x. P x*)\n  apply (erule exI)   (* da No subgoals! *)\n  done\n\ntext {* Explicaciones\n  apply (erule allE)\n  + Objetivo:       \"\u2200x. P x \u27f9 \u2203x. P x\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"?R\",      \"\u2200x. ?P x\") y \n                    (\"\u2203x. P x\", \"\u2200x. P  x\")\n    es              ?R \/ \u2203x. P x\n                    ?P \/ P\n  + Nuevo objetivo: \"P ?x \u27f9 \u2203x. P x\"\n\n  apply (erule exI)\n  + Objetivo:       \"P ?x \u27f9 \u2203x. P x\"\n  + exI:            \"?P ?x \u27f9 \u2203x. ?P x\"\n  + Unificador de   (\"\u2203x. P  x\", \"P ?x\") y\n                    (\"\u2203x. ?P x\", \"?P ?x\")\n    es              ?P \/ P\n                    ?x \/ x\n  + Nuevo objetivo: Vac\u00edo\n*}\n\ntext {* Ejemplo con erule_tac *}  \nlemma \"\u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 \u2200z. Q z\"\n  apply (rule allI)              (* da \u22c0z. \u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \n                                           \u27f9 Q z *)\n  apply (erule_tac x=z in allE)  (* da \u22c0z. \u27e6\u2200y. P y; P z \u27f6 Q z\u27e7 \n                                           \u27f9 Q z *)\n  apply (erule_tac x=z in allE)  (* da \u22c0z. \u27e6P z \u27f6 Q z; P z\u27e7 \u27f9 Q z *)\n  apply (erule impE)             (* da \u22c0z. P z \u27f9 P z\n                                       \u22c0z. \u27e6P z; Q z\u27e7 \u27f9 Q z *)\n   apply assumption+             (* da No subgoals! *)\n  done\n\nthm impE\n\ntext {* Explicaciones\n  apply (rule allI)\n  + Objetivo:       \"\u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 \u2200z. Q z\"\n  + allI:           \"(\u22c0x. ?P x) \u27f9 \u2200x. ?P x\"\n  + Unificador de   \"\u2200z. Q  z\" y\n                    \"\u2200x. ?P x\"\n    es              ?P \/ Q\n  + Ligadura:       \u22c0x \/ \u22c0z  \n  + Nuevo objetivo: \"\u22c0z. \u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 Q z\"\n\n  apply (erule_tac x=z in allE)\n  + Objetivo:       \"\u22c0z. \u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 Q z\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + allE \"x=z\"      \"\u27e6\u2200x. ?P x; ?P z \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"Q z\", \"\u2200x. P x \u27f6 Q x\") y\n                    (\"?R\",  \"\u2200x. ?P x\")\n    es              ?R   \/ Q z\n                    ?P x \/ P x \u27f6 Q x\n  + Nuevo objetivo: \"\u22c0z. \u27e6\u2200y. P y; P z \u27f6 Q z\u27e7 \u27f9 Q z\"\n  + Nota: De \"?P z \u27f9 ?R\" se obtiene la 2\u00aa hip\u00f3tesis y la conclusi\u00f3n.\n\n  apply (erule_tac x=z in allE)\n  + Objetivo:       \"\u22c0z. \u27e6\u2200y. P y; P z \u27f6 Q z\u27e7 \u27f9 Q z\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + allE \"x=z\"      \"\u27e6\u2200x. ?P x; ?P z \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"Q z\", \"\u2200y. P  y\") y\n                    (\"?R\",  \"\u2200x. ?P x\")\n    es              ?R \/ Q z\n                    ?P \/ P\n  + Nuevo objetivo: \"\u22c0z. \u27e6P z \u27f6 Q z; P z\u27e7 \u27f9 Q z\"\n  + Nota: De \"?P z \u27f9 ?R\" se obtiene la 2\u00aa hip\u00f3tesis y la conclusi\u00f3n.\n\n  apply (erule impE)\n  + Objetivo: \"\u22c0z. \u27e6P z \u27f6 Q z; P z\u27e7 \u27f9 Q z\"\n  + impE      \"\u27e6?P \u27f6 ?Q; ?P; ?Q \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de (\"Q z\", \"P z \u27f6 Q z\") y\n                  (\"?R\",  \"?P \u27f6 ?Q\")\n    es            ?R \/ Q z\n                  ?P \/ P z\n                  ?Q \/Q z\n  + Nuevos objetivos: \"\u22c0z. P z \u27f9 P z\"\n                      \"\u22c0z. \u27e6P z; Q z\u27e7 \u27f9 Q z\"\n*}\n\ntext {* Ejemplo sin erule_tac *}  \nlemma \"\u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 \u2200z. Q z\"\n  apply (rule allI)    (* da \u22c0z. \u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 Q z *)  \n  apply (erule allE)   (* da \u22c0z. \u27e6\u2200y. P y; P (?x2 z) \u27f6 Q (?x2 z)\u27e7 \n                                 \u27f9 Q z *)  \n  apply (erule allE)   (* da \u22c0z. \u27e6P (?x2 z) \u27f6 Q (?x2 z); P (?y4 z)\u27e7 \n                                 \u27f9 Q z *)  \n  apply (erule mp)     (* da \u22c0z. P (?y4 z) \u27f9 P z *)  \n  apply assumption     (* da No subgoals *)  \n  done\n\ntext {*\n  apply (rule allI)\n  + Objetivo:       \"\u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 \u2200z. Q z\"\n  + allI:           \"(\u22c0x. ?P x) \u27f9 \u2200x. ?P x\"\n  + Unificador de   \"\u2200z. Q  z\" y\n                    \"\u2200x. ?P x\"\n    es              ?P \/ Q\n  + Ligadura:       \u22c0x \/ \u22c0z \n  + Nuevo objetivo: \"\u22c0z. \u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 Q z\"\n\n  apply (erule allE)\n  + Objetivo:       \"\u22c0z. \u27e6\u2200x. P x \u27f6 Q x; \u2200y. P y\u27e7 \u27f9 Q z\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"Q z\", \"\u2200x. P x \u27f6 Q x\") y\n                    (\"?R\",  \"\u2200x. ?P x\")\n    es              ?R \/ Q z\n                    ?P x \/ P x \u27f6 Q x\n  + Nuevo objetivo: \"\u22c0z. \u27e6\u2200y. P y; P (?x2 z) \u27f6 Q (?x2 z)\u27e7 \u27f9 Q z\"\n\n  apply (erule allE)\n  + Objetivo:       \"\u22c0z. \u27e6\u2200y. P y; P (?x2 z) \u27f6 Q (?x2 z)\u27e7 \u27f9 Q z\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"Q z\", \"\u2200y. P  y\") y\n                    (\"?R\",  \"\u2200x. ?P x\")\n    es              ?R \/ Q z\n                    ?P \/ P \n  + Nuevo objetivo: \"\u22c0z. \u27e6P (?x2 z) \u27f6 Q (?x2 z); P (?y4 z)\u27e7 \u27f9 Q z\"\n\n  apply (erule mp)\n  + Objetivo:       \"\u22c0z. \u27e6P (?x2 z) \u27f6 Q (?x2 z); P (?y4 z)\u27e7 \u27f9 Q z\"\n  + mp:             \"\u27e6?P \u27f6 ?Q; ?P\u27e7 \u27f9 ?Q\"\n  + Unificador de   (\"Q z\", \"P (?x2 z) \u27f6 Q (?x2 z)\") y\n                    (\"?Q\", \"?P \u27f6 ?Q\")\n    es              ?Q \/ Q z\n                    ?x2 z\/ z\n                    ?P \/ P z\n  + Nuevo objetivo: \"\u22c0z. P (?y4 z) \u27f9 P z\"\n*}\n\ntext {* Ejemplo con exE *}    \nlemma \"(\u2203z. P z) \u2227 Q \u27f6 (\u2203y. P y \u2227 Q)\"\n  apply (rule impI)              (* da (\u2203z. P z) \u2227 Q \u27f9 \u2203y. P y \u2227 Q *)\n  apply (erule conjE)            (* da \u27e6\u2203z. P z; Q\u27e7 \u27f9 \u2203y. P y \u2227 Q *)\n  apply (erule exE)              (* da \u22c0z. \u27e6Q; P z\u27e7 \u27f9 \u2203y. P y \u2227 Q *)\n  apply (rule_tac x=\"z\" in exI)  (* da \u22c0z. \u27e6Q; P z\u27e7 \u27f9 P z \u2227 Q *)\n  apply (rule conjI)             (* da \u22c0z. \u27e6Q; P z\u27e7 \u27f9 P z\n                                       \u22c0z. \u27e6Q; P z\u27e7 \u27f9 Q *)\n   apply assumption+             (* da No subgoals! *)\n  done\n\ntext {* Explicaciones:\n  apply (rule impI)\n  + Objetivo:       \"(\u2203z. P z) \u2227 Q \u27f6 (\u2203y. P y \u2227 Q)\"\n  + impI:           \"(?P \u27f9 ?Q) \u27f9 ?P \u27f6 ?Q\"\n  + Unificador de   \"(\u2203z. P z) \u2227 Q \u27f6 (\u2203y. P y \u2227 Q)\" y\n                    \"?P \u27f6 ?Q\"\n    es              ?P \/ \"(\u2203z. P z) \u2227 Q\"\n                    ?Q \/ \"\u2203y. P y \u2227 Q\"\n  + Nuevo objetivo: \"(\u2203z. P z) \u2227 Q \u27f9 \u2203y. P y \u2227 Q\"\n\n  apply (erule conjE)            \n  + Objetivo:       \"(\u2203z. P z) \u2227 Q \u27f9 \u2203y. P y \u2227 Q\"\n  + conjE:          \"\u27e6?P \u2227 ?Q; \u27e6?P; ?Q\u27e7 \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"\u2203y. P y \u2227 Q\", \"(\u2203z. P z) \u2227 Q\") y\n                    (\"?R\",          \"?P \u2227 ?Q\")\n    es              ?R \/ \"\u2203y. P y \u2227 Q\"\n                    ?P \/ \"\u2203z. P z\"\n                    ?Q \/ Q\n  + Nuevo objetivo: \"\u27e6\u2203z. P z; Q\u27e7 \u27f9 \u2203y. P y \u2227 Q\"\n\n  apply (erule exE)              \n  + Objetivo:       \"\u27e6\u2203z. P z; Q\u27e7 \u27f9 \u2203y. P y \u2227 Q\"\n  + exE:            \"\u27e6\u2203x. ?P x; \u22c0x. ?P x \u27f9 ?Q\u27e7 \u27f9 ?Q\"\n  + Unificador de   (\"\u2203y. P y \u2227 Q\", \"\u2203z. P z\") y\n                    (\"?Q\",          \"\u2203x. ?P x\")\n    es              ?Q \/ \"\u2203y. P y \u2227 Q\"\n                    ?P x \/ P z\n  + Nuevo objetivo: \"\u22c0z. \u27e6Q; P z\u27e7 \u27f9 \u2203y. P y \u2227 Q\"\n\n  apply (rule_tac x=\"z\" in exI)  \n  + Objetivo:       \"\u22c0z. \u27e6Q; P z\u27e7 \u27f9 \u2203y. P y \u2227 Q\"\n  + exI:            \"?P ?x \u27f9 \u2203x. ?P x\"\n  + exI \"x=z\"       \"?P z \u27f9 \u2203x. ?P x\"\n  + Unificador de   \"\u2203y. P y \u2227 Q\" con\n                    \"\u2203x. ?P x\"\n    es              ?P x \/ P x \u2227 Q\n  + Nuevo objetivo: \"\u22c0z. \u27e6Q; P z\u27e7 \u27f9 P z \u2227 Q\"\n\n  apply (rule conjI)             \n  + Objetivo:         \"\u22c0z. \u27e6Q; P z\u27e7 \u27f9 P z \u2227 Q\"\n  + conjI:            \"\u27e6?P; ?Q\u27e7 \u27f9 ?P \u2227 ?Q\"\n  + Unificador de     \"P z \u2227 Q\" con\n                      \"?P \u2227 ?Q\"\n    es                ?P \/ P z\n                      ?Q \/ Q\n  + Nuevos objetivos: \"\u22c0z. \u27e6Q; P z\u27e7 \u27f9 P z\"\n                      \"\u22c0z. \u27e6Q; P z\u27e7 \u27f9 Q\"\n*}\n\nsubsection \"C\u00e1lculo de secuentes de primer orden\"\n  \nlemma \"A \u27f9 \u2200x. P x\"\n  apply (rule allI) (* da \u22c0x. A \u27f9 P x *)  \n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"A \u27f9 \u2200x. P x\"\n  + allI:           \"(\u22c0x. ?P x) \u27f9 \u2200x. ?P x\"\n  + Unificador de   \"\u2200x. P x\" y \n                    \"\u2200x. ?P x\"\n   es               ?P \/ P\n  + Nuevo objetivo: \"\u22c0x. A \u27f9 P x\" \n*}\n\nlemma \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  apply (erule allE)   (* da \u27e6A; P ?x\u27e7 \u27f9 Q *)\n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  + allI:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"Q\", \"\u2200x. P x\") y \n                    (\"?R\u00b7, \"\u2200x. ?P x)\"\n   es               ?R \/ Q\n                    ?P \/ P\n  + Nuevo objetivo: \"\u27e6A; P ?x\u27e7 \u27f9 Q\" \n*}\n\nlemma \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  apply (erule_tac x=t in allE)   (* da \u27e6A; P t\u27e7 \u27f9 Q *)\n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + allE \"x=t\"      \"\u27e6\u2200x. ?P x; ?P t \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"Q\", \"\u2200x. P x\") y \n                    (\"?R\u00b7, \"\u2200x. ?P x)\"\n   es               ?R \/ Q\n                    ?P \/ P\n  + Nuevo objetivo: \"\u27e6A; P ?t\u27e7 \u27f9 Q\" \n*}\n\nlemma \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  apply (frule spec) (* da \u27e6A; \u2200x. P x; P ?x\u27e7 \u27f9 Q *)\n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  + spec:           \"\u2200x. ?P x \u27f9 ?P ?x\" \n  + Unificador de   \"\u2200x. P x\" y \n                    \"\u2200x. ?P x\"\n   es               ?P \/ P\n  + Nuevo objetivo: \"\u27e6A; \u2200x. P x; P ?x\u27e7 \u27f9 Q\" \n*}\n\nlemma \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  apply (frule_tac x=t in spec) (* da \u27e6A; \u2200x. P x; P t\u27e7 \u27f9 Q *)\n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"\u27e6A; \u2200x. P x\u27e7 \u27f9 Q\"\n  + spec:           \"\u2200x. ?P x \u27f9 ?P ?x\" \n  + spec \"x=t\"      \"\u2200x. ?P x \u27f9 ?P t\" \n  + Unificador de   \"\u2200x. P x\" y \n                    \"\u2200x. ?P x\"\n   es               ?P \/ P\n  + Nuevo objetivo: \"\u27e6A; \u2200x. P x; P t\u27e7 \u27f9 Q\" \n*}\n\nlemma \"A \u27f9 \u2203x. P x\"\n  apply (rule exI) (* da A \u27f9 P ?x *)\n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"A \u27f9 \u2203x. P x\"\n  + spec:           \"?P ?x \u27f9 \u2203x. ?P x\" \n  + Unificador de   \"\u2203x. P x\" y \n                    \"\u2203x. ?P x\"\n   es               ?P \/ P\n  + Nuevo objetivo: \"A \u27f9 P ?x\" \n*}\n\nlemma \"A \u27f9 \u2203x. P x\"\n  apply (rule_tac x=t in exI) (* da A \u27f9 P t *)\n  oops\n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"A \u27f9 \u2203x. P x\"\n  + spec:           \"?P ?x \u27f9 \u2203x. ?P x\" \n  + spec \"x=t\":     \"?P t \u27f9 \u2203x. ?P x\" \n  + Unificador de   \"\u2203x. P x\" y \n                    \"\u2203x. ?P x\"\n   es               ?P \/ P\n  + Nuevo objetivo: \"A \u27f9 P t\" \n*}\n\nlemma \"\u27e6A; \u2203x. P x\u27e7 \u27f9 Q\"\n  apply (erule exE)  (* da \u22c0x. \u27e6A; P x\u27e7 \u27f9 Q *)\n  oops  \n\ntext {* Explicaci\u00f3n\n  + Objetivo:       \"\u27e6A; \u2203x. P x\u27e7 \u27f9 Q\"\n  + exE:            \"\u27e6\u2203x. ?P x; \u22c0x. ?P x \u27f9 ?Q\u27e7 \u27f9 ?Q\" \n  + Unificador de   (\"Q\", \"\u2203x. P x\" y \n                    (\"?Q\", \"\u2203x. ?P x\"\n   es               ?Q \/ Q\n                    ?P \/ P \n  + Nuevo objetivo: \"\u22c0x. \u27e6A; P x\u27e7 \u27f9 Q\" \n*}\n\nsection \"Ejemplos del tema 6\"\n\nsubsection {* Reglas del cuantificador universal *}\n\nlemma ej1: \"\u27e6P(c); \u2200x. (P(x) \u27f6 \u00acQ(x))\u27e7 \u27f9 \u00acQ(c)\"\n  apply (erule allE) (* da \u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c *)\n  apply (erule mp)   (* da P c \u27f9 P c *)\n  apply assumption   (* da No subgoals! *)\n  done\n    \ntext {* Explicaciones\n  apply (erule allE) \n  + Objetivo:       \"\u27e6P(c); \u2200x. (P(x) \u27f6 \u00acQ(x))\u27e7 \u27f9 \u00acQ(c)\"\n  + allE:           \"\u27e6\u2200x. ?P x; ?P ?x \u27f9 ?R\u27e7 \u27f9 ?R\"\n  + Unificador de   (\"\u00acQ(c)\", \"\u2200x. (P(x) \u27f6 \u00acQ(x))\") y\n                    (\"?R\",    \"\u2200x. ?P x\")\n    es              ?R \/ \u00acQ(c)\n                    ?P x \/ P(x) \u27f6 \u00acQ(x) \n  + Nuevo objetivo: \"\u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c\"\n\n  apply (erule mp)   \n  + Objetivo:       \"\u27e6P c; P ?x \u27f6 \u00ac Q ?x\u27e7 \u27f9 \u00ac Q c\"\n  + mp:             \"\u27e6?P \u27f6 ?Q; ?P\u27e7 \u27f9 ?Q\"\n  + Unificador de   (\"\u00ac Q c\", \"P ?x \u27f6 \u00ac Q ?x\") y\n                    (\"?Q\",    \"?P \u27f6 ?Q\")\n    es              ?Q \/ \u00ac Q c\n                    ?P \/ P c\n  + Nuevo objetivo: \"P c \u27f9 P c\" \n*}\n\nlemma ej2: \"\u27e6\u2200x. (P x \u27f6 \u00ac(Q x)); \u2200y. P y\u27e7 \u27f9 \u2200z. \u00ac(Q z)\"\n  apply (rule allI)   (* da \u22c0z. \u27e6P (?x2 z) \u27f6 \u00ac Q (?x2 z);\n                                 P (?y4 z)\u27e7\n                                \u27f9 \u00ac Q z*)\n  apply (erule allE)+ (* da \u22c0z. \u27e6P (?x2 z) \u27f6 \u00ac Q (?x2 z);\n                                 P (?y4 z)\u27e7\n                                \u27f9 \u00ac Q z *)\n  apply (erule mp)    (* da \u22c0z. P (?y4 z) \u27f9 P z *)\n  apply assumption    (* da No subgoals! *) \n  done\n    \nsubsection \"Reglas del cuantificador existencial\"\n\nlemma ej3: \"\u2200x. P x \u27f9 \u2203y. P y\"\n  apply (erule allE) (* da P ?x \u27f9 \u2203y. P y *)\n  apply (erule exI)  (* da No subgoals! *)\n  done\n    \nlemma ej4: \"\u27e6\u2200x. P x \u27f6 Q x; \u2203y. P y\u27e7 \u27f9 \u2203z. Q z\"\n  apply (erule exE)  (* da \u22c0y. \u27e6\u2200x. P x \u27f6 Q x; P y\u27e7 \u27f9 \u2203z. Q z *)\n  apply (erule allE) (* da \u22c0y. \u27e6P y; P (?x2 y) \u27f6 Q (?x2 y)\u27e7 \u27f9 \u2203z. Q z *)\n  apply (rule exI)   (* da \u22c0y. \u27e6P y; P (?x2 y) \u27f6 Q (?x2 y)\u27e7 \u27f9 Q (?z4 y) *)\n  apply (erule mp)   (* da \u22c0y. P y \u27f9 P (?x2 y) *)\n  apply assumption   (* da No subgoals! *)\n  done\n    \nsubsection \"Demostraciones de equivalencias\"\n\nlemma ej5a: \"\u00ac(\u2200x. P x) \u27f9 \u2203y. \u00acP y\"\n  apply (rule ccontr) (* da \u27e6\u00ac (\u2200x. P x); \u2204y. \u00ac P y\u27e7 \u27f9 False *)\n  apply (erule notE)  (* da \u2204y. \u00ac P y \u27f9 \u2200x. P x *)\n  apply (rule allI)   (* da \u22c0x. \u2204y. \u00ac P y \u27f9 P x *)\n  apply (rule ccontr) (* da \u22c0x. \u27e6\u2204y. \u00ac P y; \u00ac P x\u27e7 \u27f9 False *)\n  apply (erule notE)  (* da \u22c0x. \u00ac P x \u27f9 \u2203y. \u00ac P y *)\n   apply (erule exI)  (* da No subgoals! *)\n  done\n    \nlemma ej5b: \"\u2203x. \u00acP x \u27f9 \u00ac(\u2200y. P y)\"\n  apply (rule notI)  (* da \u27e6\u2203x. \u00ac P x; \u2200y. P y\u27e7 \u27f9 False *)\n  apply (erule exE)  (* da \u22c0x. \u27e6\u2200y. P y; \u00ac P x\u27e7 \u27f9 False *)\n  apply (erule allE) (* da \u22c0x. \u27e6\u00ac P x; P (?y4 x)\u27e7 \u27f9 False *)\n  apply (erule notE) (* da \u22c0x. P (?y4 x) \u27f9 P x *)\n  apply assumption   (* da No subgoals! *)\n  done\n    \nlemma ej5: \"\u00ac(\u2200x. P x) \u27f7 (\u2203x. \u00acP x)\"\n  apply (rule iffI)    (* da \u00ac (\u2200x. P x) \u27f9 \u2203x. \u00ac P x\n                             \u2203x. \u00ac P x \u27f9 \u00ac (\u2200x. P x) *)\n   apply (erule ej5a)  (* da \u2203x. \u00ac P x \u27f9 \u00ac (\u2200x. P x) *)\n  apply (erule ej5b)   (* da No subgoals! *)\n  done\n    \nlemma ej6a: \"\u2200x. P(x) \u2227 Q(x) \u27f9 (\u2200x. P x) \u2227 (\u2200x. Q x)\"\n  apply (rule conjI)    (* da \u2200x. P x \u2227 Q x \u27f9 \u2200x. P x\n                              \u2200x. P x \u2227 Q x \u27f9 \u2200x. Q x *)\n   apply (rule allI)    (* da \u22c0x. \u2200x. P x \u2227 Q x \u27f9 P x\n                              \u2200x. P x \u2227 Q x \u27f9 \u2200x. Q x *)\n   apply (erule allE)   (* da \u22c0x. P (?x5 x) \u2227 Q (?x5 x) \u27f9 P x\n                              \u2200x. P x \u2227 Q x \u27f9 \u2200x. Q x *)\n   apply (erule conjE)  (* da \u22c0x. \u27e6P (?x5 x); Q (?x5 x)\u27e7 \u27f9 P x\n                              \u2200x. P x \u2227 Q x \u27f9 \u2200x. Q x *)\n   apply assumption     (* da \u2200x. P x \u2227 Q x \u27f9 \u2200x. Q x *)\n  apply (rule allI)     (* da \u22c0x. \u2200x. P x \u2227 Q x \u27f9 Q x *)\n  apply (erule allE)    (* da \u22c0x. P (?x11 x) \u2227 Q (?x11 x) \u27f9 Q x *)\n  apply (erule conjE)   (* da \u22c0x. \u27e6P (?x11 x); Q (?x11 x)\u27e7 \u27f9 Q x *)\n  apply assumption      (* da No subgoals! *)\n  done\n    \nlemma ej6b: \"(\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 \u2200x. P x \u2227 Q x\"\n  apply (rule allI)        (* da \u22c0x. (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 P x \u2227 Q x *) \n  apply (rule conjI)       (* da \u22c0x. (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 P x\n                                 \u22c0x. (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 Q x *)\n   apply (drule conjunct1) (* da \u22c0x. \u2200x. P x \u27f9 P x\n                                 \u22c0x. (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 Q x*)\n   apply (erule spec)      (* da \u22c0x. (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 Q x *)\n   apply (drule conjunct2) (* da \u22c0x. \u2200x. Q x \u27f9 Q x *)\n  apply (erule spec)       (* da No subgoals! *)\n  done\n    \nlemma ej6: \"(\u2200x. P x \u2227 Q x) \u27f7 (\u2200x. P x) \u2227 (\u2200x. Q x)\"\n  apply (rule iffI)   (* da \u2200x. P x \u2227 Q x \u27f9 (\u2200x. P x) \u2227 (\u2200x. Q x)\n                            (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 \u2200x. P x \u2227 Q x *)\n   apply (erule ej6a) (* da (\u2200x. P x) \u2227 (\u2200x. Q x) \u27f9 \u2200x. P x \u2227 Q x *)\n  apply (erule ej6b)  (* da No subgoals! *)\n  done\n    \nlemma ej7a: \"(\u2203x. P x) \u2228 (\u2203x. Q x) \u27f9 \u2203x. P x \u2228 Q x\"\n  apply (erule disjE)   (* da \u2203x. P x \u27f9 \u2203x. P x \u2228 Q x\n                              \u2203x. Q x \u27f9 \u2203x. P x \u2228 Q x *)\n   apply (erule exE)    (* da \u22c0x. P x \u27f9 \u2203x. P x \u2228 Q x\n                              \u2203x. Q x \u27f9 \u2203x. P x \u2228 Q x *)\n   apply (rule exI)     (* da \u22c0x. P x \u27f9 P (?x5 x) \u2228 Q (?x5 x) \n                              \u2203x. Q x \u27f9 \u2203x. P x \u2228 Q x *)\n   apply (erule disjI1) (* da \u2203x. Q x \u27f9 \u2203x. P x \u2228 Q x *)\n  apply (erule exE)     (* da \u22c0x. Q x \u27f9 \u2203x. P x \u2228 Q x *)\n  apply (rule exI)      (* da \u22c0x. Q x \u27f9 P (?x10 x) \u2228 Q (?x10 x) *)\n  apply (erule disjI2)  (* da No subgoals! *) \n  done\n    \nlemma ej7b: \"\u2203x. P x \u2228 Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x)\"\n  apply (erule exE)    (* da \u22c0x. P x \u2228 Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x)*)\n  apply (erule disjE)  (* da \u22c0x. P x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x)\n                             \u22c0x. Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x) *)\n   apply (rule disjI1) (* da \u22c0x. P x \u27f9 \u2203x. P x\n                             \u22c0x. Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x) *)\n   apply (erule exI)   (* da \u22c0x. Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x) *)\n  apply (rule disjI2)  (* da  \u22c0x. Q x \u27f9 \u2203x. Q x *)\n  apply (erule exI)    (* da No subgoals! *)\n  done\n    \nlemma ej7: \"(\u2203x. P x) \u2228 (\u2203x. Q x) \u27f7 (\u2203x. P x \u2228 Q x)\"\n  apply (rule iffI)   (* da (\u2203x. P x) \u2228 (\u2203x. Q x) \u27f9 \u2203x. P x \u2228 Q x\n                            \u2203x. P x \u2228 Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x) *) \n   apply (erule ej7a) (* da \u2203x. P x \u2228 Q x \u27f9 (\u2203x. P x) \u2228 (\u2203x. Q x) *)\n  apply (erule ej7b)  (* da No subgoals! *)\n  done\n    \nlemma ej8a: \"\u2203x y. P x y \u27f9 \u2203y x. P x y\"\n  apply (erule exE)+ (* da \u22c0x y. P x y \u27f9 \u2203y x. P x y *)\n  apply (rule exI)+  (* da \u22c0x y. P x y \u27f9 P (?x6 x y) (?y4 x y) *)\n  apply assumption   (* da No subgoals! *)\n  done\n    \nlemma ej8b: \"\u2203y x. P x y \u27f9 \u2203x y. P x y\"\n  apply (erule exE)+ (* da \u22c0y x. P x y \u27f9 \u2203x y. P x *)\n  apply (rule exI)+  (* da \u22c0y x. P x y \u27f9 P (?x4 y x) (?y6 y x)*)\n  apply assumption   (* da No subgoals! *)\n  done\n\nlemma ej8: \"(\u2203x y. P x y) \u27f7 (\u2203y x. P x y)\"\n  apply (rule iffI)   (* da \u2203x y. P x y \u27f9 \u2203y x. P x y\n                            \u2203y x. P x y \u27f9 \u2203x y. P x y *)\n   apply (erule ej8a) (* da \u2203y x. P x y \u27f9 \u2203x y. P x y *)\n  apply (erule ej8b)  (* da No subgoals! *)\n  done\n    \nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3mo construir las pruebas por deducci\u00f3n natural usando las t\u00e1cticas de Isabelle\/HOL. La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<\/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":[268],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6604"}],"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=6604"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6604\/revisions"}],"predecessor-version":[{"id":6605,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6604\/revisions\/6605"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6604"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6604"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6604"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}