Teoría de modelos finitos

La teoría de modelos finitos es una subdisciplina 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 restringe la teoría de modelos a las interpretaciones en estructuras finitas , que poseen un universo finito.

Dado que muchos teoremas centrales de la teoría de modelos no se cumplen al restringirse a estructuras finitas, la teoría de modelos finitos difiere considerablemente de la teoría de modelos clásica en sus métodos de demostración. Entre los resultados centrales de la teoría de modelos clásica que fallan para estructuras finitas bajo la teoría de modelos finitos se incluyen el teorema de compacidad , el teorema de completitud de Gödel y el método de ultraproductos para la lógica de primer orden (FO). Todas estas invalidezes se derivan del teorema de Trakhtenbrot . ^{[ 1 ]}

Si bien la teoría de modelos tiene muchas aplicaciones en el álgebra matemática , la teoría de modelos finitos se convirtió en un instrumento "singularmente eficaz" ^{[ 2 ]} en la informática. 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 almacenan son siempre finitos. Para estudiar la computación, necesitamos una teoría de estructuras finitas". ^{[ 3 ]} Por lo tanto, las principales áreas de aplicación de la teoría de modelos finitos son: la teoría de la complejidad descriptiva , la teoría de bases de datos y la teoría de lenguajes formales .

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, se podría preguntar si la clase de grafos cíclicos puede distinguirse entre otros grafos mediante una oración de primer orden (FO), lo que también puede formularse como preguntar si la ciclicidad es expresable en FO.

Una única estructura finita siempre puede axiomatizarse en lógica de primer orden, donde axiomatizarse en un lenguaje L significa que se describe de forma única, salvo isomorfismo, mediante una única oración en L. De igual modo, cualquier colección finita de estructuras finitas siempre puede axiomatizarse en lógica de primer orden. Algunas colecciones infinitas de estructuras finitas, pero no todas, también pueden axiomatizarse mediante una única oración de primer orden.

Caracterización de una sola estructura

¿ Es un lenguaje L suficientemente expresivo como para axiomatizar una única estructura finita S ?

Problema

Una estructura como (1) en la figura puede describirse mediante sentencias FO en la lógica de grafos como

1. Cada nodo tiene una arista hacia otro nodo:${\displaystyle \forall _{x}\exists _{y}G(x,y).}$
2. Ningún nodo tiene una arista que lo conecte consigo mismo:${\displaystyle \forall _ {x,y}(G(x,y)\Rightarrow x\neq y).}$
3. Existe al menos un nodo que está conectado a todos los demás :${\displaystyle \exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).}$

Sin embargo, estas propiedades no axiomatizan la estructura, ya que para la estructura (1') también se cumplen las propiedades anteriores, pero 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 son válidas (todas juntas) para ninguna otra estructura (salvo isomorfismo).

Acercarse

Para una única estructura finita, siempre es posible describirla con precisión mediante una única oración FO. El principio se ilustra aquí para una estructura con una relación binaria.${\displaystyle R}$y sin constantes. Para ello, introducimos variables de primer orden.${\displaystyle x_{1},\dots ,x_{n}}$que se interpretan como el${\displaystyle n}$elementos de la estructura. A continuación, presentamos las cuatro fórmulas siguientes:

1. ${\displaystyle \varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})}$dice que hay al menos${\displaystyle n}$elementos;
2. ${\displaystyle \varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)}$dice que hay como máximo${\displaystyle n}$elementos;
3. ${\displaystyle \varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})}$establece cada borde de la relación${\displaystyle R}$;
4. ${\displaystyle \varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})}$establece cada no-arista de la relación${\displaystyle R}$.

Finalmente, la estructura se describe mediante la oración FO.${\displaystyle \exists _{x_{1}}\dots \exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})}$.

Extensión a un número fijo de estructuras

El método de describir una única estructura finita mediante una sentencia de primer orden puede extenderse 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 finitas${\displaystyle A}$y${\displaystyle B}$con oraciones definitorias${\displaystyle \varphi _{A}}$y${\displaystyle \varphi _{B}}$esto sería

${\displaystyle \varphi _{A}\lor \varphi _{B}.}$

Extensión a una estructura infinita

Por definición, un conjunto que contiene una estructura infinita queda fuera del ámbito que abarca la Teoría de la Estructura de Primer Orden (FMT). Cabe destacar que las estructuras infinitas nunca pueden distinguirse en la Teoría de Primer Orden (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 salvo isomorfismo.

El ejemplo más famoso es probablemente el teorema de Skolem , que establece que existe un modelo no estándar numerable de la aritmética.

Caracterización de una clase de estructuras

¿ Es un lenguaje L suficientemente expresivo como para describir con exactitud (salvo isomorfismo) aquellas estructuras finitas que poseen cierta propiedad P ?

Problema

Las descripciones dadas hasta ahora especifican el número de elementos del universo. Desafortunadamente, la mayoría de los conjuntos de estructuras más interesantes no se limitan a un tamaño determinado, como todos los grafos que son árboles, conexos o acíclicos. Por lo tanto, resulta de suma importancia distinguir un número finito de estructuras.

Acercarse

En lugar de una afirmación general, a continuación se presenta un esbozo de una metodología para diferenciar entre estructuras que pueden y no pueden distinguirse.

1. La idea central es que, siempre que se quiera comprobar si una propiedad P puede expresarse en FO, se eligen las estructuras A y B , donde A posee P y B no. Si para A y B se cumplen las mismas proposiciones de FO, entonces P no puede expresarse en FO. En resumen:

   ${\displaystyle A\in P,B\not \in P}$y${\displaystyle A\equiv B,}$

   dónde${\displaystyle A\equiv B}$es una abreviatura de${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$para todas las oraciones FO α , y P representa la clase de estructuras con la propiedad P.
2. La metodología considera una cantidad numerable de subconjuntos del lenguaje, cuya unión forma el lenguaje mismo. Por ejemplo, para FO consideremos las clases FO[ m ] para cada m . Para cada m, entonces debe demostrarse la idea central anterior. Es decir:

   ${\displaystyle A\in P,B\not \in P}$y${\displaystyle A\equiv _{m}B}$

   con un par${\displaystyle A,B}$para cada${\displaystyle m}$y α (en ≡) de FO[ m ]. Puede ser apropiado elegir las clases FO[ m ] para formar una partición del lenguaje.
3. Una forma común de definir FO[ m ] es mediante el rango de cuantificadores qr( α ) de una fórmula FO α , que expresa la profundidad del anidamiento de cuantificadores . Por ejemplo, para una fórmula en forma normal prenexa , qr es simplemente el número total de sus cuantificadores. Entonces, FO[ m ] se puede definir como todas las fórmulas FO α con qr( α ) ≤ m (o, si se desea una partición, como aquellas fórmulas FO con rango de cuantificadores igual a m ).
4. Por lo tanto, todo se reduce a demostrar${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$en los subconjuntos FO[ m ]. El enfoque principal aquí es utilizar la caracterización algebraica proporcionada por los juegos de Ehrenfeucht-Fraïssé . De manera informal, estos toman un único isomorfismo parcial en A y B y lo extienden m veces, para probar o refutar${\displaystyle A\equiv _{m}B}$, dependiendo de quién gane el partido.

Ejemplo

Queremos demostrar que la propiedad de que el tamaño de una estructura ordenada A = (A, ≤) sea par, no se puede expresar en FO.

1. La idea es elegir A ∈ EVEN y B ∉ EVEN , donde EVEN es la clase de todas las estructuras de tamaño par.
2. Comenzamos con dos estructuras ordenadas A ₂ y B ₂ con universos A ₂ = {1, 2, 3, 4} y B ₂ = {1, 2, 3}. Obviamente A ₂ ∈ EVEN y B ₂ ∉ EVEN .
3. Para m = 2, en un juego de Ehrenfeucht-Fraïssé de 2 movimientos en A ₂ y B ₂ el duplicador siempre gana, y por lo tanto A ₂ y B ₂ no se pueden discriminar en FO[2], es decir${\displaystyle \mathbf {A} _{2}\models \alpha \iff \mathbf {B} _{2}\models \alpha }$para cada α ∈ FO[2] .
4. A continuación, debemos aumentar la escala de las estructuras incrementando m . Por ejemplo, para m = 3 debemos encontrar A ₃ y B ₃ tales que el duplicador siempre gane el juego de 3 movimientos. Esto se puede lograr con A ₃ = {1, ..., 8} y B ₃ = {1, ..., 7}. De forma más general, podemos elegir Am ₌ {1, ..., 2m ^} y Bm ₌ {1, ..., 2m ⁻ 1 }; para cualquier m, el duplicador siempre gana el juego de m movimientos para este par de estructuras*.
5. Por lo tanto, incluso en estructuras ordenadas finitas no se puede expresar en FO.

Glebskiĭ et al. (1969) e, independientemente, Fagin (1976) demostraron una ley cero-uno para oraciones de primer orden en modelos finitos; la demostración de Fagin utilizó el teorema de compacidad . Según este resultado, cada oración de primer orden en una signatura relacional${\displaystyle \sigma }$es casi siempre verdadero o casi siempre falso en un número finito de casos.${\displaystyle \sigma }$-estructuras. Es decir, sea S una oración fija de primer orden y elijamos una estructura aleatoria.${\displaystyle \sigma }$-estructura${\displaystyle G_{n}}$con dominio${\displaystyle \{1,\dots ,n\}}$, uniformemente entre todos${\displaystyle \sigma }$-estructuras con dominio${\displaystyle \{1,\dots ,n\}}$. Entonces, en el límite cuando n tiende a infinito, la probabilidad de que G _n modele S tenderá a cero o a uno:

${\displaystyle \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.}$

El problema de determinar si una oración dada tiene una probabilidad que tiende a cero o a uno es PSPACE-completo . ^{[ 4 ]}

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 se cumple para sentencias en FO(LFP) , lógica de primer orden aumentada con un operador de punto fijo mínimo y, de forma más general, para sentencias en la lógica infinitaria.${\displaystyle L_{\infty \omega }^{\omega }}$, lo que permite conjunciones y disyunciones potencialmente arbitrariamente largas. Otra variante importante es la ley 0-1 sin etiquetar, donde en lugar de considerar la fracción de estructuras con dominio${\displaystyle \{1,\dots ,n\}}$, se considera la fracción de clases de isomorfismo de estructuras con n elementos. Esta fracción está bien definida, ya que cualesquiera dos estructuras isomorfas satisfacen las mismas proposiciones. La ley 0-1 sin etiquetar también se cumple para${\displaystyle L_{\infty \omega }^{\omega }}$y por lo tanto en particular para FO(LFP) y lógica de primer orden. ^{[ 5 ]}

Un objetivo importante de la teoría de modelos finitos es la caracterización de las clases de complejidad según 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 mediante 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 demostración y aportando 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 puede expresarse en él. Estas consultas, cuando se restringen a estructuras finitas, corresponden a los problemas computacionales de la teoría de la complejidad tradicional.

Algunos lenguajes lógicos representan clases de complejidad bien conocidas de la siguiente manera:

• En presencia de un orden lineal, la lógica de primer orden con un operador de cierre conmutativo y transitivo añadido produce L , problemas resolubles en espacio logarítmico.
• En presencia de un orden lineal, la lógica de primer orden con un operador de cierre transitivo produce NL , los problemas resolubles en el espacio logarítmico no determinista.
• En presencia de un orden lineal, la lógica de primer orden con un operador de punto fijo mínimo da P , los problemas resolubles en tiempo polinomial determinista.
• En todas las estructuras finitas (independientemente de si están ordenadas), la lógica existencial de segundo orden da NP ( teorema de Fagin ). ^{[ 6 ]}

• Trakhtenbrot 1950 : fallo del teorema de completitud en lógica de primer orden.
• Scholz 1952: caracterización de espectros en lógica de primer orden
• Fagin 1974 : el conjunto de todas las propiedades expresables en lógica existencial de segundo orden es precisamente la clase de complejidad NP.
• Chandra, Harel 1979/80: extensión de lógica de primer orden de punto fijo para lenguajes de consulta de bases de datos capaces de expresar cierre transitivo -> consultas como objetos centrales de FMT
• Immerman , Vardi 1982: la lógica de punto fijo sobre estructuras ordenadas captura PTIME -> complejidad descriptiva ( teorema de Immerman–Szelepcsényi )
• Ebbinghaus , Flum 1995: primer libro exhaustivo "Teoría de modelos finitos"
• Abiteboul , Hull, Vianu 1995: libro "Fundamentos de las bases de datos"
• Immerman 1999: libro " Complejidad descriptiva "
• Kuper, Libkin, Paredaens 2000: libro "Bases de datos de restricciones"
• Darmstadt 2005/ Aachen 2006: primeros talleres internacionales sobre "Teoría de modelos algorítmicos".

• Ebbinghaus, Heinz-Dieter ; Flum, Jörg (1995). Teoría de modelos finitos . Saltador . ISBN 978-3-540-60149-4.

• Fagin, Ronald (1976). "Probabilidades en modelos finitos". The Journal of Symbolic Logic . 41 (1): 50– 58. doi : 10.2307/2272945 . JSTOR 2272945 . 
• Glebskiĭ, Yu V.; Kogan, DI; Liogon'kiĭ, MI; Talanov, VA (1969). "Объем и доля выполнимости формул узкого исчисления предикатов" [ Volumen y fracción de satisfacibilidad de fórmulas del cálculo de predicados de primer orden ] . Kibernética . 5 (2): 17-27 .También disponible como: "Rango y grado de realizabilidad de fórmulas en el cálculo de predicados restringido". Cibernética . 5 (2): 142– 154. 1972. doi : 10.1007/BF01071084 .
• Libkin, Leonid (2004). Elementos de la teoría de modelos finitos . Springer . ISBN 3-540-21202-7.

• Abiteboul, Serge ; Hull, Richard; Vianu, Victor (1995). Fundamentos de las bases de datos . Addison-Wesley . ISBN 0-201-53771-0.

• Immerman, Neil (1999). Complejidad descriptiva . Nueva York: Springer . ISBN 0-387-98600-6.

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos en Ciencias de la Computación Teórica. Una serie de EATCS. ​​Berlín: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 . 

• Libkin, Leonid (2009). "El conjunto de herramientas de la teoría de modelos finitos de un teórico de bases de datos". PODS 2009: Actas del vigésimo octavo simposio ACM SIGACT–SIGMOD sobre Principios de los sistemas de bases de datos . pp. 65–76 . doi : 10.1145/1559795.1559807 .  También resulta adecuado como introducción general y panorama general.
• Leonid Libkin. Capítulo introductorio de "Elementos de la teoría de modelos finitos". Archivado el 24 de septiembre de 2015 en Wayback Machine . Motiva tres áreas de aplicación principales: bases de datos, complejidad y lenguajes formales.
• Jouko Väänänen. Un curso breve sobre teoría de modelos finitos . Departamento de Matemáticas, Universidad de Helsinki. Basado en conferencias de 1993 a 1994.
• Anuj Dawar. Teoría de modelos infinitos y finitos , diapositivas, Universidad de Cambridge, 2002.
• "Teoría de modelos algorítmicos" . RWTH Aachen. Archivado del original el 17 de julio de 2012. Consultado el 7 de noviembre de 2013 .Incluye una lista de problemas FMT abiertos.