La teoría de modelos finitos es una subárea de la teoría de modelos . La teoría de modelos es la rama de la lógica que estudia la relación entre un lenguaje formal (sintaxis) y sus interpretaciones (semántica). La teoría de modelos finitos es una restricción de la teoría de modelos a las interpretaciones sobre estructuras finitas , que tienen un universo finito.
Dado que muchos teoremas centrales de la teoría de modelos no se sostienen cuando se restringen a estructuras finitas, la teoría de modelos finitos es bastante diferente de la teoría de modelos en sus métodos de prueba. Los resultados centrales de la teoría de modelos clásica que fallan para estructuras finitas bajo la teoría de modelos finitos incluyen el teorema de compacidad , el teorema de completitud de Gödel y el método de ultraproductos para lógica de primer orden (FO). Si bien la teoría de modelos tiene muchas aplicaciones para el álgebra matemática , la teoría de modelos finitos se convirtió en un instrumento "inusualmente efectivo" [1] en la ciencia de la computación. En otras palabras: "En la historia de la lógica matemática, la mayor parte del interés se ha concentrado en las estructuras infinitas. [...] Sin embargo, los objetos que las computadoras tienen y sostienen son siempre finitos. Para estudiar la computación necesitamos una teoría de estructuras finitas". [2] Por lo tanto, las principales áreas de aplicación de la teoría de modelos finitos son: teoría de la complejidad descriptiva , teoría de bases de datos y teoría del lenguaje formal .
Una pregunta motivadora común en la teoría de modelos finitos es si una clase dada de estructuras puede describirse en un lenguaje dado. Por ejemplo, uno podría preguntar si la clase de grafos cíclicos puede distinguirse entre grafos mediante una oración FO, que también puede formularse como si la ciclicidad es expresable mediante FO.
Una única estructura finita siempre puede axiomatizarse en lógica de primer orden , donde axiomatizada en un lenguaje L significa descrita de forma única hasta el isomorfismo por una única oración L. De manera similar, cualquier colección finita de estructuras finitas siempre puede axiomatizarse en lógica de primer orden. Algunas, pero no todas, colecciones infinitas de estructuras finitas también pueden axiomatizarse mediante una única oración de primer orden.
¿Es un lenguaje L lo suficientemente expresivo como para axiomatizar una única estructura finita S ?
Una estructura como (1) en la figura puede describirse mediante oraciones FO en la lógica de gráficos como
Sin embargo, estas propiedades no axiomatizan la estructura, ya que para la estructura (1') las propiedades anteriores también se cumplen, aunque las estructuras (1) y (1') no son isomorfas.
De manera informal, la pregunta es si al agregar suficientes propiedades, estas propiedades juntas describen exactamente (1) y no son válidas (todas juntas) para ninguna otra estructura (salvo el isomorfismo).
En el caso de una estructura finita única, siempre es posible describir con precisión la estructura mediante una única oración FO. El principio se ilustra aquí para una estructura con una relación binaria y sin constantes:
todo para la misma tupla , produciendo la oración FO .
El método de describir una estructura única mediante una oración de primer orden se puede extender fácilmente a cualquier número fijo de estructuras. Se puede obtener una descripción única mediante la disyunción de las descripciones para cada estructura. Por ejemplo, para dos estructuras y con oraciones definitorias y esto sería
Por definición, un conjunto que contiene una estructura infinita queda fuera del área que aborda la FMT. Nótese que las estructuras infinitas nunca pueden discriminarse en FO, debido al teorema de Löwenheim-Skolem , que implica que ninguna teoría de primer orden con un modelo infinito puede tener un modelo único hasta el isomorfismo.
El ejemplo más famoso es probablemente el teorema de Skolem , que sostiene que existe un modelo aritmético contable y no estándar.
¿Es un lenguaje L lo suficientemente expresivo para describir exactamente (hasta el isomorfismo) aquellas estructuras finitas que tienen cierta propiedad P ?
Las descripciones dadas hasta ahora especifican el número de elementos del universo. Desafortunadamente, la mayoría de los conjuntos de estructuras interesantes no están restringidos a un tamaño determinado, como todos los grafos que son árboles, están conectados o son acíclicos. Por lo tanto, discriminar un número finito de estructuras es de especial importancia.
En lugar de una declaración general, lo que sigue es un esbozo de una metodología para diferenciar entre estructuras que se pueden y no se pueden discriminar.
Queremos demostrar que la propiedad de que el tamaño de una estructura ordenada A = (A, ≤) es par, no se puede expresar en FO.
(*) Nótese que se ha omitido la prueba del resultado del juego Ehrenfeucht–Fraïssé , ya que no es el foco principal aquí.
Glebskiĭ et al. (1969) e, independientemente, Fagin (1976) demostraron una ley cero-uno para oraciones de primer orden en modelos finitos; la prueba de Fagin utilizó el teorema de compacidad . Según este resultado, cada oración de primer orden en una firma relacional es casi siempre verdadera o casi siempre falsa en estructuras finitas . Es decir, sea S una oración fija de primer orden y elija una estructura aleatoria con dominio , de manera uniforme entre todas las estructuras con dominio . Entonces, en el límite cuando n tiende a infinito, la probabilidad de que G n modele S tenderá a cero o a uno:
El problema de determinar si una oración dada tiene una probabilidad que tiende a cero o a uno es PSPACE-completo . [3]
Se ha realizado un análisis similar para lógicas más expresivas que la lógica de primer orden. Se ha demostrado que la ley 0-1 es válida para oraciones en FO(LFP) , lógica de primer orden aumentada con un operador de punto fijo mínimo, y de manera más general para oraciones en la lógica infinitaria , que permite conjunciones y disyunciones potencialmente arbitrarias. Otra variante importante es la ley 0-1 no etiquetada, donde en lugar de considerar la fracción de estructuras con dominio , se considera la fracción de clases de isomorfismo de estructuras con n elementos. Esta fracción está bien definida, ya que dos estructuras isomorfas cualesquiera satisfacen las mismas oraciones. La ley 0-1 no etiquetada también es válida para y, por lo tanto, en particular para FO(LFP) y la lógica de primer orden. [4]
Un objetivo importante de la teoría de modelos finitos es la caracterización de las clases de complejidad por el tipo de lógica necesaria para expresar los lenguajes que las componen. Por ejemplo, PH , la unión de todas las clases de complejidad en la jerarquía polinómica, es precisamente la clase de lenguajes expresables por enunciados de lógica de segundo orden . Esta conexión entre la complejidad y la lógica de las estructuras finitas permite transferir fácilmente los resultados de un área a otra, facilitando nuevos métodos de prueba y proporcionando evidencia adicional de que las principales clases de complejidad son de alguna manera "naturales" y no están ligadas a las máquinas abstractas específicas utilizadas para definirlas.
En concreto, cada sistema lógico produce un conjunto de consultas que se pueden expresar en él. Las consultas, cuando se limitan a estructuras finitas, corresponden a los problemas computacionales de la teoría de la complejidad tradicional.
Algunas clases de complejidad bien conocidas son capturadas por lenguajes lógicos de la siguiente manera:
Un fragmento sustancial de SQL (a saber, lo que es efectivamente álgebra relacional ) se basa en lógica de primer orden (que se puede traducir más precisamente en cálculo relacional de dominio mediante el teorema de Codd ), como ilustra el siguiente ejemplo: Piense en una tabla de base de datos "GIRLS" con las columnas "FIRST_NAME" y "LAST_NAME". Esto corresponde a una relación binaria, digamos G(f, l) en FIRST_NAME × LAST_NAME. La consulta FO , que devuelve todos los apellidos donde el nombre es 'Judy', se vería en SQL así:
Seleccione APELLIDO de CHICAS donde NOMBRE = 'Judy'
Tenga en cuenta que aquí asumimos que todos los apellidos aparecen solo una vez (o deberíamos usar SELECT DISTINCT ya que asumimos que las relaciones y las respuestas son conjuntos, no bolsas).
A continuación, queremos realizar una declaración más compleja. Por lo tanto, además de la tabla "GIRLS", tenemos una tabla "BOYS" también con las columnas "FIRST_NAME" y "LAST_NAME". Ahora queremos consultar los apellidos de todas las niñas que tengan el mismo apellido que al menos uno de los niños. La consulta FO es y la declaración SQL correspondiente es:
seleccione NOMBRE , APELLIDO de NIÑAS donde APELLIDO EN ( seleccione APELLIDO de NIÑOS );
Observe que para expresar "∧" introdujimos el nuevo elemento de lenguaje "IN" con una declaración de selección posterior. Esto hace que el lenguaje sea más expresivo a cambio de una mayor dificultad para aprender e implementar. Esta es una compensación común en el diseño de lenguajes formales. La forma que se muestra arriba ("IN") no es ni mucho menos la única para extender el lenguaje. Una forma alternativa es, por ejemplo, introducir un operador "JOIN", es decir:
seleccionar distinto g.NOMBRE , g.APELLIDO de NIÑAS g , NIÑOS b donde g.APELLIDO = b.APELLIDO ;
La lógica de primer orden es demasiado restrictiva para algunas aplicaciones de bases de datos, por ejemplo, debido a su incapacidad para expresar clausura transitiva . Esto ha llevado a que se agreguen construcciones más poderosas a los lenguajes de consulta de bases de datos, como el recursivo WITH en SQL:1999 . Por lo tanto, se han estudiado lógicas más expresivas, como las lógicas de punto fijo , en la teoría de modelos finitos debido a su relevancia para la teoría y las aplicaciones de bases de datos.
Los datos narrativos no contienen relaciones definidas. Por lo tanto, la estructura lógica de las consultas de búsqueda de texto se puede expresar en lógica proposicional , como en:
("Java" Y NO "isla") O ("C#" Y NO "música")
Tenga en cuenta que los desafíos en la búsqueda de texto completo son diferentes a los de la consulta de bases de datos, como la clasificación de los resultados.
{{cite journal}}
: CS1 maint: bot: original URL status unknown (link)