Elementos de lógica formalizados en Isabelle/HOL

Elementos de l´ogica formalizados en Isabelle/HOL Facultad de Matem´ aticas Departamento de Ciencias de la Computaci´ on e Inteligencia Artificial Trabajo Fin de Grado Sof´ıa Santiago Fern´andez 2 El presente Trabajo Fin de Grado se ha realizado en el Departamento de Ciencias de la Computaci´ on e Inteligencia Artificial de la Universidad de Sevilla y ha sido supervisado por Jos´ e Antonio Alonso Jim´ enez y Mar´ ıa Jos´ e Hidalgo Doblado. ´ Indice Sumario 5 Introducci´on 7 1 Sintaxis 11 1.1 F´ ormulas ...................................... 11 1.2 Subf´ ormulas .................................... 19 1.3 Conectivas generalizadas ............................ 46 2 Sem´antica 51 2.1 Sem´ antica ..................................... 51 2.2 Sem´ antica de f´ ormulas con conectivas generalizadas ............. 71 2.3 Sem´ antica de conjuntos de f´ ormulas ...................... 76 3 Lema de Hintikka 83 3.1 Conjuntos de Hintikka y propiedades b´ asicas ................. 83 3.2 Lema de Hintikka .................................100 A Lemas de HOL usados 121 A.1 La base de l´ ogica de primer orden (2) ......................121 A.1.1 L´ ogica primitiva (2.1) ..........................121 A.1.2 Reglas fundamentales (2.2) .......................122 A.1.3 Configuraci´ on del paquete (2.3) .....................124 A.2 Grupos, tambi´ en combinados con ´ ordenes (5) .................124 A.2.1 Estructuras abstractas ..........................124 3 4´ Indice A.3 Ret´ ıculos abstractos (6) ..............................124 A.4 Teor´ ıa de conjuntos para l´ ogica de orden superior (7) ............125 A.4.1 Subconjuntos y cuantificadores acotados (7.2) ............125 A.4.2 Operaciones b´ asicas (7.3) ........................125 A.4.3 M´ as operaciones y lemas (7.4) ......................126 A.5 Nociones sobre funciones (9) ..........................128 A.5.1 Actualizaci´ on de funciones (9.6) ....................128 A.6 Ret´ ıculos completos (10) .............................128 A.6.1 Ret´ ıculos completos en conjuntos (10.6) ................128 A.7 Conjuntos finitos (18) ...............................128 A.7.1 Predicado de conjuntos finitos (18.1) ..................128 A.7.2 Finitud y operaciones de conjuntos comunes (18.2) .........129 A.8 Composici´ on de functores naturales acotados (33) ..............129 A.9 El tipo de datos de la listas finitas (66) .....................129 A.9.1 Funciones b´ asicas de procesamiento de listas (66.1) .........129 Bibliograf´ıa 131 Sumario El objetivo de la L´ ogica es la formalizaci´ on del conocimiento y su razonamiento. En este trabajo, estudiaremos elementos de la l´ ogica proposicional desde la perspectiva te´ orica de First−Order Logic and Automated Theorem Proving [4]de Melvin Fitting. En particular, nos centraremos en la sintaxis y la sem´ antica, concluyendo con la versi´ on proposicional del lema de Hintikka sobre la satisfacibilidad de una clase determinada de conjuntos de f´ ormulas. Siguiendo la inspiraci´ on de Propositional Proof Systems [10] por Julius Michaelis y Tobias Nipkow, los resultados expuestos ser´ an formalizados mediante Isabelle: un demostrador interactivo que incluye herramientas de razonamiento autom´ atico para guiar al usuario en el proceso de formalizaci´ on, verificaci´ on y automatizaci´ on de resultados. Concretamente, Isabelle/HOL es una especializaci´ on de Isabelle para la l´ ogica de orden superior. Las demostraciones de los resultados en Isabelle/HOL se elaborar´ an siguiendo dos t´ acticas distintas a lo largo del trabajo. En primer lugar, cada lema ser´ a probado de manera detallada prescindiendo de toda herramienta de razonamiento autom´ atico, como resultado de una b´ usqueda inversa en cada paso de la prueba. En contraposici´ on, elaboraremos una demostraci´ on autom´ atica alternativa de cada resultado que utilice todas las herramientas de razonamiento autom´ atico que proporciona el demostrador. De este modo, se evidenciar´ a la capacidad de razonamiento autom´ atico de Isabelle. Logic’s purpose is about knowledge’s formalisation and its reasoning. In this project, we will approach Propositional Logic’s elements from the theoretical perspective of First−Order Logic and Automated Theorem Proving [4]by Melvin Fitting. We will focus on the study of Syntax and Semantics to reach propositional version of Hintikka’s lemma, which determinate the satisfiability of a concrete type of formula set. Inspired by Propositional Proof Systems [10]by Julius Michaelis and Tobias Nipkow, these results will be formalised using Isabelle: a proof assistant including automatic reasoning tools to guide the user on formalising, verifying and automating results. In particular, Isabelle/HOL is the specialization of Isabelle for High-Order Logic. The processing of the results formalised in Isabelle/HOL follows two directions. In the first place, each lemma will be proved on detail without any automation, as the result of an inverse research on every step of the demonstration until it is only completed with deductions based on elemen- 5 6´ Indice tary rules and definitions. Conversely, we will alternatively prove the results using all the automatic reasoning tools that are provide by the proof assistant. In this way, Isabelle’s power of automatic reasoning will be shown as the contrast between these two different proving tactics. Introducci´on El objetivo de la L´ ogica es la formalizaci´ on del conocimiento y el razonamiento sobre el mismo. Tiene su origen en la Antigua Grecia con Arist´ oteles y su investigaci´ on acerca de los principios del razonamiento v´ alido o correcto, recogidos fundamentalmente en su obra Organon. De este modo, dio lugar a la l´ ogica silog´ ıstica, que consist´ ıa en la deducci´ on de conclusiones a partir de dos premisas iniciales. Posteriormente, los estoicos (400-200 a.C) comenzaron a cuestionarse temas relacionados con la sem´ antica, como la naturaleza de la verdad. Formularon la paradoja del mentiroso, que plantea una incongruencia acerca de la veracidad del siguiente predicado. Esta oraci´on es falsa. Sin embargo, no fue hasta el siglo XVII que el matem´ atico y fil´ osofo Gottfried Wilhelm Leibniz (1646 – 1716) instaura un programa l´ ogico que propone la b´ usqueda de un sistema simb´ olico del lenguaje natural junto con la matematizaci´ on del concepto de validez. Estas ideas fueron la principal motivaci´ on del desarrollo de la l´ ogica moderna del siglo XIX de la mano de matem´ aticos y fil´ osofos como Bernard Bolzano (1781 – 1848), George Boole (1815 – 1864), Charles Saunders Pierce (1839 – 1914) y Gottlob Frege (1848 – 1925). Fue este ´ ultimo quien introdujo el primer tratamiento sistem´ atico de la l´ ogica proposicional. Frege bas´ o su tesis en el desarrollo de una sintaxis completa que combina el razonamiento de deducci´ on de la silog´ ıstica aristot´ elica con la noci´ on estoica de conectivas para relacionar ideas. Paralelamente desarroll´ o una sem´ antica asociada a dicha sintaxis que permitiese verificar la validez de los procesos deductivos. La l´ ogica proposicional de Frege form´ o parte de la escuela denominada logicismo. Su objetivo consist´ ıa en investigar los fundamentos de las matem´ aticas con el fin de formalizarlos l´ ogicamente, para as´ ı realizar deducciones y razonamientos v´ alidos. En las ´ ultimas d´ ecadas, el desarrollo de la computaci´ on y la inteligencia artificial ha permitido la formalizaci´ on de las matem´ aticas y la l´ ogica mediante el lenguaje computacional. Concretamente, el razonamiento autom´ atico es un ´ area que investiga los distintos aspectos del razonamiento con el fin de crear programas y algoritmos para razonar de manera pr´ acticamente autom´ atica. Se fundamenta en el programa l´ ogico desarrollado por Leibniz, estructurado en base a dos principios: la formalizaci´ on rigurosa 7 8´ Indice de resultados y el desarrollo de algoritmos que permitan manipular y razonar a partir de dichas formalizaciones. Entre las principales aplicaciones de este ´ ares se encuentra la verificaci´ on y s´ ıntesis autom´ aticas de programas. De este modo, podemos validar distintos razonamientos, as´ ı como crear herramientas de razonamiento autom´ atico que permitan el desarrollo de nuevos resultados. En este contexto nace Isabelle en 1986, desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Techniche Universit¨ at M¨ unchen. Isabelle es un demostrador interactivo que, desde el razonamiento autom´ atico, facilita la formalizaci´ on l´ ogica de resultados y proporciona herramientas para realizar deducciones. En particular, Isabelle/HOL es la especializaci´ on de Isabelle para la l´ ogica de orden superior. Junto con Coq, ACL2 y PVS, entre otros, constituye uno de los demostradores interactivos m´ as influyentes. Como demostrador interactivo, Isabelle permite automatizar razonamientos guiados por el usuario, verificando cada paso de una deducci´ on de manera precisa. Adem´ as, incorpora herramientas de razonamiento autom´ atico para mejorar la productividad del proceso de demostraci´ on. Para ello, cuenta con una extensa librer´ ıa de resultados l´ ogicos y matem´ aticos que han sido formalizados y contin´ uan en desarrollo por parte de proyectos como The Alexandria Project:Large−Scale Formal Proof for the Working Mathematician. Este proyecto comienza en 2017, dirigido por Lawrence Paulson desde la Universidad de Cambridge. Tiene como finalidad la formalizaci´ on de distintas teor´ ıas para ampliar la librer´ ıa de Isabelle, junto con la creaci´ on de herramientas interactivas que asistan a los matem´ aticos en el proceso de formalizaci´ on, demostraci´ on y b´ usqueda de nuevos resultados. El objetivo de este trabajo es la formalizaci´ on de elementos y resultados destacados de la l´ ogica proposicional en Isabelle/HOL. Est´ a inspirado en la primera secci´ on de la publicaci´ on Propositional Proof Systems [10]de Julius Michaelis y Tobias Nipkow. Del mismo modo, cabe citar los art´ ıculos Constructive Formalization of Classical Modal Logic [3]de Christian Doczkal y Gert Smolka, y Propositional Calculus in Coq [13]de Floris van Doorn, por la influencia ejercida en el desarrollo de este trabajo. El contenido te´ orico del mismo se fundamenta en el libro First−Order Logic and Automated Theorem Proving [4]de Melvin Fitting. Los tres cap´ ıtulos tratados consisten en la sintaxis, sem´ antica y, finalmente, la versi´ on proposicional del lema de Hintikka. Este ´ ultimo fue desarrollado por el fil´ osofo y l´ ogico Jaakko Hintikka (1929- 2015) como herramienta para probar la completitud de la l´ ogica de primer orden. En el primer cap´ ıtulo sobre sintaxis se establecen inicialmente las variables proposicionales que conforman los elementos b´ asicos del alfabeto, junto con una serie de conectivas que act´ uan sobre ellas. De este modo, se define por recursi´ on el conjunto de las f´ ormulas proposicionales como el menor conjunto de estructuras sint´ acticas con dicho alfabeto y conectivas que contiene a las f´ ormulas b´ asicas (una constante ⊥y las propias ´ Indice 9 variables proposicionales, llamadas f´ ormulas at´ omicas) y es cerrado mediante procedimientos de formaci´ on de nuevas f´ ormulas a partir de otras, en los que intervienen las conectivas. Como es habitual, dada esta definici´ on recursiva, se dispone de un esquema de inducci´ on sobre f´ ormulas que nos permitir´ a probar los resultados expuestos. Del mismo modo, se define recursivamente el conjunto de subf´ ormulas de una f´ ormula, mostrando propiedades que describen la estructura de las mismas en relaci´ on con las propias f´ ormulas. Finalmente se presenta la f´ ormula >a partir de la constante ⊥, y dos conectivas generalizadas que permiten extender conectivas binarias a una lista de f´ ormulas. En el siguiente cap´ ıtulo precisamos la sem´ antica asociada a las estructuras sint´ acticas. Para ello, se define una interpretaci´ on como una aplicaci´ on que asocia un booleano a cada variable proposicional. Por recursi´ on sobre la estructura de las f´ ormulas proposicionales, podemos definir el valor de una f´ ormula en una interpretaci´ on dada. De este modo, se prueba que dicho valor queda un´ ıvocamente determinado por la imagen que la interpretaci´ on asocia a cada variable proposicional que aparece en la f´ ormula. Las nociones sem´ anticas se extienden an´ alogamente a las f´ ormulas formadas con conectivas generalizadas. Posteriormente se introducen dos definiciones sem´ anticas fundamentales: modelo de una f´ ormula y f´ ormula satisfacible. La primera hace referencia a una interpretaci´ on en la que el valor de una f´ ormula dada es verdadero, mientras la segunda se trata de una f´ ormula para la que existe una interpretaci´ on que sea modelo suyo. Ambas nociones se extienden a conjuntos de f´ ormulas. Por otro lado, se define el concepto de tautolog´ ıa como aquella f´ ormula cuyo valor es verdadero en toda interpretaci´ on. Para concluir la secci´ on, daremos una noci´ on formal de consecuencia l´ ogica. El cap´ ıtulo tercero, y ´ ultimo, tiene como objetivo probar el lema de Hintikka, que manifiesta la satisfacibilidad de ciertos conjuntos de f´ ormulas. Para ello define dicha clase de conjuntos, llamados conjuntos de Hintikka, de modo que para cada uno de ellos se determina paralelamente una interpretaci´ on asociada, garantizando que esta es modelo de cada f´ ormula del conjunto. En lo referente a las demostraciones asistidas por Isabelle/HOL de los resultados formalizados a lo largo de las secciones, se elaborar´ an dos tipos de pruebas correspondientes a dos t´ acticas distintas. En primer lugar, se probar´ a cada resultado siguiendo un esquema de demostraci´ on detallado. En ´ el utilizaremos ´ unicamente y de manera precisa las reglas de simplificaci´ on y definiciones incluidas en la librer´ ıa de Isabelle, prescindiendo de las herramientas de razonamiento autom´ atico del demostrador. Para ello, se realiza una b´ usqueda inversa en cada paso de la demostraci´ on autom´ atica hasta llegar a un desarrollo de la prueba basado en deducciones a partir de resultados elementales que la completen de manera rigurosa. En contraposici´ on, se evidenciar´ a la capacidad de razonamiento autom´ atico de Isabelle/HOL mediante la realizaci´ on de una 16 Cap´ ıtulo 1. Sintaxis • Dado un conjunto finito A y un elemento cualquiera a, entonces {a} ∪ A es finito. La formalizaci´ on en Isabelle de la definici´ on anterior es precisamente finite perteneciente a la teor´ ıa FiniteSet.thy. Dicha definici´ on inductiva genera dos reglas an´ alogas a las anteriores que definen a los conjuntos finitos y que emplearemos en la demostraci´ on del resultado. fold-graph f z ∅z(emptyI) x/∈A∧fold-graph f z A y fold-graph f z ({x} ∪ A) (fxy)(insertI) De este modo, en Isabelle podemos especificar el lema como sigue. lemma finite (atoms F) oops A continuaci´ on, veamos la demostraci´ on cl´ asica del lema. Demostraci´on: La prueba es por inducci´ on sobre el tipo recursivo de las f´ ormulas. Veamos cada caso. Consideremos una f´ ormula at´ omica pcualquiera. Entonces, su conjunto de variables proposicionales es {p}, finito. Sea la f´ ormula ⊥. Entonces, su conjunto de ´ atomos es vac´ ıo y, por lo tanto, finito. Sea Funa f´ ormula cuyo conjunto de variables proposicionales sea finito. Entonces, por definici´ on, ¬FyFtienen igual conjunto de ´ atomos y, por hip´ otesis de inducci´ on, es finito. Consideremos las f´ ormulas FyGcuyos conjuntos de ´ atomos son finitos. Por construcci´ on, el conjunto de variables de F∗Ges la uni´ on de sus respectivos conjuntos de ´ atomos para cualquier ∗conectiva binaria. Por lo tanto, usando la hip´ otesis de inducci´ on, dicho conjunto es finito.  Veamos ahora la prueba detallada en Isabelle. Mostraremos con detalle todos los casos de conectivas binarias, aunque se puede observar que son completamente an´ alogos. Para facilitar la lectura, primero demostraremos por separado cada uno de los casos seg´ un el esquema inductivo de f´ ormulas, y finalmente a˜ nadiremos la prueba para una f´ ormula cualquiera a partir de los anteriores. lemma atoms-finite-atom: finite (atoms (Atom x)) 1.1. F´ ormulas 17 proof − have finite ∅ by (simp only:finite.emptyI) then have finite {x} by (simp only:finite-insert) then show finite (atoms (Atom x)) by (simp only:formula.set(1)) qed lemma atoms-finite-bot: finite (atoms ⊥) proof − have finite ∅ by (simp only:finite.emptyI) then show finite (atoms ⊥) by (simp only:formula.set(2)) qed lemma atoms-finite-not: assumes finite (atoms F) shows finite (atoms (¬F)) using assms by (simp only:formula.set(3)) lemma atoms-finite-and: assumes finite (atoms F1) finite (atoms F2) shows finite (atoms (F1 ∧F2)) proof − have finite (atoms F1 ∪atoms F2) using assms by (simp only:finite-UnI) then show finite (atoms (F1 ∧F2)) by (simp only:formula.set(4)) qed lemma atoms-finite-or: assumes finite (atoms F1) finite (atoms F2) shows finite (atoms (F1 ∨F2)) 18 Cap´ ıtulo 1. Sintaxis proof − have finite (atoms F1 ∪atoms F2) using assms by (simp only:finite-UnI) then show finite (atoms (F1 ∨F2)) by (simp only:formula.set(5)) qed lemma atoms-finite-imp: assumes finite (atoms F1) finite (atoms F2) shows finite (atoms (F1 →F2)) proof − have finite (atoms F1 ∪atoms F2) using assms by (simp only:finite-UnI) then show finite (atoms (F1 →F2)) by (simp only:formula.set(6)) qed lemma atoms-finite:finite (atoms F) proof (induction F) case (Atom x) then show ?case by (simp only:atoms-finite-atom) next case Bot then show ?case by (simp only:atoms-finite-bot) next case (Not F) then show ?case by (simp only:atoms-finite-not) next case (And F1 F2) then show ?case by (simp only:atoms-finite-and) next case (Or F1 F2) then show ?case by (simp only:atoms-finite-or) next case (Imp F1 F2) then show ?case by (simp only:atoms-finite-imp) qed 1.2. Subf´ ormulas 19 Su demostraci´ on autom´ atica es la siguiente. lemma finite (atoms F) by (induction F)simp-all 1.2 Subf´ormulas Veamos la noci´ on de subf´ ormulas. Definici´on 1.2.1 El conjunto de subf´ormulas de una f´ormula F, notada Subf(F), se define recursivamente como: •{F}si F es una f´ormula at´omica. •{⊥} si F es ⊥. •{F} ∪ Subf (G)si F es ¬G. •{F} ∪ Subf (G)∪Subf(H)si F es G∗H donde ∗es cualquier conectiva binaria. Para proceder a la formalizaci´ on de Isabelle, seguiremos dos etapas. En primer lugar, definimos la funci´ on primitiva recursiva subformulae. Esta nos devolver´ a la lista de todas las subf´ ormulas de una f´ ormula original obtenidas recursivamente. primrec subformulae :: 0a formula ⇒0a formula list where subformulae (Atom k)=[Atom k] |subformulae ⊥= [⊥] |subformulae (¬F) = (¬F)#subformulae F |subformulae (F∧G) = (F∧G)#subformulae F @subformulae G |subformulae (F∨G) = (F∨G)#subformulae F @subformulae G |subformulae (F→G)=(F→G)#subformulae F @subformulae G Observemos que, en la definici´ on anterior, # es el operador que a˜ nade un elemento al comienzo de una lista y @ concatena varias listas. Siguiendo con los ejemplos, apliquemos subformulae en las distintas f´ ormulas. En particular, al tratarse de una lista pueden aparecer elementos repetidos como se muestra a continuaci´ on. notepad begin fix p:: 0a 20 Cap´ ıtulo 1. Sintaxis have subformulae (Atom p)=[Atom p] by simp have subformulae (¬(Atom p)) = [¬(Atom p),Atom p] by simp have subformulae ((Atom p →Atom q)∨Atom r) = [(Atom p →Atom q)∨Atom r,Atom p →Atom q,Atom p, Atom q,Atom r] by simp have subformulae (Atom p ∧⊥)=[Atom p ∧⊥,Atom p,⊥] by simp have subformulae (Atom p ∨Atom p) = [Atom p ∨Atom p,Atom p,Atom p] by simp end En la segunda etapa de formalizaci´ on, definimos setSubformulae, que convierte al tipo conjunto la lista de subf´ ormulas anterior. abbreviation setSubformulae :: 0a formula ⇒0a formula set where setSubformulae F ≡set (subformulae F) De este modo, la funci´ on setSubformulae es la formalizaci´ on en Isabelle de Subf(·). En Isabelle, primero hemos definido la lista de subf´ ormulas pues, en algunos casos, es m´ as sencilla la prueba de resultados sobre este tipo. Algunas de las ventajas del tipo conjuntos son la eliminaci´ on de elementos repetidos o las operaciones propias de teor´ ıa de conjuntos. Observemos los siguientes ejemplos con el tipo de conjuntos. notepad begin fix pqr:: 0a have setSubformulae (Atom p ∨Atom p) = {Atom p ∨Atom p,Atom p} by simp have setSubformulae ((Atom p →Atom q)∨Atom r) = {(Atom p →Atom q)∨Atom r,Atom p →Atom q,Atom p, Atom q,Atom r} by auto end 1.2. Subf´ ormulas 21 Por otro lado, debemos se˜ nalar que el uso de abbreviation para definir setSubformulae no es arbitrario. No es una definici´ on propiamente dicha, sino una forma de nombrar la composici´ on de las funciones set ysubformulae. En primer lugar, veamos que setSubformulae es una formalizaci´ on de Subf en Isabelle. Para ello utilizaremos el siguiente resultado sobre listas, probado como sigue. lemma set-insert:set (x#ys) = {x} ∪ set ys by (simp only:list.set(2)Un-insert-left sup-bot.left-neutral) Por tanto, obtenemos la equivalencia como resultado de los siguientes lemas, que aparecen demostrados de manera detallada. lemma setSubformulae-atom: setSubformulae (Atom p) = {Atom p} by (simp only:subformulae.simps(1)list.set) lemma setSubformulae-bot: setSubformulae (⊥) = {⊥} by (simp only:subformulae.simps(2)list.set) lemma setSubformulae-not: shows setSubformulae (¬F) = {¬F} ∪ setSubformulae F proof − have setSubformulae (¬F) = set (¬F#subformulae F) by (simp only:subformulae.simps(3)) also have . . . ={¬F} ∪ set (subformulae F) by (simp only:set-insert) finally show ?thesis by this qed lemma setSubformulae-and: setSubformulae (F1 ∧F2) ={F1 ∧F2} ∪ (setSubformulae F1 ∪setSubformulae F2) proof − have setSubformulae (F1 ∧F2) =set ((F1 ∧F2)#(subformulae F1 @subformulae F2)) by (simp only:subformulae.simps(4)) also have . . . ={F1 ∧F2} ∪ (set (subformulae F1 @subformulae F2)) by (simp only:set-insert) also have . . . ={F1 ∧F2} ∪ (setSubformulae F1 ∪setSubformulae F2) by (simp only:set-append) 22 Cap´ ıtulo 1. Sintaxis finally show ?thesis by this qed lemma setSubformulae-or: setSubformulae (F1 ∨F2) ={F1 ∨F2} ∪ (setSubformulae F1 ∪setSubformulae F2) proof − have setSubformulae (F1 ∨F2) =set ((F1 ∨F2)#(subformulae F1 @subformulae F2)) by (simp only:subformulae.simps(5)) also have . . . ={F1 ∨F2} ∪ (set (subformulae F1 @subformulae F2)) by (simp only:set-insert) also have . . . ={F1 ∨F2} ∪ (setSubformulae F1 ∪setSubformulae F2) by (simp only:set-append) finally show ?thesis by this qed lemma setSubformulae-imp: setSubformulae (F1 →F2) ={F1 →F2} ∪ (setSubformulae F1 ∪setSubformulae F2) proof − have setSubformulae (F1 →F2) =set ((F1 →F2)#(subformulae F1 @subformulae F2)) by (simp only:subformulae.simps(6)) also have . . . ={F1 →F2} ∪ (set (subformulae F1 @subformulae F2)) by (simp only:set-insert) also have . . . ={F1 →F2} ∪ (setSubformulae F1 ∪setSubformulae F2) by (simp only:set-append) finally show ?thesis by this qed Una vez probada la equivalencia, comencemos con los resultados correspondientes a las subf´ ormulas. En primer lugar, tenemos la siguiente propiedad como consecuencia directa de la equivalencia de funciones anterior. Lema 1.2.2 Toda f´ormula es subf´ormula de ella misma. Demostraci´on: La demostraci´ on se hace en cada caso de la estructura de las f´ ormulas. 1.2. Subf´ ormulas 23 Sea pf´ ormula at´ omica cualquiera. Por definici´ on, tenemos que su conjunto de subf´ ormulas es {p}, luego se tiene la propiedad. Sea la f´ ormula ⊥. Por definici´ on, su conjunto de subf´ ormulas es {⊥}, luego se verifica el resultado. Sea la f´ ormula ¬F. Veamos que pertenece a su conjunto de subf´ ormulas. Por definici´ on, tenemos que el conjunto de subf´ ormulas de ¬Fes {¬ F} ∪ Subf(F). Por tanto, ¬Fpertence a su propio conjunto de subf´ ormulas como quer´ ıamos demostrar. Sea ∗una conectiva binaria cualquiera y las f´ ormulas FyGVeamos que F∗Gpertenece a su conjunto de subf´ ormulas. Por definici´ on, tenemos que el conjunto de subf´ ormulas de F∗Ges {F∗G} ∪ Subf (F)∪Subf(G). Por tanto, F∗Gpertence a su propio conjunto de subf´ ormulas como quer´ ıamos demostrar.  Formalicemos ahora el lema con su correspondiente demostraci´ on detallada. lemma subformulae-self:F∈setSubformulae F proof (cases F) case (Atom x1) then show ?thesis by (simp only:singletonI setSubformulae-atom) next case Bot then show ?thesis by (simp only:singletonI setSubformulae-bot) next case (Not F) then show ?thesis by (simp only:singletonI UnI1 setSubformulae-not) next case (And F1 F2) then show ?thesis by (simp only:singletonI UnI1 setSubformulae-and) next case (Or F1 F2) then show ?thesis by (simp only:singletonI UnI1 setSubformulae-or) next case (Imp F1 F2) then show ?thesis by (simp only:singletonI UnI1 setSubformulae-imp) qed 24 Cap´ ıtulo 1. Sintaxis La demostraci´ on autom´ atica es la siguiente. lemma F∈setSubformulae F by (cases F)simp-all Procedamos con los dem´ as resultados de la secci´ on. Como hemos se˜ nalado con anterioridad, utilizaremos varias propiedades de conjuntos pertenecientes a la teor´ ıa Set.thy de Isabelle, que apareceran en el glosario final. Adem´ as, definiremos dos reglas adicionales que utilizaremos con frecuencia. lemma subContUnionRev1: assumes A∪B⊆C shows A⊆C proof − have A⊆C∧B⊆C using assms by (simp only:sup.bounded-iff ) then show A⊆C by (rule conjunct1) qed lemma subContUnionRev2: assumes A∪B⊆C shows B⊆C proof − have A⊆C∧B⊆C using assms by (simp only:sup.bounded-iff ) then show B⊆C by (rule conjunct2) qed Sus correspondientes demostraciones autom´ aticas se muestran a continuaci´ on. lemma A∪B⊆C=⇒A⊆C by simp lemma A∪B⊆C=⇒B⊆C by simp Veamos ahora los distintos resultados sobre subf´ ormulas. Lema 1.2.3 Todas las f´ormulas at´omicas de una f´ormula son subf´ormulas. 1.2. Subf´ ormulas 25 Demostraci´on: Aclaremos que el conjunto de las f´ ormulas at´ omicas de una f´ ormula cualquiera est´ a formado a partir de cada elemento de su conjunto de variables proposicionales. Queremos demostrar que este conjunto est´ a contenido en el conjunto de subf´ ormulas de dicha f´ ormula. De este modo, la prueba seguir´ a el esquema inductivo para la estructura de f´ ormulas. Veamos cada caso: Consideremos la f´ ormula at´ omica pcualquiera. Como su conjunto de ´ atomos es {p}, el conjunto de sus f´ ormulas at´ omicas correspondiente ser´ a{p}. Por otro lado, su conjunto de subf´ ormulas es tambi´ en {p}, luego el conjunto de sus f´ ormulas at´ omicas est´ a contenido en el conjunto de sus subf´ ormulas como quer´ ıamos demostrar. Sea la f´ ormula ⊥. Como su conjunto de ´ atomos es vac´ ıo, es claro que el conjunto de sus f´ ormulas at´ omicas es tambi´ en el vac´ ıo y, por tanto, est´ a contenido en el conjunto de sus subf´ ormulas. Sea la f´ ormula Ftal que el conjunto de sus f´ ormulas at´ omicas est´ a contenido en el conjunto de sus subf´ ormulas. Probemos el resultado para ¬F. En primer lugar, sabemos que los conjuntos de variables proposicionales de Fy¬Fcoinciden, luego tendr´ an igual conjunto de f´ ormulas at´ omicas. Por lo tanto, por hip´ otesis de inducci´ on tenemos que el conjunto de f´ ormulas at´ omicas de Fest´ a contenido en el conjunto de subf´ ormulas de F. Por otro lado, como el conjunto de subf´ ormulas de ¬Fest´ a definido como Subf(¬F) = {¬ F} ∪ Subf (F), tenemos que el el conjunto de subf´ ormulas de Fest´ a contenido en el de ¬F. Por tanto, por propiedades de contenci´ on, tenemos que el conjunto de f´ ormulas at´ omicas de ¬Fest´ a contenido en el conjunto de subf´ ormulas de ¬Fcomo quer´ ıamos demostrar. Sean las f´ ormulas FyGtales que sus conjuntos de f´ ormulas at´ omicas est´ an contenidos en sus conjuntos de subf´ ormulas respectivamente. Probemos ahora el resultado para F∗G, donde ∗simboliza una conectiva binaria cualquiera. En primer lugar, sabemos que el conjunto de ´ atomos de F∗Ges la uni´ on de sus correspondientes conjuntos de ´ atomos. De este modo, el conjunto de f´ ormulas at´ omicas de F∗Gser´ a la uni´ on del conjunto de f´ ormulas at´ omicas de Fy el correspondiente de G. Por tanto, por hip´ otesis de inducci´ on tenemos que el conjunto de f´ ormulas at´ omicas de F∗Gest´ a contenido en la uni´ on del conjunto de subf´ ormulas de Fy el conjunto de subf´ ormulas de G. Como el conjunto de subf´ ormulas de F∗Gse define como Subf(F∗G) = {F∗G} ∪ Subf(F)∪Subf(G), tenemos que la uni´ on de los conjuntos de subf´ ormulas de FyGest´ a contenida en el conjunto de subf´ ormulas de F∗G. Por tanto, por propiedades de la contenci´ on, tenemos que le conjunto de f´ ormulas at´ omicas de F∗Gest´ a contenido en el conjunto de subf´ ormulas de F∗Gcomo quer´ ıamos demostrar.  En Isabelle, se especifica como sigue. lemma Atom ‘ atoms F ⊆setSubformulae F 32 Cap´ ıtulo 1. Sintaxis G∈setSubformulae (¬F) shows atoms G ⊆atoms (¬F) proof − have G∈ {¬F} ∪ setSubformulae F using assms(2) by (simp only:setSubformulae-not) then have G∈ {¬F} ∨ G∈setSubformulae F by (simp only:Un-iff ) then show atoms G ⊆atoms (¬F) proof (rule disjE) assume G∈ {¬F} then have G=¬F by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) next assume G∈setSubformulae F then have atoms G ⊆atoms F by (simp only:assms(1)) also have . . . =atoms (¬F) by (simp only:formula.set(3)) finally show ?thesis by this qed qed lemma subformulas-atoms-and: assumes G∈setSubformulae F1 =⇒atoms G ⊆atoms F1 G∈setSubformulae F2 =⇒atoms G ⊆atoms F2 G∈setSubformulae (F1 ∧F2) shows atoms G ⊆atoms (F1 ∧F2) proof − have G∈ {F1 ∧F2} ∪ (setSubformulae F1 ∪setSubformulae F2) using assms(3) by (simp only:setSubformulae-and) then have G∈ {F1 ∧F2} ∨ G∈setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈ {F1 ∧F2} 1.2. Subf´ ormulas 33 then have G=F1 ∧F2 by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) next assume G∈setSubformulae F1 ∪setSubformulae F2 then have G∈setSubformulae F1 ∨G∈setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈setSubformulae F1 then have atoms G ⊆atoms F1 by (rule assms(1)) also have . . . ⊆atoms F1 ∪atoms F2 by (simp only:Un-upper1) also have . . . =atoms (F1 ∧F2) by (simp only:formula.set(4)) finally show ?thesis by this next assume G∈setSubformulae F2 then have atoms G ⊆atoms F2 by (rule assms(2)) also have . . . ⊆atoms F1 ∪atoms F2 by (simp only:Un-upper2) also have . . . =atoms (F1 ∧F2) by (simp only:formula.set(4)) finally show ?thesis by this qed qed qed lemma subformulas-atoms-or: assumes G∈setSubformulae F1 =⇒atoms G ⊆atoms F1 G∈setSubformulae F2 =⇒atoms G ⊆atoms F2 G∈setSubformulae (F1 ∨F2) shows atoms G ⊆atoms (F1 ∨F2) proof − have G∈ {F1 ∨F2} ∪ (setSubformulae F1 ∪setSubformulae F2) 34 Cap´ ıtulo 1. Sintaxis using assms(3) by (simp only:setSubformulae-or) then have G∈ {F1 ∨F2} ∨ G∈setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈ {F1 ∨F2} then have G=F1 ∨F2 by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) next assume G∈setSubformulae F1 ∪setSubformulae F2 then have G∈setSubformulae F1 ∨G∈setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈setSubformulae F1 then have atoms G ⊆atoms F1 by (rule assms(1)) also have . . . ⊆atoms F1 ∪atoms F2 by (simp only:Un-upper1) also have . . . =atoms (F1 ∨F2) by (simp only:formula.set(5)) finally show ?thesis by this next assume G∈setSubformulae F2 then have atoms G ⊆atoms F2 by (rule assms(2)) also have . . . ⊆atoms F1 ∪atoms F2 by (simp only:Un-upper2) also have . . . =atoms (F1 ∨F2) by (simp only:formula.set(5)) finally show ?thesis by this qed qed qed 1.2. Subf´ ormulas 35 lemma subformulas-atoms-imp: assumes G∈setSubformulae F1 =⇒atoms G ⊆atoms F1 G∈setSubformulae F2 =⇒atoms G ⊆atoms F2 G∈setSubformulae (F1 →F2) shows atoms G ⊆atoms (F1 →F2) proof − have G∈ {F1 →F2} ∪ (setSubformulae F1 ∪setSubformulae F2) using assms(3) by (simp only:setSubformulae-imp) then have G∈ {F1 →F2} ∨ G∈setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈ {F1 →F2} then have G=F1 →F2 by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) next assume G∈setSubformulae F1 ∪setSubformulae F2 then have G∈setSubformulae F1 ∨G∈setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈setSubformulae F1 then have atoms G ⊆atoms F1 by (rule assms(1)) also have . . . ⊆atoms F1 ∪atoms F2 by (simp only:Un-upper1) also have . . . =atoms (F1 →F2) by (simp only:formula.set(6)) finally show ?thesis by this next assume G∈setSubformulae F2 then have atoms G ⊆atoms F2 by (rule assms(2)) also have . . . ⊆atoms F1 ∪atoms F2 by (simp only:Un-upper2) also have . . . =atoms (F1 →F2) 36 Cap´ ıtulo 1. Sintaxis by (simp only:formula.set(6)) finally show ?thesis by this qed qed qed lemma subformulae-atoms: G∈setSubformulae F =⇒atoms G ⊆atoms F proof (induction F) case (Atom x) then show ?case by (simp only:subformulas-atoms-atom) next case Bot then show ?case by (simp only:subformulas-atoms-bot) next case (Not F) then show ?case by (simp only:subformulas-atoms-not) next case (And F1 F2) then show ?case by (simp only:subformulas-atoms-and) next case (Or F1 F2) then show ?case by (simp only:subformulas-atoms-or) next case (Imp F1 F2) then show ?case by (simp only:subformulas-atoms-imp) qed Por ´ ultimo, su demostraci´ on autom´ atica. lemma G∈setSubformulae F =⇒atoms G ⊆atoms F by (induction F)auto A continuaci´ on vamos a introducir un lema para facilitar las siguientes demostraciones detalladas mediante contenciones en cadena. Lema 1.2.5 Sea G una subf´ormula de F, entonces el conjunto de subf´ormulas de G est´a contenido en el de F. Demostraci´on: La prueba es por inducci´ on en la estructura de f´ ormula. 1.2. Subf´ ormulas 37 Sea puna f´ ormula at´ omica cualquiera. Por definici´ on, el conjunto de sus subf´ ormulas es {p}, luego su ´ unica subf´ ormula es ella misma y, por tanto, tienen igual conjunto de subf´ ormulas. Sea la f´ ormula ⊥. Por definici´ on, el conjunto de sus subf´ ormulas es {⊥}, luego su ´ unica subf´ ormula es ella misma y, por tanto, tienen igual conjunto de subf´ ormulas. Sea una f´ ormula Ftal que para toda subf´ ormula suya se tiene que el conjunto de sus subf´ ormulas est´ a contenido en el conjunto de subf´ ormulas de F. Supongamos G subf´ ormula de ¬F. Vamos a probar que el conjunto de subf´ ormulas de Gest´ a contenido en el de ¬F. En primer lugar, por definici´ on se cumple que el conjunto de subf´ ormulas de ¬Fes de la forma Subf (¬F) = {¬ F} ∪ Subf (F). Como hemos supuesto Gsubf´ ormula de ¬F, hay dos opciones posibles: G∈ {¬ F}oG∈Subf (F). Del primer caso se obtiene que G=¬Fy, por tanto, tienen igual conjunto de subf´ ormulas. Por otro lado si suponemos que Ges subf´ ormula de F, por hip´ otesis de inducci´ on tenemos que el conjunto de subf´ ormulas de Gest´ a contenido en el de F. Como, a su vez, el conjunto de subf´ ormulas de Fest´ a contenido en el de ¬Fseg´ un la definici´ on anterior, por propiedades de la contenci´ on de verifica que el conjunto de subf´ ormulas de Gest´ a contenido en el de ¬F, como quer´ ıamos demostrar. Sean las f´ ormulas F1 yF2 tales que para cualquier subf´ ormula de F1 el conjunto de sus subf´ ormulas est´ a contenido en el conjunto de subf´ ormulas de F1, y para cualquier subf´ ormula de F2 el conjunto de sus subf´ ormulas est´ a contenido en el conjunto de subf´ ormulas de F2. Supongamos Gsubf´ ormula de F1∗F2 donde ∗simboliza una conectiva binaria cualquiera. Vamos a probar que el conjunto de subf´ ormulas de Gest´ a contenido en el de F1∗F2. En primer lugar, por definici´ on se cumple que el conjunto de subf´ ormulas de F1∗F2 es de la forma {F1∗F2} ∪ (Subf(F1)∪Subf(F2)). De este modo, tenemos dos opciones: G∈ {F1∗F2}oG∈Subf (F1)∪Subf (F2). De la primera opci´ on se deduce G=F1∗F2 y, por tanto, tienen igual conjunto de subf´ ormulas. Por otro lado, si G∈Subf(F1)∪Subf(F2), tenemos a su vez dos opciones: Ges subf´ ormula de F1 o Ges subf´ ormula de F2. Supongamos que fuese subf´ ormula de F1. En este caso, por hip´ otesis de inducci´ on se tiene que el conjunto de subf´ ormulas de Gest´ a contenido en el de F1. Por la definici´ on anterior del conjunto de subf´ ormulas de F1∗F2, se verifica que el conjunto de subf´ ormulas de F1 est´ a contenido en el de F1∗F2. Por tanto, por propiedades de contenci´ on se tiene que el conjunto de subf´ ormulas de Gest´ a contenido en el conjunto de subf´ ormulas de F1∗F2. El caso de Gsubf´ ormula de F2 se demuestra an´ alogamente cambiando el ´ ındice de la f´ ormula correspondiente. Por tanto, se verifica el resultado en este caso.  Veamos su formalizaci´ on en Isabelle junto con su demostraci´ on estructurada. lemma subContsubformulae-atom: assumes G∈setSubformulae (Atom x) 38 Cap´ ıtulo 1. Sintaxis shows setSubformulae G ⊆setSubformulae (Atom x) proof − have G∈ {Atom x}using assms by (simp only:setSubformulae-atom) then have G=Atom x by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) qed lemma subContsubformulae-bot: assumes G∈setSubformulae ⊥ shows setSubformulae G ⊆setSubformulae ⊥ proof − have G∈ {⊥} using assms by (simp only:setSubformulae-bot) then have G=⊥ by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) qed lemma subContsubformulae-not: assumes G∈setSubformulae F =⇒setSubformulae G ⊆setSubformulae F G∈setSubformulae (¬F) shows setSubformulae G ⊆setSubformulae (¬F) proof − have G∈ {¬F} ∪ setSubformulae F using assms(2) by (simp only:setSubformulae-not) then have G∈ {¬F} ∨ G∈setSubformulae F by (simp only:Un-iff ) then show setSubformulae G ⊆setSubformulae (¬F) proof assume G∈ {¬F} then have G=¬F by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) 1.2. Subf´ ormulas 39 next assume G∈setSubformulae F then have setSubformulae G ⊆setSubformulae F by (simp only:assms(1)) also have setSubformulae F ⊆setSubformulae (¬F) by (simp only:setSubformulae-not Un-upper2) finally show ?thesis by this qed qed lemma subContsubformulae-and: assumes G∈setSubformulae F1 =⇒setSubformulae G ⊆setSubformulae F1 G∈setSubformulae F2 =⇒setSubformulae G ⊆setSubformulae F2 G∈setSubformulae (F1 ∧F2) shows setSubformulae G ⊆setSubformulae (F1 ∧F2) proof − have G∈ {F1 ∧F2} ∪ (setSubformulae F1 ∪setSubformulae F2) using assms(3) by (simp only:setSubformulae-and) then have G∈ {F1 ∧F2} ∨ G∈setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈ {F1 ∧F2} then have G=F1 ∧F2 by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) next assume G∈setSubformulae F1 ∪setSubformulae F2 then have G∈setSubformulae F1 ∨G∈setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof assume G∈setSubformulae F1 then have setSubformulae G ⊆setSubformulae F1 by (simp only:assms(1)) 40 Cap´ ıtulo 1. Sintaxis also have . . . ⊆setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-upper1) also have . . . ⊆setSubformulae (F1 ∧F2) by (simp only:setSubformulae-and Un-upper2) finally show ?thesis by this next assume G∈setSubformulae F2 then have setSubformulae G ⊆setSubformulae F2 by (rule assms(2)) also have . . . ⊆setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-upper2) also have . . . ⊆setSubformulae (F1 ∧F2) by (simp only:setSubformulae-and Un-upper2) finally show ?thesis by this qed qed qed lemma subContsubformulae-or: assumes G∈setSubformulae F1 =⇒setSubformulae G ⊆setSubformulae F1 G∈setSubformulae F2 =⇒setSubformulae G ⊆setSubformulae F2 G∈setSubformulae (F1 ∨F2) shows setSubformulae G ⊆setSubformulae (F1 ∨F2) proof − have G∈ {F1 ∨F2} ∪ (setSubformulae F1 ∪setSubformulae F2) using assms(3) by (simp only:setSubformulae-or) then have G∈ {F1 ∨F2} ∨ G∈setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈ {F1 ∨F2} then have G=F1 ∨F2 by (simp only:singletonD) then show ?thesis by (simp only:subset-refl) 1.2. Subf´ ormulas 41 next assume G∈setSubformulae F1 ∪setSubformulae F2 then have G∈setSubformulae F1 ∨G∈setSubformulae F2 by (simp only:Un-iff ) then show ?thesis proof (rule disjE) assume G∈setSubformulae F1 then have setSubformulae G ⊆setSubformulae F1 by (simp only:assms(1)) also have . . . ⊆setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-upper1) also have . . . ⊆setSubformulae (F1 ∨F2) by (simp only:setSubformulae-or Un-upper2) finally show ?thesis by this next assume G∈setSubformulae F2 then have setSubformulae G ⊆setSubformulae F2 by (rule assms(2)) also have . . . ⊆setSubformulae F1 ∪setSubformulae F2 by (simp only:Un-upper2) also have . . . ⊆setSubformulae (F1 ∨F2) by (simp only:setSubformulae-or Un-upper2) finally show ?thesis by this qed qed qed lemma subContsubformulae-imp: assumes G∈setSubformulae F1 =⇒setSubformulae G ⊆setSubformulae F1 G∈setSubformulae F2 =⇒setSubformulae G ⊆setSubformulae F2 G∈setSubformulae (F1 →F2) shows setSubformulae G ⊆setSubformulae (F1 →F2) proof − have G∈ {F1 →F2} ∪ (setSubformulae F1 ∪setSubformulae F2) using assms(3) by (simp only:setSubformulae-imp) 48 Cap´ ıtulo 1. Sintaxis a˜ nadiendo una f´ ormula a una lista de f´ ormulas. Adem´ as, se observa en cada definici´ on el nuevo s´ ımbolo de notaci´ on que aparece entre par´ entesis. Por otro lado, como es habitual, de acuerdo a la definici´ on recursiva de listas, Isabelle genera autom´ aticamente un esquema inductivo que emplearemos m´ as adelante. Vamos a mostrar una propiedad sobre la conjunci´ on plural. Lema 1.3.5 El conjunto de ´atomos de la conjunci´on generalizada de una lista de f´ormulas es la uni´on de los conjuntos de ´atomos de cada f´ormula de la lista. Demostraci´on: La prueba se hace por inducci´ on sobre listas, en particular, listas de f´ ormulas. Para ello, demostremos el resultado en los casos siguientes. En primer lugar lo probaremos para la lista vac´ ıa de f´ ormulas. Es claro por definici´ on que la conjunci´ on generalizada de la lista vac´ ıa es ¬ ⊥. De este modo, su conjunto de ´ atomos coincide con los de ⊥, luego es el vac´ ıo. Por tanto, queda demostrado el resultado, pues el vac´ ıo es igual a la uni´ on del conjunto de ´ atomos de cada elemento de la lista vac´ ıa de f´ ormulas. Supongamos ahora una lista de f´ ormulas Fs verificando el enunciado. Sea la f´ ormula F, vamos a probar que F#Fs cumple la propiedad. Por definici´ on de la nueva conectiva, el conjunto de ´ atomos de la conjunci´ on generalizada de F#Fs es igual al conjunto de ´ atomos de la conjunci´ on de Fcon la conjunci´ on generalizada de Fs. De este modo, por propiedades del conjunto de ´ atomos de la conjunci´ on, tenemos que dicho conjunto es la uni´ on del conjunto de ´ atomos de Fy el conjunto de ´ atomos de la conjunci´ on generalizada de Fs. Aplicando ahora la hip´ otesis de inducci´ on sobre Fs, tenemos que lo anterior es igual a la uni´ on del conjunto de ´ atomos de Fcon la uni´ on (generalizada) de los conjuntos de ´ atomos de cada f´ ormula de Fs. Luego, por propiedades de la uni´ on, es equivalente a la uni´ on de los conjuntos de ´ atomos de cada elemento de F#Fs como quer´ ıamos demostrar.  En Isabelle se formaliza como sigue. lemma atoms-BigAnd: atoms (VFs) = S(atoms ‘ set Fs) oops Observemos el lado izquierdo de la igualdad. Fs es una lista de f´ ormulas, luego la conjunci´ on generalizada de dicha lista se trata de una f´ ormula. Al aplicarle atoms a dicha f´ ormula, obtenemos finalmente el conjunto de sus ´ atomos. Por otro lado, en el lado derecho de la igualdad tenemos el conjunto set Fs cuyos elementos son las f´ ormulas de la lista Fs. De este modo, al aplicar atoms ‘ a dicho conjunto obtenemos la imagen por atoms de cada uno de sus elementos, es decir, un conjunto cuyos elementos son los 1.3. Conectivas generalizadas 49 conjuntos de ´ atomos de cada f´ ormula de Fs. Por ´ ultimo, mediante la uni´ on se obtiene el conjunto de los ´ atomos de cada f´ ormula de la lista inicial. Veamos ahora la demostraci´ on detallada. Esta seguir´ a el esquema de inducci´ on sobre listas. Previamente vamos a probar cada caso por separado. lemma atoms-BigAnd-nil: atoms (V[]) = S(atoms ‘ set Nil) proof − have atoms (V[]) = atoms (¬⊥) by (simp only:BigAnd.simps(1)) also have . . . =atoms ⊥ by (simp only:formula.set(3)) also have . . . =∅ by (simp only:formula.set(2)) also have . . . =S∅ by (simp only:Union-empty) also have . . . =S(atoms ‘ ∅) by (simp only:image-empty) also have . . . =S(atoms ‘ set []) by (simp only:list.set) finally show ?thesis by this qed Mostramos el siguiente lema auxiliar que utilizaremos en la demostraci´ on del ´ ultimo caso de inducci´ on. lemma union-imagen:f a ∪S(f‘B) = S(f ‘ ({a} ∪ B)) by (simp only:Union-image-insert insert-is-Un[THEN sym]) Se trata de una modificaci´ on del lema Union-image-insert en Isabelle para adaptarlo al caso particular. S(f ‘ ({a} ∪ B)) = f a ∪S(f‘B)(Union-image-insert) Para ello empleamos el lema insert-is-Un. insert a A ={a} ∪ A(insert-is-Un) De esta manera, la uni´ on de un conjunto de un solo elemento y otro conjunto cualquiera es equivalente a insertar dicho elemento en el conjunto. Adem´ as, aplicamos 50 Cap´ ıtulo 1. Sintaxis el lema seguido de [THEN sym]para mostrar la equivalencia en el sentido en el que acaba de ser enunciada por simetr´ ıa, pues en Isabelle aparece en sentido opuesto. Por tanto, el lema auxiliar union-imagen es fundamentalmente el lema de Isabelle Union-image-insert teniendo en cuenta las equivalencias anteriores. Procedamos a la demostraci´ on del ´ ultimo caso de inducci´ on. lemma atoms-BigAnd-cons: assumes atoms (VFs) = S(atoms ‘ set Fs) shows atoms (V(F#Fs)) = S(atoms ‘ set (F#Fs)) proof − have atoms (V(F#Fs)) = atoms (F∧VFs) by (simp only:BigAnd.simps(2)) also have . . . =atoms F ∪atoms (VFs) by (simp only:formula.set(4)) also have . . . =atoms F ∪S(atoms ‘ set Fs) by (simp only:assms) also have . . . =S(atoms ‘ ({F} ∪ set Fs)) by (simp only:union-imagen) also have . . . =S(atoms ‘ set (F#Fs)) by (simp only:set-insert) finally show atoms (V(F#Fs)) = S(atoms ‘ set (F#Fs)) by this qed Por tanto, la demostraci´ on detallada completa es la siguiente. lemma atoms (VFs) = S(atoms ‘ set Fs) proof (induction Fs) case Nil then show ?case by (rule atoms-BigAnd-nil) next case (Cons a Fs) assume atoms (VFs) = S(atoms ‘ set Fs) then show ?case by (rule atoms-BigAnd-cons) qed Por ´ ultimo, su demostraci´ on autom´ atica. lemma atoms-BigAnd: atoms (VFs) = S(atoms ‘ set Fs) by (induction Fs)simp-all Cap´ıtulo 2 Sem´antica 2.1 Sem´antica En esta secci´ on presentaremos la sem´ antica de las f´ ormulas proposicionales y su formalizaci´ on en Isabelle/HOL. Definici´on 2.1.1 Una interpretaci´on es una aplicaci´on del conjunto de variables proposicionales en el conjunto Bde los booleanos. De este modo, las interpretaciones asignan valores de verdad a las variables proposicionales. En Isabelle, se formaliza como sigue. type-synonym 0a valuation =0a⇒bool Como podemos observar, 0a valuation representa una funci´ on entre elementos de tipo 0acualquiera que conforman los ´ atomos de una f´ ormula proposicional a los que les asigna un booleano. Se define mediante el tipo type-synonym, pues consiste en renombrar una construcci´ on ya existente en Isabelle. Dada una interpretaci´ on, vamos a definir el valor de verdad de una f´ ormula proposicional en dicha interpretaci´ on. Definici´on 2.1.2 Para cada interpretaci´on Aexiste una ´unica aplicaci´on IAdesde el conjunto de f´ormulas al conjunto Bde los booleanos definida recursivamente sobre la estructura de las f´ormulas como sigue: Sea F una f´ormula cualquiera, • Si F es una f´ormula at´omica de la forma p, entonces IA(F) = A(p). 51 52 Cap´ ıtulo 2. Sem´ antica • Si F es la f´ormula ⊥, entonces IA(F) = False. • Si F es de la forma ¬G para cierta f´ormula G, entonces IA(F) = ¬ IA(G). • Si F es de la forma G ∧H para ciertas f´ormulas G y H, entonces IA(F)= IA(G)∧ IA(H). • Si F es de la forma G ∨H para ciertas f´ormulas G y H, entonces IA(F)= IA(G)∨ IA(H). • Si F es de la forma G −→ H para ciertas f´ormulas G y H, entonces IA(F)= IA(G)−→ IA(H). En estas condiciones se dice que IA(F)es el valor de la f´ormula F en la interpretaci´on A. En Isabelle, dada una interpretaci´ on Ay una f´ ormula F, vamos a definir IA(F) mediante la funci´ on formula-semantics AF, notado como A |=F. primrec formula-semantics :: 0a valuation ⇒0a formula ⇒bool (infix |=51)where A |=Atom k =Ak | A |=⊥=False | A |=Not F = (¬ A |=F) | A |=And F G = (A |=F∧ A |=G) | A |=Or F G = (A |=F∨ A |=G) | A |=Imp F G = (A |=F−→ A |=G) Como podemos observar, formula-semantics es una funci´ on primitiva recursiva, como indica el tipo primrec, notada con el s´ ımbolo infijo |=. De este modo, dada una interpretaci´ on Asobre variables proposicionales de un tipo 0acualquiera y una f´ ormula, se define el valor de la f´ ormula en la interpretaci´ on Acomo se muestra. Veamos algunos ejemplos. notepad begin fix A:: nat valuation have (A(1:=True,2:=False,3:=True) |= (¬((Atom 1 ∨Atom 2)) →Atom 3)) = True by simp have (A(1:=True)|=Atom 1) = True by simp 2.1. Sem´ antica 53 have (A(1:=True)|=¬(Atom 1)) = False by simp have (A(1:=True,2:=False)|=¬(Atom 1)∧(Atom 2)) = False by simp have (A(1:=True,2:=False,3:=False) |= (¬((Atom 1 ∧Atom 2)) →Atom 3)) = False by simp end En los ejemplos anteriores se ha usado la notaci´ on para funciones f(a:=b). Dicha notaci´ on abreviada se corresponde con la definci´ on de fun-upd f a b. f(a:=b)=(λx.if x=athen belse f x)(fun-upd-def) Es decir, f(a:=b)es la funci´ on que para cualquier valor xdel dominio, si x=a, entonces devuelve b. En caso contrario, devuelve el valor f x. A continuaci´ on veamos una serie de definiciones sobre f´ ormulas e interpretaciones. En primer lugar, la noci´ on de modelo de una f´ ormula. Definici´on 2.1.3 Una interpretaci´on es modelo de una f´ormula si el valor de la f´ormula dada dicha interpretaci´on es Verdadero. En Isabelle se formaliza de la siguiente manera. definition isModel AF≡ A |=F Veamos cu´ ales de las interpretaciones de los ejemplos anteriores son modelos de las f´ ormulas dadas. notepad begin fix A:: nat valuation have isModel (A(1:=True)) (Atom 1) by (simp add:isModel-def ) have ¬isModel (A(1:=True)) (¬(Atom 1)) by (simp add:isModel-def ) 54 Cap´ ıtulo 2. Sem´ antica have ¬isModel (A(1:=True,2:=False)) (¬(Atom 1)∧(Atom 2)) by (simp add:isModel-def ) have ¬isModel (A(1:=True,2:=False,3:=False)) (¬((Atom 1 ∧Atom 2)) →Atom 3) by (simp add:isModel-def ) have isModel (A(1:=True,2:=False,3:=True)) (¬((Atom 1 ∨Atom 2)) →Atom 3) by (simp add:isModel-def ) end Demos ahora la noci´ on de f´ ormula satisfacible. Definici´on 2.1.4 Una f´ormula es satisfacible si tiene alg´un modelo. Se concreta en Isabelle como sigue. definition satF(F)≡ ∃ A.A |=F Mostremos ejemplos de f´ ormulas satisfacibles y no satisfacibles. Estas ´ ultimas son tambi´ en llamadas contradicciones, pues son falsas para cualquier interpretaci´ on. notepad begin fix A:: nat valuation have satF (Atom 1) by (meson formula-semantics.simps(1)satF-def ) have satF (Atom 1 ∧Atom 3) using satF-def by force have ¬satF (Atom 2 ∧(¬(Atom 2))) using satF-def by force end Como podemos observar, isModel ysatF se han formalizado usando el tipo definition pues, en ambos casos, hemos renombrado una construcci´ on no recursiva ya existente en Isabelle/HOL. 2.1. Sem´ antica 55 Continuemos con la noci´ on de f´ ormula v´ alida o tautolog´ ıa. Definici´on 2.1.5 F es una f´ormula v´alida o tautolog´ıa (|=F) si toda interpretaci´on es modelo de F. Es decir, una tautolog´ ıa es una f´ ormula que es verdadera para cualquier interpretaci´ on. En otras palabras, toda interpretaci´ on es modelo de dicha f´ ormula. En Isabelle se formaliza de la siguiente manera. abbreviation valid (|=- 51)where |=F≡ ∀ A.A |=F Por otro lado, podemos observar que se ha definido mediante el tipo abbreviation, introduciendo una nueva notaci´ on para la construcci´ on formada por un cuantificador universal aplicado al primer argumento de formula-semantics. Veamos un ejemplo cl´ asico de tautolog´ ıa: el principio del tercio excluso. notepad begin fix A:: nat valuation have |= (Atom 5 ∨(¬(Atom 5))) by simp end Otro ejemplo de tautolog´ ıa se muestra con el siguiente lema. Lema 2.1.6 La f´ormula >es una tautolog´ıa. Veamos su prueba. Demostraci´on: Sea una interpretaci´ on cualquiera A. Es obvio que, aplicando la propiedad reflexiva de la implicaci´ on, tenemos que Verdadero es equivalente a suponer que valor de ⊥en Ase implica a s´ ı mismo. Por definici´ on, se tiene que la implicaci´ on anterior es, a su vez, equivalente al valor de la f´ ormula ⊥→⊥en la interpretaci´ on A. Seg´ un la definici´ on de >, tenemos que esto es igual al valor de la f´ ormula >en la interpretaci´ on A. Finalmente, mediante esta cadena de equivalencias se observa que el valor de >en una interpretaci´ on Acualquiera es Verdadero como quer´ ıamos probar.  En Isabelle se enuncia y demuestra de manera detallada como sigue. lemma A |=> 56 Cap´ ıtulo 2. Sem´ antica proof − have A |=⊥ −→ A |=⊥ by (rule imp-refl) then have A |= (⊥→⊥) by (simp only:formula-semantics.simps(6)) thus A |=>unfolding Top-def by this qed Se demuestra autom´ aticamente como sigue. lemma top-semantics:A |=> unfolding Top-def by simp Una vez presentados los conceptos y ejemplos anteriores, continuemos con el siguiente resultado de la secci´ on. Lema 2.1.7 Sea una f´ormula F de modo que p es una variable proposicional que no pertenece a su conjunto de ´atomos. Entonces, el valor de F en una interpretaci´on no depende del valor de la variable p en dicha interpretaci´on. En Isabelle se formaliza de la siguiente manera empleando la notaci´ on de fun-upd. lemma p/∈atoms F =⇒(A(p:=V)) |=F←→ A |=F oops Veamos ahora la prueba del lema. Demostraci´on: Vamos a probar el resultado por inducci´ on en la estructura recursiva de las f´ ormulas. Para ello, dada una interpretaci´ on cualquier Ay una variable pque no pertenece al conjunto de ´ atomos de una f´ ormula, definimos la interpretaci´ on A0 como aquella que devuelve A(q)para cualquier variable qdistinta de p, y un valor cualquiera Ven caso contrario. Para demostrar que el valor de una f´ ormula en una interpretaci´ on no depende del valor de pen dicha interpretaci´ on, basta probar que el valor de la f´ ormula en Acoincide con su valor en A0seg´ un la definici´ on dada anteriormente. Demostremos los siguientes casos. Sea quna f´ ormula at´ omica cualquiera tal que pno pertenece al conjunto de sus ´ atomos {q}. De este modo, se tiene q6=p. Por definici´ on, el valor de la f´ ormula at´ omica qen la interpretaci´ on A0, es A0(q). Como hemos visto que q6=p, tenemos a su vez A0(q) = A(q)seg´ un la definici´ on de A0. A su vez, A(q)es el valor de la f´ ormula at´ omica qen la interpretaci´ on A, luego se tiene finalmente que ambos valores coinciden. Sea la f´ ormula ⊥. Por definici´ on, el valor de dicha f´ ormula es Falso en cualquier interpretaci´ on, luego se verifica el resultado en particular. 2.1. Sem´ antica 57 Sea Funa f´ ormula tal que para cualquier variable que no pertenezca al conjunto de sus ´ atomos, entonces el valor de Fen la interpretaci´ on Acoincide con su valor en la interpretaci´ on A0construida como se indica en el enunciado. Vamos a demostrar el resultado para la f´ ormula ¬Fconsiderando una variable pcualquiera que no pertenezca al conjunto de ´ atomos de ¬F. Como los conjuntos de ´ atomos de Fy¬Fson el mismo, entonces ptampoco pertenece al conjunto de ´ atomos de F. De este modo, por hip´ otesis de inducci´ on, el valor de la f´ ormula Fen la interpretaci´ on Acoincide con su valor en la interpretaci´ on A0. Por otro lado, por definici´ on tenemos que el valor de la f´ ormula ¬F en Aes la negaci´ on del valor de Fen A. Por lo visto anteriormente seg´ un la hip´ otesis de inducci´ on, esto es igual a la negaci´ on del valor de Fen A0. Por ´ ultimo, por definici´ on, esto es igual al valor de ¬Fen A0, como quer´ ıa demostrar. Sean ahora las f´ ormulas GyHtales que, para cada una, su valor en la interpretaci´ on Acoincide con su valor en la interpretaci´ on A0construida como se indica en el enunciado a partir de una variable que no pertenezca al conjunto de sus ´ atomos. Veamos que se verifica el resultado para la f´ ormula G∧H. Sea puna variable proposicional que no pertenece al conjunto de ´ atomos de G∧H. Por definici´ on, dicho conjunto es igual a la uni´ on del conjunto de ´ atomos de Gy el conjunto de ´ atomos de H. Por tanto, en particular pno pertenece al conjunto de ´ atomos de Gy, por hip´ otesis de inducci´ on, el valor de Gen la interpretaci´ on Acoincide con su valor en la interpretaci´ on A0. Por el mismo motivo, pno pertenece al conjunto de ´ atomos de Hy, por hip´ otesis de inducci´ on, el valor de Hes el mismo en las interpretaciones AyA0. Aclaradas estas observaciones, se tiene por definici´ on que el valor de la f´ ormula G∧Hen la interpretaci´ on A0es la conjunci´ on del valor de Gen A0y el valor de Hen A0. Por lo demostrado anteriormente seg´ un las hip´ otesis de inducci´ on, esto es igual a la conjunci´ on del valor de Gen Ay el valor de Hen A. Aplicando la definici´ on, esto es el valor de G∧Hen la interpretaci´ on A. Por tanto, queda probada la equivalencia en este caso. Sean las f´ ormulas GyHcumpliendo las hip´ otesis supuestas para el caso anterior. Veamos que el resultado se verifica para la f´ ormula G∨H. Sea puna variable proposicional que no pertenece al conjunto de ´ atomos de G∨H. Por definici´ on, dicho conjunto es la uni´ on de los conjuntos de ´ atomos de GyH. Por tanto, como se ha probado en el caso anterior, tenemos que pno pertenece al conjunto de ´ atomos de G. Por tanto, aplicando la hip´ otesis de inducci´ on se tiene que el valor de Gen la interpretaci´ on A coincide con su valor en la interpretaci´ on A0. An´ alogamente ocurre para la f´ ormula H como vimos en el caso anterior, de modo que pno pertenece al conjunto de ´ atomos de H. Por tanto, por hip´ otesis de inducci´ on, el valor de Hes el mismo en AyA0. Veamos la equivalencia. Por definici´ on tenemos que el valor de la f´ ormula G∨Hen la interpretaci´ on A0es la disyunci´ on entre el valor de Gen A0y el valor de Hen A0. Por lo probado anteriormente seg´ un las hip´ otesis de inducic´ on, esto es igual a la disyunci´ on entre el valor de Gen Ay el valor de Hen A. Por definici´ on, se verifica que es igual al valor de G∨Hen la interpretaci´ on A, como quer´ ıamos demostrar. 64 Cap´ ıtulo 2. Sem´ antica finally show A(p:=V)|= (F→G)←→ A |= (F→G) by this qed lemma p/∈atoms F =⇒(A(p:=V)) |=F←→ A |=F proof (induction F) case (Atom x) then show ?case by (rule irrelevant-atom-atomic) next case Bot then show ?case by (rule irrelevant-atom-bot) next case (Not F) then show ?case by (rule irrelevant-atom-not) next case (And F1 F2) then show ?case by (rule irrelevant-atom-and) next case (Or F1 F2) then show ?case by (rule irrelevant-atom-or) next case (Imp F1 F2) then show ?case by (rule irrelevant-atom-imp) qed Por ´ ultimo, su demostraci´ on autom´ atica. lemma irrelevant-atom: p/∈atoms F =⇒(A(p:=V)) |=F←→ A |=F by (induction F)simp-all Procedamos con el siguiente lema de la secci´ on. Lema 2.1.8 Si dos interpretaciones coinciden sobre el conjunto de ´atomos de una f´ormula, entonces dicha f´ormula tiene el mismo valor en ambas interpretaciones. Su formalizaci´ on en Isabelle es la siguiente. lemma ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F oops Vamos a probar el resultado. 2.1. Sem´ antica 65 Demostraci´on: La prueba sigue el esquema de inducci´ on sobre la estructura de las f´ ormulas. De este modo, procedamos con la demostraci´ on de cada caso. En primer lugar sea una f´ ormula at´ omica p, donde pes una variable proposicional cualquiera. Sean las interpretaciones A1yA2tales que toman los mismos valores sobre el conjunto de ´ atomos de p. Veamos que el valor de pen A1coincide con su valor en A2. Por definici´ on, el valor de pen la interpretaci´ on A1es A1(p). Como el conjunto de ´ atomos de pes {p}, se tiene por hip´ otesis que A1(p) = A2(p). Finalmente, aplicando la definici´ on, esto es igual al valor de la f´ ormula pen la interpretaci´ on A2, como quer´ ıamos probar. Consideremos ahora la f´ ormula ⊥y dos interpretaciones en las condiciones del enunciado. Es f´ acil observar que, como el valor de ⊥es Falso en cualquier interpretaci´ on, se tiene en particular el resultado. Sea una f´ ormula Ftal que, si dos interpretaciones coinciden sobre el conjunto de ´ atomos de F, entonces el valor de Fes el mismo en ambas interpretaciones. Sean dos interpretaciones cualesquiera A1yA2que toman los mismos valores sobre el conjunto de ´ atomos de ¬F. Vamos a probar que el valor de ¬Fen A1coincide con su valor en A2. Observemos que, como el conjunto de ´ atomos de Fy¬Fcoinciden, se tiene por hip´ otesis de inducci´ on que el valor de Fen A1coincide con su valor en A2. Por otro lado, por definici´ on, el valor de ¬Fen A1es la negaci´ on del valor de Fen A1. Por la observaci´ on anterior, esto es igual a la negaci´ on del valor de Fen A2que, por definici´ on, es el valor de ¬Fen A2, probando as´ ı el resultado. Consideremos las f´ ormulas FyGcon las mismas hip´ otesis que la f´ ormula del caso anterior. Sean las interpretaciones A1yA2tales que coinciden sobre el conjunto de ´ atomos de F∧G. Vamos a probar que el valor de F∧Gen A1es el mismo que en A2. Como el conjunto de ´ atomos de F∧Ges la uni´ on del conjunto de ´ atomos de Fy el conjunto de ´ atomos de G, tenemos que A1yA2coinciden sobre los elementos de dicha uni´ on. En particular, coinciden sobre los elementos del conjunto de ´ atomos de Fy, por hip´ otesis de inducci´ on, tenemos que el valor de Fen A1coincide con su valor en A2. Del mismo modo, las interpretaciones anteriores coinciden tambi´ en sobre los elementos del conjunto de ´ atomos de Gluego, aplicando an´ alogamente la hip´ otesis de inducci´ on, tenemos que el valor de Ges el mismo en las interpretaciones A1yA2. Veamos ahora que el valor de F∧Gtambi´ en coincide en dichas interpretaciones. Por definici´ on, el valor de F∧Gen A1es la conjunci´ on del valor de Fen A1y el valor de Gen A1. Por lo obtenido anteriormente por las hip´ otesis de inducci´ on, tenemos que esto es igual a la conjunci´ on del valor de Fen A2y el valor de Gen A2. Por ´ ultimo se tiene que esto es igual al valor de F∧Gen A2tras aplicar la definici´ on. Volvamos a considerar FyGen las condiciones anteriores y dos interpretaciones A1yA2que coinciden sobre el conjunto de ´ atomos de F∨G. Vamos a probar que el valor de dicha f´ ormula es el mismo en ambas interpretaciones. De manera an´ aloga al 66 Cap´ ıtulo 2. Sem´ antica caso anterior, como el conjunto de ´ atomos de F∨Ges la uni´ on del conjunto de ´ atomos de Fy el conjunto de ´ atomos de G, tenemos que las interpretaciones coinciden sobre los elementos de esta uni´ on. En particular, coinciden sobre el conjunto de ´ atomos de F. Por tanto, por hip´ otesis de inducci´ on, el valor de Fen A1coincide con su valor en A2. Igualmente obtenemos que las interpretaciones coinciden sobre el conjunto de ´ atomos de Gy, aplicando de nuevo hip´ otesis de inducci´ on, el valor de Ges el mismo en ambas interpretaciones. Por otra parte, por definici´ on tenemos que le valor de F∨Gen la interpretaci´ on A1es la disyunci´ on entre el valor de Fen A1y el valor de Gen A1. Por las observaciones anteriores derivadas de las hip´ otesis de inducci´ on, tenemos que esto es igual a la disyunci´ on entre el valor de Fen A2y el valor de Gen A2. Por definici´ on, esto es el valor de F∨Gen A2, como quer´ ıamos demostrar. Veamos el ´ ultimo caso de las f´ ormulas. Sean FyGf´ ormulas en las condiciones de los casos anteriores. Consideremos las interpretaciones A1yA2que coinciden sobre los elementos del conjunto de ´ atomos de F→G. Probemos que el valor de F→Ges el mismo en ambas interpretaciones. Por definici´ on, el conjunto de ´ atomos de F→Ges la uni´ on de los conjuntos de ´ atomos de FyG. Por tanto, dichas interpretaciones coinciden sobre los elementos de dicha uni´ on. Como hemos visto en casos anteriores, en particular coinciden sobre los ´ atomos de Fluego, por hip´ otesis de inducci´ on, el valor de Fen A1coincide con su valor en A2. An´ alogamente, las interpretaciones coinciden sobre los ´ atomos de Gy, por hip´ otesis de inducci´ on, el valor de Ges el mismo en ambas interpretaciones. Probemos que tambi´ en coincide el valor de F→Gen A1yA2. Por definici´ on, el valor de F→Gen A1es la implicaci´ on entre el valor de Fen A1y el valor de Gen A1. De esta manera, por las observaciones anteriores tenemos que esto es igual a la implicaci´ on entre el valor de Fen A2y el valor de Gen A2. Finalmente, por definici´ on, esto es el valor de F→Gen la interpretaci´ on A2, probando as´ ı el resultado.  Probemos ahora el lema de forma detallada en Isabelle, haciendo cada caso de la estructura de las f´ ormulas por separado y empleando lemas auxiliares sobre la pertenencia a los conjuntos de ´ atomos cuando sea necesario. lemma relevant-atoms-same-semantics-atomic-l1: x∈atoms (Atom x) proof show x∈ {x} by (simp only:singleton-iff ) next show {x} ⊆ atoms (Atom x) by (simp only:formula.set(1)) qed 2.1. Sem´ antica 67 lemma relevant-atoms-same-semantics-atomic: assumes ∀k∈atoms (Atom x).A1k=A2k shows A1|=Atom x ←→ A2|=Atom x proof − have A1|=Atom x =A1x by (simp only:formula-semantics.simps(1)) also have . . . =A2x using assms(1) by (simp only:relevant-atoms-same-semantics-atomic-l1) also have . . . =A2|=Atom x by (simp only:formula-semantics.simps(1)) finally show ?thesis by this qed Para las f´ ormulas at´ omicas, se observa el uso del lema auxiliar relevant-atoms-same-semantics-atomic-l. Sigamos con los siguientes casos. lemma relevant-atoms-same-semantics-bot: assumes ∀k∈atoms ⊥.A1k=A2k shows A1|=⊥ ←→ A2|=⊥ by (simp only:formula-semantics.simps(2)) lemma relevant-atoms-same-semantics-not: assumes ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F ∀k∈atoms (¬F).A1k=A2k shows A1|= (¬F)←→ A2|= (¬F) proof − have ∀k∈atoms F.A1k=A2kusing assms(2) by (simp only:formula.set(3)) then have H:A1|=F←→ A2|=F by (simp only:assms(1)) have A1|= (¬F)=(¬ A1|=F) by (simp only:formula-semantics.simps(3)) also have . . . = (¬ A2|=F) using Hby (rule arg-cong) also have . . . =A2|= (¬F) by (simp only:formula-semantics.simps(3)) finally show ?thesis by this qed 68 Cap´ ıtulo 2. Sem´ antica Para los casos de la f´ ormula ⊥y la negaci´ on ¬Fno han sido necesarios los lemas auxiliares pues, en el primer caso, el conjunto de ´ atomos es el vac´ ıo y, en el segundo caso, el conjunto de ´ atomos de ¬Fcoincide con el de F. Finalmente, introducimos los siguientes lemas auxiliares para facilitar las demostraciones detalladas en Isabelle de los casos correspondientes a las conectivas binarias. lemma forall-union1: assumes ∀x∈A∪B.P x shows ∀x∈A.P x proof (rule ballI) fix x assume x∈A then have x∈A∪B by (simp only:UnI1) then show P x by (simp only:assms) qed lemma forall-union2: assumes ∀x∈A∪B.P x shows ∀x∈B.P x proof (rule ballI) fix x assume x∈B then have x∈A∪B by (simp only:UnI2) then show P x by (simp only:assms) qed Empleando dichos resultados, veamos las demostraciones detalladas de los tres ´ ultimos casos. Despu´ es se mostrar´ a la demostraci´ on detallada del lema completo en Isabelle. lemma relevant-atoms-same-semantics-and: assumes ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F ∀k∈atoms G.A1k=A2k=⇒ A1|=G←→ A2|=G ∀k∈atoms (F∧G).A1k=A2k shows A1|= (F∧G)←→ A2|= (F∧G) proof − have H:∀k∈atoms F ∪atoms G.A1k=A2kusing assms(3) by (simp only:formula.set(4)) 2.1. Sem´ antica 69 then have ∀k∈atoms F.A1k=A2k by (rule forall-union1) then have H1:A1|=F←→ A2|=F by (simp only:assms(1)) have ∀k∈atoms G.A1k=A2k using Hby (rule forall-union2) then have H2:A1|=G←→ A2|=G by (simp only:assms(2)) have A1|=F∧G= (A1|=F∧ A1|=G) by (simp only:formula-semantics.simps(4)) also have . . . = (A2|=F∧ A2|=G) using H1 H2 by (rule arg-cong2) also have . . . =A2|=F∧G by (simp only:formula-semantics.simps(4)) finally show ?thesis by this qed lemma relevant-atoms-same-semantics-or: assumes ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F ∀k∈atoms G.A1k=A2k=⇒ A1|=G←→ A2|=G ∀k∈atoms (F∨G).A1k=A2k shows A1|= (F∨G)←→ A2|= (F∨G) proof − have H:∀k∈atoms F ∪atoms G.A1k=A2kusing assms(3) by (simp only:formula.set(5)) then have ∀k∈atoms F.A1k=A2k by (rule forall-union1) then have H1:A1|=F←→ A2|=F by (simp only:assms(1)) have ∀k∈atoms G.A1k=A2k using Hby (rule forall-union2) then have H2:A1|=G←→ A2|=G by (simp only:assms(2)) have A1|=F∨G= (A1|=F∨ A1|=G) by (simp only:formula-semantics.simps(5)) also have . . . = (A2|=F∨ A2|=G) using H1 H2 by (rule arg-cong2) also have . . . =A2|=F∨G by (simp only:formula-semantics.simps(5)) 70 Cap´ ıtulo 2. Sem´ antica finally show ?thesis by this qed lemma relevant-atoms-same-semantics-imp: assumes ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F ∀k∈atoms G.A1k=A2k=⇒ A1|=G←→ A2|=G ∀k∈atoms (F→G).A1k=A2k shows A1|= (F→G)←→ A2|= (F→G) proof − have H:∀k∈atoms F ∪atoms G.A1k=A2kusing assms(3) by (simp only:formula.set(6)) then have ∀k∈atoms F.A1k=A2k by (rule forall-union1) then have H1:A1|=F←→ A2|=F by (simp only:assms(1)) have ∀k∈atoms G.A1k=A2k using Hby (rule forall-union2) then have H2:A1|=G←→ A2|=G by (simp only:assms(2)) have A1|=F→G= (A1|=F−→ A1|=G) by (simp only:formula-semantics.simps(6)) also have . . . = (A2|=F−→ A2|=G) using H1 H2 by (rule arg-cong2) also have . . . =A2|=F→G by (simp only:formula-semantics.simps(6)) finally show ?thesis by this qed lemma ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F proof (induction F) case (Atom x) then show ?case by (rule relevant-atoms-same-semantics-atomic) next case Bot then show ?case by (rule relevant-atoms-same-semantics-bot) next case (Not F) then show ?case by (rule relevant-atoms-same-semantics-not) 2.2. Sem´ antica de f´ ormulas con conectivas generalizadas 71 next case (And F1 F2) then show ?case by (rule relevant-atoms-same-semantics-and) next case (Or F1 F2) then show ?case by (rule relevant-atoms-same-semantics-or) next case (Imp F1 F2) then show ?case by (rule relevant-atoms-same-semantics-imp) qed Su demostraci´ on autom´ atica es la siguiente. lemma relevant-atoms-same-semantics: ∀k∈atoms F.A1k=A2k=⇒ A1|=F←→ A2|=F by (induction F)simp-all 2.2 Sem´antica de f´ormulas con conectivas generalizadas En este apartado mostraremos varios resultados relativos a la sem´ antica de las f´ ormulas construidas con conectivas generalizadas. Lema 2.2.1 Una interpretaci´on es modelo de la conjunci´on generalizada de una lista de f´ormulas si y solo si es modelo de cada f´ormula de la lista. Su formalizaci´ on en Isabelle es la siguiente. lemma (A |=VFs)←→ (∀f∈set Fs.A |=f) oops Como podemos observar, en el enunciado de la derecha hemos empleado set para cambiar al tipo de los conjuntos la lista de f´ ormulas, pues esto permite emplear el cuantificador universal. Procedamos con la prueba del lema. Demostraci´on: La prueba se basa en el esquema de inducci´ on sobre listas. Para ello, demostraremos el resultado mediante cadenas de equivalencias en los siguientes casos. En primer lugar, lo probamos para la lista vac´ ıa de f´ ormulas. Sea la interpretaci´ on Atal que es modelo de la conjunci´ on generalizada de la lista vac´ ıa. Por definici´ on de la conjunci´ on generalizada, Aes modelo de ¬ ⊥. Aplicando la definici´ on del valor de una f´ ormula en una interpretaci´ on para el caso de la negaci´ on, tenemos que esto es 72 Cap´ ıtulo 2. Sem´ antica equivalente a que Ano es modelo de ⊥. An´ alogamente, como sabemos que el valor de ⊥es Falso en cualquier interpretaci´ on, se tiene que lo anterior es equivalente a ¬Falso, es decir, Verdadero. Por otro lado, por propiedades del conjunto vac´ ıo, se tiene que toda propiedad sobre sus elementos es verdadera. Por tanto, lo anterior es equivalente a decir que Aes modelo de todos los elementos del conjunto vac´ ıo. Es decir, Aes modelo de todos los elementos de la lista vac´ ıa, como quer´ ıamos demostrar. Consideramos ahora la interpretaci´ on Ay la lista de f´ ormulas Fs de modo que A es modelo de la conjunci´ on generalizada de Fs si y solo si es modelo de cada f´ ormula de Fs. Veamos ahora que se verifica la propiedad para la lista F#Fs formada al a˜ nadir la f´ ormula F. En primer lugar, si Aes modelo de la conjunci´ on generalizada de F#Fs, por definici´ on de dicha conjunci´ on, esto es equivalente a que Aes modelo de la conjunci´ on de Fy la conjunci´ on generalizada de Fs. Seg´ un el valor de una f´ ormula en una interpretaci´ on, esto es a su vez equivalente a la conjunci´ on de ”Aes modelo de F” y ”Aes modelo de la conjunci´ on generalizada de Fs”. Aplicando la hip´ otesis de inducci´ on sobre el segundo t´ ermino de la conjunci´ on, es equivalente a la conjunci´ on de ”Aes modelo de F”y”Aes modelo de toda f´ ormula del conjunto formado por los elementos de Fs”. Equivalentemente, Aes modelo de toda f´ ormula del conjunto formado por la uni´ on de {F}y el conjunto de los elementos de Fs. Es decir, Aes modelo de toda f´ ormula del conjunto formado por los elementos de F#Fs, probando as´ ı el resultado.  Veamos ahora su demostraci´ on detallada en Isabelle. Primero se probar´ an los dos casos correspondientes a la estructura de listas por separado. lemma BigAnd-semantics-nil:(A |=V[]) ←→ (∀f∈set [].A |=f) proof− have (A |=V[]) = A |= (¬⊥) by (simp only:BigAnd.simps(1)) also have . . . = (¬ A |=⊥) by (simp only:formula-semantics.simps(3)) also have . . . = (¬False) by (simp only:formula-semantics.simps(2)) also have . . . =True by (simp only:not-False-eq-True) also have . . . = (∀f∈∅.A |=f) by (simp only:ball-empty) also have . . . = (∀f∈set [].A |=f) by (simp only:list.set) finally show ?thesis by this qed 2.2. Sem´ antica de f´ ormulas con conectivas generalizadas 73 Para el caso de la lista formada a˜ nadiendo un elemento, vamos a emplear el siguiente lema auxiliar. lemma Bigprop1:(∀x∈({a} ∪ B).P x)=(P a ∧(∀x∈B.P x)) by (simp only:ball-simps(7) insert-is-Un[THEN sym]) Se trata de una adaptaci´ on del s´ eptimo apartado del lema ball-simps en Isabelle, para adecuarlo a nuestro caso particular. (∀x∈insert a B.P x)←→ (P a ∧(∀x∈B.P x)) (ball-simps(7)) Para ello, empleamos el lema insert-is-Un seguido de [THEN sym]como hemos hecho anteriormente. Procedamos, as´ ı, con la demostraci´ on del caso del lema correspondiente. Por ´ ultimo, mostraremos tambi´ en su demostraci´ on detallada completa. lemma BigAnd-semantics-cons: assumes (A |=VFs)←→ (∀f∈set Fs.A |=f) shows (A |=V(F#Fs)) ←→ (∀f∈set (F#Fs).A |=f) proof − have (A |=V(F#Fs)) = A |=F∧VFs by (simp only:BigAnd.simps(2)) also have . . . = (A |=F∧ A |=VFs) by (simp only:formula-semantics.simps(4)) also have . . . = (A |=F∧(∀f∈set Fs.A |=f)) by (simp only:assms) also have . . . = (∀f∈({F} ∪ set Fs).A |=f) by (simp only:Bigprop1) also have . . . = (∀f∈set (F#Fs).A |=f) by (simp only:set-insert) finally show ?thesis by this qed lemma (A |=VFs)←→ (∀f∈set Fs.A |=f) proof (induction Fs) case Nil then show ?case by (rule BigAnd-semantics-nil) next case (Cons a Fs) then show ?case by (rule BigAnd-semantics-cons) 80 Cap´ ıtulo 2. Sem´ antica que se diferencia por el contexto. En Isabelle/HOL es imprescindible aclarar la diferencia. Mostremos alg´ un ejemplo de f´ ormula que sea consecuencia l´ ogica de un conjunto. notepad begin fix A:: nat valuation have {Atom 1 →Atom 2,Atom 2 →Atom 3} ||= (Atom 1 →Atom 3) by (simp add:entailment-def ) end Llegamos as´ ı al ´ ultimo lema de la secci´ on. Lema 2.3.5 ⊥es consecuencia l´ogica de un conjunto si y solo si el conjunto es insatisfacible. Su formalizaci´ on en Isabelle es la siguiente. lemma Γ||=⊥ ←→ ¬ sat Γ oops Comencemos las demostraciones del resultado. Demostraci´on: Vamos a probar la doble implicaci´ on mediante una cadena de equivalencias. Sea un conjunto de f´ ormulas Γtal que la f´ ormula ⊥es consecuencia l´ ogica de dicho conjunto. Por definici´ on, esto es equivalente a que toda interpretaci´ on que sea modelo de Γes, a su vez, modelo de ⊥. Como el valor de ⊥es Falso en cualquier interpretaci´ on, ninguna interpretaci´ on es modelo suyo. Por tanto, por la hip´ otesis inicial, se verifica que ninguna interpretaci´ on es modelo del conjunto Γ. Es decir, no existe ninguna interpretaci´ on que sea modelo de dicho conjunto. Seg´ un la definici´ on, esto es equivalente a que el conjunto Γes insatisfacible, como quer´ ıamos demostrar.  Procedamos con las pruebas en Isabelle/HOL. lemma Γ||=⊥ ←→ ¬ sat Γ proof − have Γ||=⊥= (∀ A.((∀G∈Γ.A |=G)−→ A |=⊥)) by (simp only:entailment-def ) also have . . . = (∀ A.((∀G∈Γ.A |=G)−→ False)) by (simp only:formula-semantics.simps(2)) 2.3. Sem´ antica de conjuntos de f´ ormulas 81 also have . . . = (∀ A.¬(∀G∈Γ.A |=G)) by (simp only:not-def ) also have . . . = (¬(∃ A.∀G∈Γ.A |=G)) by (simp only:not-ex) also have . . . = (¬sat Γ) by (simp only:sat-def ) finally show ?thesis by this qed Finalmente su demostraci´ on autom´ atica es la siguiente. lemma entail-sat: Γ||=⊥ ←→ ¬ sat Γ unfolding sat-def entailment-def by simp 82 Cap´ ıtulo 2. Sem´ antica Cap´ıtulo 3 Lema de Hintikka 3.1 Conjuntos de Hintikka y propiedades b´asicas En esta secci´ on presentaremos un tipo de conjuntos de f´ ormulas: los conjuntos de Hintikka. Probaremos finalmente que todo conjunto de Hintikka es satisfacible. Definici´on 3.1.1 Se llama conjunto de Hintikka a todo conjunto de f´ormulas S que verifica las siguientes condiciones: 1. ⊥/∈S. 2. Dada p una f´ormula at´omica cualquiera, no se tiene simult´aneamente que p∈S y ¬p∈S. 3. Si F ∧G∈S, entonces F ∈SyG∈S. 4. Si F ∨G∈S, entonces F ∈SoG∈S. 5. Si F →G∈S, entonces ¬F∈SoG∈S. 6. Si ¬(¬F)∈S, entonces F ∈S. 7. Si ¬(F∧G)∈S, entonces ¬F∈S o ¬G∈S. 8. Si ¬(F∨G)∈S, entonces ¬F∈S y ¬G∈S. 9. Si ¬(F→G)∈S, entonces F ∈S y ¬G∈S. En Isabelle se formaliza mediante el tipo definition como sigue. definition Hintikka S ≡ 83 84 Cap´ ıtulo 3. Lema de Hintikka (⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S)) A continuaci´ on ilustramos con un ejemplo de conjunto de f´ ormulas de Hintikka. notepad begin have Hintikka {Atom 0 ∧((¬(Atom 1)) →Atom 2), ((¬(Atom 1)) →Atom 2), Atom 0,¬(¬(Atom 1)),Atom 1} unfolding Hintikka-def by simp end En contraposici´ on, el siguiente conjunto de f´ ormulas no es de Hintikka, pues no cumple la segunda condici´ on de la definici´ on anterior. notepad begin have ¬Hintikka {Atom 0 ∧((¬(Atom 1)) →Atom 2), ((¬(Atom 1)) →Atom 2), Atom 0,¬(¬(Atom 1)),Atom 1,¬(Atom 1)} unfolding Hintikka-def by auto end En adelante presentaremos una serie de lemas auxiliares derivados de la definici´ on de conjunto de Hintikka que nos facilitar´ an posteriormente las demostraciones en Isabelle/HOL. El primer lema expresa que la conjunci´ on de las nueve condiciones de la definici´ on anterior es una condici´ on necesaria para que un conjunto sea de Hintikka. lemma auxEq: assumes Hintikka S 3.1. Conjuntos de Hintikka y propiedades b´ asicas 85 shows ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) proof − have Hintikka S = ( ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S)) using Hintikka-def by (simp only:atomize-eq) then show ?thesis using assms by (rule iffD1) qed Asimismo presentaremos nueve lemas correspondientes a cada condici´ on de la definici´ on de conjunto de Hintikka. Lema 3.1.2 Si S es un conjunto de Hintikka, ⊥/∈S. Lema 3.1.3 Sea S un conjunto de Hintikka. Si p es una f´ormula at´omica tal que p ∈S, entonces ¬p/∈S. Lema 3.1.4 Sea S un conjunto de Hintikka. Si F ∧G∈S, entonces F ∈SyG∈S. Lema 3.1.5 Sea S un conjunto de Hintikka. Si F ∨G∈S, entonces F ∈SoG∈S. Lema 3.1.6 Sea S un conjunto de Hintikka. Si F →G∈S, entonces ¬F∈SoG∈S. Lema 3.1.7 Sea S un conjunto de Hintikka. Si ¬(¬F)∈S, entonces F ∈S. Lema 3.1.8 Sea S un conjunto de Hintikka. Si ¬(F∧G)∈S, entonces ¬F∈S o ¬G∈S. 86 Cap´ ıtulo 3. Lema de Hintikka Lema 3.1.9 Sea S un conjunto de Hintikka. Si ¬(F∨G)∈S, entonces ¬F∈S y ¬G∈S. Lema 3.1.10 Sea S un conjunto de Hintikka. Si ¬(F→G)∈S, entonces F ∈S y ¬G∈S. Como se puede observar, los lemas anteriores se corresponden con cada condici´ on necesaria de la definici´ on de conjunto de Hintikka. De este modo, la prueba de estos resultados se obtiene directamente de dicha definici´ on al suponer que Ses un conjunto de Hintikka. Su formalizaci´ on y demostraci´ on en Isabelle/HOL son las siguientes. lemma assumes Hintikka S shows ⊥/∈S proof − have ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) using assms by (rule auxEq) thus ⊥/∈Sby (rule conjunct1) qed lemma Hintikka-l1: Hintikka S =⇒ ⊥ /∈S using Hintikka-def by blast lemma assumes Hintikka S shows Atom k ∈S−→ ¬(Atom k)/∈S proof (rule impI) assume H:Atom k ∈S have ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) 3.1. Conjuntos de Hintikka y propiedades b´ asicas 87 ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) using assms by (rule auxEq) then have (∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) by (iprover elim:conjunct2 conjunct1) then have ∀k.Atom k ∈S−→ ¬(Atom k)/∈S by (simp only:not-def ) then have Atom k ∈S−→ ¬(Atom k)/∈S by (rule allE) thus ¬(Atom k)/∈S using Hby (rule mp) qed lemma Hintikka-l2: Hintikka S =⇒(Atom k ∈S−→ ¬(Atom k)/∈S) by (smt Hintikka-def) lemma assumes Hintikka S shows F∧G∈S−→ F∈S∧G∈S proof (rule impI) assume F∧G∈S have ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) using assms by (rule auxEq) then have ∀F G.F∧G∈S−→ F∈S∧G∈S by (iprover elim:conjunct2 conjunct1) then have F∧G∈S−→ F∈S∧G∈S by (iprover elim:allE) thus F∈S∧G∈S using hF∧G∈Siby (rule mp) 88 Cap´ ıtulo 3. Lema de Hintikka qed lemma Hintikka-l3: Hintikka S =⇒(F∧G∈S−→ F∈S∧G∈S) by (smt Hintikka-def) lemma assumes Hintikka S shows F∨G∈S−→ F∈S∨G∈S proof (rule impI) assume H:F∨G∈S have ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) using assms by (rule auxEq) then have ∀F G.F∨G∈S−→ F∈S∨G∈S by (iprover elim:conjunct2 conjunct1) then have F∨G∈S−→ F∈S∨G∈S by (iprover elim:allE) thus F∈S∨G∈S using Hby (rule mp) qed lemma Hintikka-l4: Hintikka S =⇒(F∨G∈S−→ F∈S∨G∈S) by (smt Hintikka-def) lemma assumes Hintikka S shows F→G∈S−→ ¬F∈S∨G∈S proof (rule impI) assume H:F→G∈S have ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) 3.1. Conjuntos de Hintikka y propiedades b´ asicas 89 ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) using assms by (rule auxEq) then have ∀F G.F→G∈S−→ ¬F∈S∨G∈S by (iprover elim:conjunct2 conjunct1) then have F→G∈S−→ ¬F∈S∨G∈S by (iprover elim:allE) thus ¬F∈S∨G∈S using Hby (rule mp) qed lemma Hintikka-l5: Hintikka S =⇒(F→G∈S−→ ¬F∈S∨G∈S) by (smt Hintikka-def) lemma assumes Hintikka S shows (¬(¬F)∈S−→ F∈S) proof (rule impI) assume H:¬(¬F)∈S have ⊥/∈S ∧(∀k.Atom k ∈S−→ ¬(Atom k)∈S−→ False) ∧(∀F G.F∧G∈S−→ F∈S∧G∈S) ∧(∀F G.F∨G∈S−→ F∈S∨G∈S) ∧(∀F G.F→G∈S−→ ¬F∈S∨G∈S) ∧(∀F.¬(¬F)∈S−→ F∈S) ∧(∀F G.¬(F∧G)∈S−→ ¬F∈S∨¬G∈S) ∧(∀F G.¬(F∨G)∈S−→ ¬F∈S∧¬G∈S) ∧(∀F G.¬(F→G)∈S−→ F∈S∧¬G∈S) using assms by (rule auxEq) then have ∀F.¬(¬F)∈S−→ F∈S by (iprover elim:conjunct2 conjunct1) then have ¬(¬F)∈S−→ F∈S by (rule allE) thus F∈S 96 Cap´ ıtulo 3. Lema de Hintikka de un predicado, introducir la negaci´ on de una conjunci´ on o disyunci´ on de dicho predicado con otro cualquiera. lemma notConj1: assumes ¬P shows ¬(P∧Q) proof (rule notI) assume P∧Q then have P by (rule conjunct1) show False using assms hPiby (rule notE) qed lemma notConj2: assumes ¬Q shows ¬(P∧Q) proof (rule notI) assume P∧Q then have Q by (rule conjunct2) show False using assms hQiby (rule notE) qed lemma notDisj: assumes ¬P ¬Q shows ¬(P∨Q) proof (rule notI) assume P∨Q then show False proof (rule disjE) assume P show False using assms(1)hPiby (rule notE) next assume Q show False using assms(2)hQiby (rule notE) qed 3.1. Conjuntos de Hintikka y propiedades b´ asicas 97 qed Comencemos las pruebas detalladas de los casos correspondientes a las conectivas binarias. Una vez terminadas, se mostrar´ a la prueba detallada del lema completo. lemma Hintikka-l10-and: assumes Hintikka S =⇒¬G∈S−→ G/∈S Hintikka S =⇒¬H∈S−→ H/∈S Hintikka S shows ¬(G∧H)∈S−→ G∧H/∈S proof (rule impI) assume ¬(G∧H)∈S have ¬(G∧H)∈S−→ ¬G∈S∨¬H∈S using assms(3)by (rule Hintikka-l7) then have ¬G∈S∨¬H∈S using h¬(G∧H)∈Siby (rule mp) then show G∧H/∈S proof (rule disjE) assume ¬G∈S have ¬G∈S−→ G/∈S using assms(1)assms(3)by this then have G/∈S using h¬G∈Siby (rule mp) then have ¬(G∈S∧H∈S) by (rule notConj1) have G∧H∈S−→ G∈S∧H∈S using assms(3)by (rule Hintikka-l3) thus G∧H/∈S using h¬(G∈S∧H∈S)iby (rule mt) next assume ¬H∈S have ¬H∈S−→ H/∈S using assms(2)assms(3)by this then have H/∈S using h¬H∈Siby (rule mp) then have ¬(G∈S∧H∈S) by (rule notConj2) have G∧H∈S−→ G∈S∧H∈S using assms(3)by (rule Hintikka-l3) thus G∧H/∈S using h¬(G∈S∧H∈S)iby (rule mt) qed 98 Cap´ ıtulo 3. Lema de Hintikka qed lemma Hintikka-l10-or: assumes Hintikka S =⇒¬G∈S−→ G/∈S Hintikka S =⇒¬H∈S−→ H/∈S Hintikka S shows ¬(G∨H)∈S−→ G∨H/∈S proof (rule impI) assume ¬(G∨H)∈S have ¬(G∨H)∈S−→ (¬G∈S∧¬H∈S) using assms(3)by (rule Hintikka-l8) then have C:¬G∈S∧¬H∈S using h¬(G∨H)∈Siby (rule mp) then have ¬G∈S by (rule conjunct1) have ¬G∈S−→ G/∈S using assms(1)assms(3)by this then have G/∈S using h¬G∈Siby (rule mp) have ¬H∈S using Cby (rule conjunct2) have ¬H∈S−→ H/∈S using assms(2)assms(3)by this then have H/∈S using h¬H∈Siby (rule mp) have ¬(G∈S∨H∈S) using hG/∈Si hH/∈Siby (rule notDisj) have (G∨H∈S−→ G∈S∨H∈S) using assms(3)by (rule Hintikka-l4) thus G∨H/∈S using h¬(G∈S∨H∈S)iby (rule mt) qed lemma Hintikka-l10-imp: assumes Hintikka S =⇒¬G∈S−→ G/∈S Hintikka S =⇒¬H∈S−→ H/∈S Hintikka S shows ¬(G→H)∈S−→ G→H/∈S proof (rule impI) assume ¬(G→H)∈S 3.1. Conjuntos de Hintikka y propiedades b´ asicas 99 have ¬(G→H)∈S−→ (G∈S∧¬H∈S) using assms(3)by (rule Hintikka-l9) then have C:G∈S∧¬H∈S using h¬(G→H)∈Siby (rule mp) then have G∈S by (rule conjunct1) then have ¬(G/∈S) by (rule contrapos-pn) have ¬G∈S−→ G/∈S using assms(1)assms(3)by this then have ¬G/∈S using h¬(G/∈S)iby (rule mt) have ¬H∈S using Cby (rule conjunct2) have ¬H∈S−→ H/∈S using assms(2)assms(3)by this then have H/∈S using h¬H∈Siby (rule mp) have ¬(¬G∈S∨H∈S) using h¬G/∈Si hH/∈Siby (rule notDisj) have G→H∈S−→ ¬G∈S∨H∈S using assms(3)by (rule Hintikka-l5) thus G→H/∈S using h¬(¬G∈S∨H∈S)iby (rule mt) qed lemma Hintikka S =⇒¬F∈S−→ F/∈S proof (induct F) case (Atom x) then show ?case by (rule Hintikka-l10-atom) next case Bot then show ?case by (rule Hintikka-l10-bot) next case (Not F) then show ?case by (rule Hintikka-l10-not) next case (And F1 F2) then show ?case by (rule Hintikka-l10-and) next 100 Cap´ ıtulo 3. Lema de Hintikka case (Or F1 F2) then show ?case by (rule Hintikka-l10-or) next case (Imp F1 F2) then show ?case by (rule Hintikka-l10-imp) qed Por ´ ultimo, su demostraci´ on autom´ atica es la que sigue. lemma Hintikka-l10: Hintikka S =⇒¬F∈S−→ F/∈S apply (induct F) apply (meson Hintikka-l2) apply (simp add:Hintikka-l1) using Hintikka-l6 apply blast using Hintikka-l3 Hintikka-l7 apply blast apply (smt Hintikka-def) using Hintikka-l5 Hintikka-l9 by blast 3.2 Lema de Hintikka Una vez definida la noci´ on de conjunto de Hintikka y conocidas las propiedades que se deducen de ella, nuestro objetivo ser´ a demostrar que todo conjunto de Hintikka es satisfacible. Por definici´ on, para probar que un conjunto es satisfacible basta hallar una interpretaci´ on que sea modelo suyo. De este modo, definimos el siguiente tipo de interpretaciones. Definici´on 3.2.1 Sea un conjunto de f´ormulas cualquiera. Se define la interpretaci´on asociada al conjunto como aquella que devuelve Verdadero sobre las variables proposicionales cuya correspondiente f´ormula at´omica pertence al conjunto, y Falso en caso contrario. En Isabelle se formalizar´ a mediante el tipo definition como se expone a continuaci´ on. definition setValuation :: (0a formula)set ⇒0a valuation where setValuation S ≡λk.Atom k ∈S Presentemos ahora ejemplos del valor de ciertas f´ ormulas en la interpretaci´ on asociada a los conjuntos siguientes. notepad 3.2. Lema de Hintikka 101 begin have (setValuation {Atom 0 ∧((¬(Atom 1)) →Atom 2), ((¬(Atom 1)) →Atom 2),Atom 0, ¬(¬(Atom 1)),Atom 1})|=Atom 1 →Atom 0 =True unfolding setValuation-def by simp have (setValuation {Atom 3 ∨(¬(Atom 1)), ¬(¬(Atom 6))})|=Atom 2 ∨Atom 6 =False unfolding setValuation-def by simp end Previamente a probar que los conjuntos de Hintikka son satisfacibles y con el fin de facilitar dicha demostraci´ on, introducimos el siguiente resultado. Lema 3.2.2 La interpretaci´on asociada a un conjunto de Hintikka es modelo de una f´ormula si esta pertenece al conjunto. Adem´as, dicha interpretaci´on no es modelo de una f´ormula si su negaci´on pertenece al conjunto. Su formalizaci´ on en Isabelle es la siguiente. lemma Hintikka S =⇒(F∈S−→ isModel (setValuation S)F) ∧(¬F∈S−→ (¬(isModel (setValuation S)F))) oops Procedamos a la demostraci´ on del resultado. Demostraci´on: Sea Sun conjunto de Hintikka y denotemos por ISa la interpretaci´ on asociada a S. Sea Funa f´ ormula, hay que probar lo siguiente: (F∈S=⇒ IS|=F)∧(¬F∈S=⇒ IS6|=F) La prueba se realiza por inducci´ on sobre la estructura de las f´ ormulas proposicionales. Veamos los distintos casos. Caso 1: F=p, f´ ormula at´ omica. Si p∈S, entonces IS(p) = True por definici´ on de la interpretaci´ on asociada a S. Por otro lado, si ¬p∈S, entonces p/∈Spor ser Sde Hintikka. Por tanto, IS(p) = False por definici´ on de IS. Caso 2: F=⊥ 102 Cap´ ıtulo 3. Lema de Hintikka Si ⊥ ∈ S, como por definici´ on de conjunto de Hintikka sabemos que ⊥/∈S, se tendr´ ıa una contradicci´ on. Luego, en particular, tenemos el resultado. Por otra parte, si ¬ ⊥ ∈ S,ISno es modelo de ⊥pues el valor de ⊥es Falso en cualquier interpretaci´ on. Caso 3: F=¬G, y Gverifica la hip´ otesis de inducci´ on. Es decir, HI:(G∈S=⇒ IS|=G)∧(¬G∈S=⇒ IS6|=G) Probemos que (F∈S=⇒ IS|=F)∧(¬F∈S=⇒ IS6|=F) En efecto, F∈S =⇒ ¬ G∈S =⇒ IS(G)= False (HI) =⇒ IS(¬G)= True =⇒ IS|=F An´ alogamente, ¬F∈S =⇒ ¬¬ G∈S =⇒G∈S(S es conjunto de Hintikka) =⇒ IS(G)= True (HI) =⇒ IS(¬G)= False =⇒ IS(F)= False =⇒ IS6|=F Caso 4: F=G∧Hy tanto Gcomo Hverifican la hip´ otesis de inducci´ on. Es decir, se verifican HI1: (G∈S=⇒ IS|=G)∧(¬G∈S=⇒ IS6|=G) HI2: (H∈S=⇒ IS|=H)∧(¬H∈S=⇒ IS6|=H) Probemos que (F∈S=⇒ IS|=F)∧(¬F∈S=⇒ IS6|=F) En efecto, F∈S =⇒G∧H∈S =⇒G∈S∧H∈S(S es conjunto de Hintikka) =⇒ IS|=G∧ IS|=H(HI1 y HI2) =⇒ IS(G)∧ IS(H)= True =⇒ IS(G∧H)= True =⇒ IS(F)= True =⇒ IS|=F 3.2. Lema de Hintikka 103 Por otra parte, ¬F∈S =⇒ ¬ (G∧H)∈S =⇒ ¬ G∈S∨ ¬ H∈S(S es conjunto de Hintikka) =⇒ IS6|=G∨ IS6|=H(HI1 y HI2) =⇒ ¬ (IS|=G∧ IS|=H) =⇒ IS(G)∧ IS(H)= False =⇒ IS(G∧H)= False =⇒ IS(F)= False =⇒ IS6|=F Caso 5: F=G∨Hy tanto Gcomo Hverifican la hip´ otesis de inducci´ on. Es decir, se verifican HI1: (G∈S=⇒ IS|=G)∧(¬G∈S=⇒ IS6|=G) HI2: (H∈S=⇒ IS|=H)∧(¬H∈S=⇒ IS6|=H) Probemos que (F∈S=⇒ IS|=F)∧(¬F∈S=⇒ IS6|=F) En efecto, F∈S =⇒G∨H∈S =⇒G∈S∨H∈S(S es conjunto de Hintikka) =⇒ IS|=G∨ IS|=H(HI1 y HI2) =⇒ IS(G)∨ IS(H)= True =⇒ IS(G∨H)= True =⇒ IS(F)= True =⇒ IS|=F Por otra parte, ¬F∈S =⇒ ¬ (G∨H)∈S =⇒ ¬ G∈S∧ ¬ H∈S(S es conjunto de Hintikka) =⇒ IS6|=G∧ IS6|=H(HI1 y HI2) =⇒ ¬ (IS|=G∨ IS|=H) =⇒ IS(G)∨ IS(H)= False =⇒ IS(G∨H)= False =⇒ IS(F)= False =⇒ IS6|=F 104 Cap´ ıtulo 3. Lema de Hintikka Caso 6: F=G−→ Hy tanto Gcomo Hverifican la hip´ otesis de inducci´ on. Es decir, se verifican HI1: (G∈S=⇒ IS|=G)∧(¬G∈S=⇒ IS6|=G) HI2: (H∈S=⇒ IS|=H)∧(¬H∈S=⇒ IS6|=H) Probemos que (F∈S=⇒ IS|=F)∧(¬F∈S=⇒ IS6|=F) En efecto, F∈S =⇒G−→ H∈S =⇒ ¬ G∈S∨H∈S(S es conjunto de Hintikka) Veamos que IS|=Fconsiderando ambos casos de la disyunci´ on anterior. ¬G∈S =⇒ IS6|=G(HI1) =⇒ IS|=G−→ IS|=H =⇒ IS(G)−→ IS(H)= True =⇒ IS(G−→ H)= True =⇒ IS(F)= True =⇒ IS|=F H∈S =⇒ IS|=H(HI2) =⇒ IS|=G−→ IS|=H =⇒ IS(G)−→ IS(H)= True =⇒ IS(G−→ H)= True =⇒ IS(F)= True =⇒ IS|=F Probando el resultado para este caso. Por otra parte, ¬F∈S =⇒ ¬ (G−→ H)∈S =⇒G∈S∧ ¬ H∈S(S es conjunto de Hintikka) =⇒ IS|=G∧ IS6|=H(HI1 y HI2) =⇒ ¬ (IS|=G−→ IS|=H) =⇒ IS(G)−→ IS(H)= False =⇒ IS(G−→ H)= False =⇒ IS(F)= False =⇒ IS6|=F 3.2. Lema de Hintikka 105 Queda probada la segunda afirmaci´ on. Con lo que termina la demostraci´ on.  Una vez terminada la prueba anterior, procedemos a las distintas demostraciones del lema mediante Isabelle/HOL. En primer lugar aparecer´ an las demostraciones detalladas de cada caso de la estructura de las f´ ormulas por separado. Posteriormente se mostrar´ a la prueba detallada del lema completo. lemma assumes Hintikka S shows Vx.(Atom x ∈S−→ isModel (setValuation S) (Atom x)) ∧ (¬(Atom x)∈S−→ ¬ isModel (setValuation S) (Atom x)) proof (rule conjI) show Vx.Atom x ∈S−→ isModel (setValuation S) (Atom x) proof fix x assume Atom x ∈S hence (setValuation S)x by (simp only:setValuation-def ) hence setValuation S |=Atom x by (simp only:formula-semantics.simps(1)) thus isModel (setValuation S) (Atom x) by (simp only:isModel-def ) qed next show Vx.¬(Atom x)∈S−→ ¬ isModel (setValuation S) (Atom x) proof fix x assume ¬(Atom x)∈S have ¬(Atom x)∈S−→ Atom x /∈S using assms by (rule Hintikka-l10) then have Atom x /∈S using h¬(Atom x)∈Siby (rule mp) also have (¬(Atom x ∈S)) = (¬(setValuation S)x) by (simp only:setValuation-def ) also have . . . = (¬((setValuation S)|= (Atom x))) by (simp only:formula-semantics.simps(1)) also have . . . = (¬isModel (setValuation S) (Atom x)) by (simp only:isModel-def ) 112 Cap´ ıtulo 3. Lema de Hintikka by (simp only:isModel-def ) next assume F2 ∈S have F2 ∈S−→ isModel (setValuation S)F2 using assms(3)by (rule conjunct1) then have isModel (setValuation S)F2 using hF2 ∈Siby (rule mp) then have (setValuation S)|=F2 by (simp only:isModel-def ) then have (setValuation S)|=F1 ∨(setValuation S)|=F2 by (rule disjI2) then have (setValuation S)|= (F1 ∨F2) by (simp only:formula-semantics.simps(5)) thus isModel (setValuation S) (F1 ∨F2) by (simp only:isModel-def ) qed qed next show VF1 F2.¬(F1 ∨F2)∈S−→ ¬ isModel (setValuation S) (F1 ∨F2) proof (rule impI) fix F1 F2 assume ¬(F1 ∨F2)∈S have ¬(F1 ∨F2)∈S−→ ¬F1 ∈S∧¬F2 ∈S using assms(1)by (rule Hintikka-l8) then have C:¬F1 ∈S∧¬F2 ∈S using h¬(F1 ∨F2)∈Siby (rule mp) then have ¬F1 ∈S by (rule conjunct1) have ¬F1 ∈S−→ ¬ isModel (setValuation S)F1 using assms(2)by (rule conjunct2) then have ¬isModel (setValuation S)F1 using h¬F1 ∈Siby (rule mp) also have (¬isModel (setValuation S)F1)=(¬(setValuation S)|=F1) by (simp only:isModel-def ) finally have D1:¬(setValuation S)|=F1 by this have ¬F2 ∈S using Cby (rule conjunct2) have ¬F2 ∈S−→ ¬ isModel (setValuation S)F2 using assms(3)by (rule conjunct2) 3.2. Lema de Hintikka 113 then have ¬isModel (setValuation S)F2 using h¬F2 ∈Siby (rule mp) also have (¬isModel (setValuation S)F2)=(¬(setValuation S)|=F2) by (simp only:isModel-def ) finally have D2:¬(setValuation S)|=F2 by this have ¬((setValuation S)|=F1 ∨(setValuation S)|=F2) using D1 D2 by (rule notDisj) also have (¬((setValuation S)|=F1 ∨(setValuation S)|=F2)) = (¬(setValuation S)|= (F1 ∨F2)) by (simp only:formula-semantics.simps(5)) also have . . . = (¬isModel (setValuation S) (F1 ∨F2)) by (simp only:isModel-def ) finally show ¬isModel (setValuation S) (F1 ∨F2) by this qed qed lemma Hl2-5: assumes Hintikka S shows VF1 F2. (F1 ∈S−→ isModel (setValuation S)F1)∧ (¬F1 ∈S−→ ¬ isModel (setValuation S)F1) =⇒ (F2 ∈S−→ isModel (setValuation S)F2)∧ (¬F2 ∈S−→ ¬ isModel (setValuation S)F2) =⇒ (F1 ∨F2 ∈S−→ isModel (setValuation S) (F1 ∨F2)) ∧ (¬(F1 ∨F2)∈S−→ ¬ isModel (setValuation S) (F1 ∨F2)) by (smt Hintikka-def assms isModel-def formula-semantics.simps(5)) lemma assumes Hintikka S VF1.(F1 ∈S−→ isModel (setValuation S)F1)∧ (¬F1 ∈S−→ ¬ isModel (setValuation S)F1) VF2.(F2 ∈S−→ isModel (setValuation S)F2)∧ (¬F2 ∈S−→ ¬ isModel (setValuation S)F2) shows VF1 F2.(F1 →F2 ∈S−→ isModel (setValuation S) (F1 →F2)) ∧(¬(F1 →F2)∈S−→ ¬ isModel (setValuation S) (F1 →F2)) proof (rule conjI) show VF1 F2.F1 →F2 ∈S−→ isModel (setValuation S) (F1 →F2) 114 Cap´ ıtulo 3. Lema de Hintikka proof (rule impI) fix F1 F2 assume F1 →F2 ∈S have F1 →F2 ∈S−→ ¬F1 ∈S∨F2 ∈S using assms(1)by (rule Hintikka-l5) then have ¬F1 ∈S∨F2 ∈S using hF1 →F2 ∈Siby (rule mp) then show isModel (setValuation S) (F1 →F2) proof (rule disjE) assume ¬F1 ∈S have ¬F1 ∈S−→ ¬ isModel (setValuation S)F1 using assms(2)by (rule conjunct2) then have ¬isModel (setValuation S)F1 using h¬F1 ∈Siby (rule mp) also have (¬isModel (setValuation S)F1)=(¬(setValuation S)|=F1) by (simp only:isModel-def ) finally have ¬(setValuation S)|=F1 by this have (setValuation S)|=F1 −→ (setValuation S)|=F2 proof (rule impI) assume (setValuation S)|=F1 show (setValuation S)|=F2 using h¬(setValuation S)|=F1i h(setValuation S)|=F1iby (rule notE) qed then have (setValuation S)|= (F1 →F2) by (simp only:formula-semantics.simps(6)) thus ?thesis by (simp only:isModel-def ) next assume F2 ∈S have F2 ∈S−→ isModel (setValuation S)F2 using assms(3)by (rule conjunct1) then have isModel (setValuation S)F2 using hF2 ∈Siby (rule mp) then have (setValuation S)|=F2 by (simp only:isModel-def ) have (setValuation S)|=F1 −→ (setValuation S)|=F2 proof (rule impI) assume (setValuation S)|=F1 show (setValuation S)|=F2 3.2. Lema de Hintikka 115 using h(setValuation S)|=F2iby this qed then have (setValuation S)|= (F1 →F2) by (simp only:formula-semantics.simps(6)) thus ?thesis by (simp only:isModel-def ) qed qed next show VF1 F2.¬(F1 →F2)∈S−→ ¬ isModel (setValuation S) (F1 →F2) proof (rule impI) fix F1 F2 assume ¬(F1 →F2)∈S have ¬(F1 →F2)∈S−→ F1 ∈S∧¬F2 ∈S using assms(1)by (rule Hintikka-l9) then have C:F1 ∈S∧¬F2 ∈S using h¬(F1 →F2)∈Siby (rule mp) then have F1 ∈S by (rule conjunct1) have F1 ∈S−→ isModel (setValuation S)F1 using assms(2)by (rule conjunct1) then have isModel (setValuation S)F1 using hF1 ∈Siby (rule mp) then have (setValuation S)|=F1 by (simp only:isModel-def ) have ¬F2 ∈S using Cby (rule conjunct2) have ¬F2 ∈S−→ ¬ isModel (setValuation S)F2 using assms(3)by (rule conjunct2) then have ¬isModel (setValuation S)F2 using h¬F2 ∈Siby (rule mp) also have (¬isModel (setValuation S)F2)=(¬(setValuation S)|=F2) by (simp only:isModel-def ) finally have ¬(setValuation S)|=F2 by this have ¬((setValuation S)|=F1 −→ (setValuation S)|=F2) proof (rule notI) assume (setValuation S)|=F1 −→ (setValuation S)|=F2 then have (setValuation S)|=F2 using h(setValuation S)|=F1iby (rule mp) 116 Cap´ ıtulo 3. Lema de Hintikka show False using h¬(setValuation S)|=F2i h(setValuation S)|=F2iby (rule notE) qed also have (¬((setValuation S)|=F1 −→ (setValuation S)|=F2)) = (¬(setValuation S)|= (F1 →F2)) by (simp only:formula-semantics.simps(6)) also have . . . = (¬isModel (setValuation S) (F1 →F2)) by (simp only:isModel-def ) finally show ¬isModel (setValuation S) (F1 →F2) by this qed qed lemma Hl2-6: assumes Hintikka S shows VF1 F2. (F1 ∈S−→ isModel (setValuation S)F1)∧ (¬F1 ∈S−→ ¬ isModel (setValuation S)F1) =⇒ (F2 ∈S−→ isModel (setValuation S)F2)∧ (¬F2 ∈S−→ ¬ isModel (setValuation S)F2) =⇒ (F1 →F2 ∈S−→ isModel (setValuation S) (F1 →F2)) ∧ (¬(F1 →F2)∈S−→ ¬ isModel (setValuation S) (F1 →F2)) by (meson Hintikka-l5 Hintikka-l9 assms isModel-def formula-semantics.simps(6)) lemma Hintikkas-lemma-l2: assumes Hintikka S shows (F∈S−→ isModel (setValuation S)F) ∧(¬F∈S−→ (¬(isModel (setValuation S)F))) proof (induct F) fix x show (Atom x ∈S−→ isModel (setValuation S) (Atom x)) ∧ (¬(Atom x)∈S−→ ¬ isModel (setValuation S) (Atom x)) using assms by (rule Hl2-1) next show (⊥ ∈ S−→ isModel (setValuation S)⊥)∧ (¬⊥ ∈ S−→ ¬ isModel (setValuation S)⊥) using assms by (rule Hl2-2) next fix F show (F∈S−→ isModel (setValuation S)F)∧ 3.2. Lema de Hintikka 117 (¬F∈S−→ ¬ isModel (setValuation S)F) =⇒ (¬F∈S−→ isModel (setValuation S) (¬F)) ∧ (¬(¬F)∈S−→ ¬ isModel (setValuation S) (¬F)) using assms by (rule Hl2-3) next fix F1 F2 show (F1 ∈S−→ isModel (setValuation S)F1)∧ (¬F1 ∈S−→ ¬ isModel (setValuation S)F1) =⇒ (F2 ∈S−→ isModel (setValuation S)F2)∧ (¬F2 ∈S−→ ¬ isModel (setValuation S)F2) =⇒ (F1 ∧F2 ∈S−→ isModel (setValuation S) (F1 ∧F2)) ∧ (¬(F1 ∧F2)∈S−→ ¬ isModel (setValuation S) (F1 ∧F2)) using assms by (rule Hl2-4) next fix F1 F2 show (F1 ∈S−→ isModel (setValuation S)F1)∧ (¬F1 ∈S−→ ¬ isModel (setValuation S)F1) =⇒ (F2 ∈S−→ isModel (setValuation S)F2)∧ (¬F2 ∈S−→ ¬ isModel (setValuation S)F2) =⇒ (F1 ∨F2 ∈S−→ isModel (setValuation S) (F1 ∨F2)) ∧ (¬(F1 ∨F2)∈S−→ ¬ isModel (setValuation S) (F1 ∨F2)) using assms by (rule Hl2-5) next fix F1 F2 show (F1 ∈S−→ isModel (setValuation S)F1)∧ (¬F1 ∈S−→ ¬ isModel (setValuation S)F1) =⇒ (F2 ∈S−→ isModel (setValuation S)F2)∧ (¬F2 ∈S−→ ¬ isModel (setValuation S)F2) =⇒ (F1 →F2 ∈S−→ isModel (setValuation S) (F1 →F2)) ∧ (¬(F1 →F2)∈S−→ ¬ isModel (setValuation S) (F1 →F2)) using assms by (rule Hl2-6) qed Para concluir, demostremos el Lema de Hintikka empleando el resultado anterior. Teorema 3.2.3 (Lema de Hintikka) Todo conjunto de Hintikka es satisfacible. Demostraci´on: Consideremos un conjunto de f´ ormulas Stal que sea un conjunto de Hintikka. Queremos demostrar que Ses satisfacible, es decir, que tiene alg´ un modelo. En otras palabras, debemos hallar una interpretaci´ on que sea modelo de S. 118 Cap´ ıtulo 3. Lema de Hintikka En primer lugar, probemos que la interpretaci´ on asociada a Ses modelo de S. Por definici´ on de modelo de un conjunto, basta comprobar que es modelo de toda f´ ormula perteneciente al mismo. Fijada una f´ ormula cualquiera, hemos visto anteriormente que la interpretaci´ on asociada a Ses modelo de la f´ ormula si esta pertenece al conjunto. Por tanto, dicha interpretaci´ on es, en efecto, modelo de todas las f´ ormulas que pertenecen a S. Luego la interpretaci´ on asociada a Ses modelo de S. En conclusi´ on, hemos hallado una interpretaci´ on que es modelo del conjunto. Por lo tanto, Ses satisfacible, como se quer´ ıa probar.  Por su parte, la prueba detallada en Isabelle emplea el lema auxiliar Hintikka-model. Con ´ el se demuestra la primera parte del lema de Hintikka: dado un conjunto de Hintikka, la interpretaci´ on asociada al conjunto es modelo del mismo. lemma Hintikka-model: assumes Hintikka S shows isModelSet (setValuation S)S proof − have ∀F.(F∈S−→ isModel (setValuation S)F) proof (rule allI) fix F have (F∈S−→ isModel (setValuation S)F) ∧(¬F∈S−→ (¬(isModel (setValuation S)F))) using assms by (rule Hintikkas-lemma-l2) thus F∈S−→ isModel (setValuation S)F by (rule conjunct1) qed thus isModelSet (setValuation S)S by (simp only:modelSet) qed Finalmente, las pruebas detallada y autom´ atica del Lema de Hintikka en Isabelle/HOL. theorem assumes Hintikka S shows sat S proof − have isModelSet (setValuation S)S using assms by (rule Hintikka-model) then have ∃ A.isModelSet AS by (simp only:exI) thus sat S by (simp only:satAlt) 3.2. Lema de Hintikka 119 qed theorem Hintikkaslemma: assumes Hintikka S shows sat S using Hintikka-model assms satAlt by blast 120 Cap´ ıtulo 3. Lema de Hintikka Ap´endice A Lemas de HOL usados En este glosario se recoge la lista de los lemas y reglas usadas indicando la p´ agina del libro de HOL donde se encuentran. A.1 La base de l´ogica de primer orden (2) En Isabelle corresponde a la teor´ ıa HOL.thy A.1.1 L´ogica primitiva (2.1) A.1.1.1 Conectivas y cuantificadores definidos (2.1.2) • (p.34) ¬P≡P−→ False (not-def) A.1.1.2 Axiomas y definiciones b´asicas (2.1.4) • (p.36) P Q P−→ Q(impI) • (p.36) (P−→ Q)∧P Q(mp) 121 128 Ap´ endice A. Lemas de HOL usados • (p.188) Q−→ P ¬P−→ ¬ Q(not-mono) A.5 Nociones sobre funciones (9) En Isabelle, la teor´ ıa de funciones se corresponde con Fun.thy. A.5.1 Actualizaci´on de funciones (9.6) • (p.212) f(a:=b)=(λx.if x=athen belse f x)(fun-upd-def) • (p.213) z6=x (f(x:=y)) z=f z (fun-upd-other) A.6 Ret´ıculos completos (10) En Isabelle corresponde a la teor´ ıa Complete-Lattices.thy. A.6.1 Ret´ıculos completos en conjuntos (10.6) A.6.1.1 Uni´on (10.6.3) • (p.238) S∅=∅(Union-empty) A.7 Conjuntos finitos (18) A continuaci´ on se muestran resultados relativos a la teor´ ıa Finite-Set.thy. A.7.1 Predicado de conjuntos finitos (18.1) • (p.419) finite A (finite) A.8. Composici´ on de functores naturales acotados (33) 129 A.7.2 Finitud y operaciones de conjuntos comunes (18.2) • (p.422) finite F ∧finite G finite (F∪G)(finite-UnI) • (p.423) finite ({a} ∪ A) = finite A (finite-insert) A.8 Composici´on de functores naturales acotados (33) En esta secci´ on se muestran resultados pertenecientes a la teor´ ıa de composici´ on de functores naturales acotados de Isabelle BNFComposition.thy. • (p.718) S(f ‘ ({a} ∪ B)) = f a ∪S(f‘B)(Union-image-insert) A.9 El tipo de datos de la listas finitas (66) En esta secci´ on se muestran resultados sobre listas finitas dentro de la teor´ ıa de listas de Isabelle List.thy. • (p.1169) [] = ∅ x21 ·x22 ={x21} ∪ x22 (list.set) A.9.1 Funciones b´asicas de procesamiento de listas (66.1) A.9.1.1 Funci´on set • (p.1195) xs @ys =xs ∪ys (set-append) 130 Ap´ endice A. Lemas de HOL usados Bibliograf´ıa [1] Jos´ e A. Alonso. Temas de “L´ ogica matem´ atica y fundamentos (2018–19)”. Technical report, Univ. de Sevilla, 2019. En https://www.cs.us.es/∼jalonso/cursos/lmf-18/ temas.php. [2] Lawrence C. Paulson Computer Laboratory. Old Introduction to Isabelle. Technical report, University of Cambridge, 2019. En https://isabelle.in.tum.de/ website-Isabelle2019/dist/Isabelle2019/doc/intro.pdf. [3] Christian Doczkal and Gert Smolka. Constructive Formalization of Classical Modal Logic. Technical report, 2011. En http://www.cs.ru.nl/∼spitters/coqw files/ paper 1.pdf. [4] M. Fitting. First-order Logic and Automated Theorem Proving. Graduate texts in computer science. Springer, 1996. [5] L.T.F Gamut. Introducci´on a la l´ogica. Editorial Universitaria de Buenos Aires, 2002. [6] John Harrison. An overview of automated reasoning. Technical report, 2014. En https://www.cl.cam.ac.uk/∼jrh13/slides/lyon-03feb14/slides.pdf. [7] Angeliki Koutsoukou-Argyraki. Formalising Mathematics -in praxis, 2019. En https://www.researchgate.net/publication/334549483 formalising mathematis -in praxis a mathematician’s first experiences with isabellehol and the why and how of getting started. [8] Dr. Kevin P. Lee. A Guide to Writing Mathematics. En http://cc.kangwon.ac.kr/ ∼kimoon/me/me-132/math-writing.pdf. [9] F. F´ elix Lara Mart´ ın. Temas 3 de “Ciencias de la computaci´ on (2018–19)”: Funciones recursivas. Technical report, Univ. de Sevilla, 2019. En http://www.cs.us. es/cursos/cc-2018/Tema-03.pdf. [10] Julius Michaelis and Tobias Nipkow. Propositional Proof Systems. Technical report, 2020. En https://www.isa-afp.org/browser info/current/AFP/Propositional Proof Systems/document.pdf. 131 132 Bibliograf´ ıa [11] Tobias Nipkow. What’s in Main, 2019. En https://isabelle.in.tum.de/ website-Isabelle2019/dist/Isabelle2019/doc/main.pdf. [12] Lawrence C. Paulson Tobias Nipkow and Markus Wenzel. Isabelle/HOL: A proof assistant for Higher–Order Logic. Lecture Notes in Computer Science, Vol. 2283, Springer–Verlag, 2019. En https://isabelle.in.tum.de/website-Isabelle2019/dist/ Isabelle2019/doc/tutorial.pdf. [13] Floris van Doorn. Propositional Calculus in Coq. Technical report, 2015. En https: //arxiv.org/abs/1503.08744. [14] Makarius Wenzel. The Isabelle/Isar Implementation, 2019. En https://isabelle.in. tum.de/website-Isabelle2019/dist/Isabelle2019/doc/implementation.pdf. [15] Makarius Wenzel. The Isabelle/Isar Reference Manual, 2019. En https://isabelle. in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/isar-ref.pdf.