lógica monádica de segundo orden

En lógica matemática , la lógica monádica de segundo orden ( MSO ) es el fragmento de lógica de segundo orden donde la cuantificación de segundo orden se limita a la cuantificación sobre conjuntos. ^{[ 1 ]} Es particularmente importante en la lógica de grafos , debido al teorema de Courcelle , que proporciona algoritmos para evaluar fórmulas monádicas de segundo orden sobre grafos de ancho de árbol acotado . También es de importancia fundamental en la teoría de autómatas , donde el teorema de Büchi-Elgot-Trakhtenbrot da una caracterización lógica de los lenguajes regulares .

La lógica de segundo orden permite la cuantificación sobre predicados . Sin embargo, MSO es el fragmento en el que la cuantificación de segundo orden se limita a predicados monádicos (predicados con un solo argumento). Esto se suele describir como cuantificación sobre "conjuntos" porque los predicados monádicos tienen un poder expresivo equivalente al de los conjuntos (el conjunto de elementos para los que el predicado es verdadero).

La lógica monádica de segundo orden es expresivamente equivalente a la lógica plural .

La lógica monádica de segundo orden se presenta en dos variantes. En la variante considerada sobre estructuras como grafos y en el teorema de Courcelle, la fórmula puede incluir constantes de predicado no monádicas (en este caso, el predicado de arista binaria ), pero la cuantificación se restringe a variables de predicado monádicas únicamente. En la variante considerada en la teoría de autómatas y el teorema de Büchi-Elgot-Trakhtenbrot, todos los predicados, constantes o variables, deben ser monádicos, con las excepciones de las relaciones de igualdad ( ) y orden ( ).${\displaystyle E(x,y)}$${\displaystyle =}$${\displaystyle <}$

La lógica monádica existencial de segundo orden (EMSO) es el fragmento de MSO en el que todos los cuantificadores sobre conjuntos deben ser cuantificadores existenciales , fuera de cualquier otra parte de la fórmula. Los cuantificadores de primer orden no están restringidos. Es decir, se puede hablar de "existe algún x tal que..." y "para todo x se tiene..." donde x es un término, pero solo se puede hablar de "existe algún predicado monádico P tal que...", no de "para todo predicado monádico P se tiene...".

El teorema de Fagin afirma que la lógica existencial de segundo orden (LSO) captura con precisión la complejidad descriptiva de la clase de complejidad NP . Por analogía, la clase de problemas que pueden expresarse en lógica monádica existencial de segundo orden se ha denominado NP monádica . En otras palabras, la LSO captura con precisión la complejidad descriptiva de la NP monádica (NPM).

En la lógica de grafos , probar si un grafo es desconectado pertenece a MNP, ya que la prueba puede representarse mediante una fórmula que describe la existencia de un subconjunto propio de vértices sin aristas que los conecten con el resto del grafo. El problema complementario, probar si un grafo es conexo, no pertenece a NP monádico. Es decir, es un problema en co -MNP \ MNP. Por simetría, la prueba de desconexión de grafos está en MNP \ co-MNP, lo que demuestra que ninguna clase de complejidad contiene a la otra. ^{[ 2 ] [ 3 ]} La adición de "monádico" hace la pregunta más fácil. La pregunta análoga, de si NP = co-NP , es una pregunta abierta en complejidad computacional.

Por el contrario, cuando deseamos comprobar si una fórmula MSO booleana es satisfecha por un árbol finito de entrada , este problema puede resolverse en tiempo lineal en el árbol, traduciendo la fórmula MSO booleana a un autómata de árbol ^{[ 4 ]} y evaluando el autómata en el árbol. Sin embargo, en términos de la consulta, la complejidad de este proceso generalmente no es elemental . ^{[ 5 ] [ 6 ]} Gracias al teorema de Courcelle , también podemos evaluar una fórmula MSO booleana en tiempo lineal en un grafo de entrada si el ancho del árbol del grafo está acotado por una constante.

Para fórmulas MSO con variables libres , cuando los datos de entrada son un árbol o tienen un ancho de árbol limitado, existen algoritmos de enumeración eficientes para generar el conjunto de todas las soluciones, ^{[ 7 ]} asegurando que los datos de entrada se preprocesen en tiempo lineal y que cada solución se genere con un retardo lineal en el tamaño de cada solución, es decir, retardo constante en el caso común donde todas las variables libres de la consulta son variables de primer orden (es decir, no representan conjuntos). También existen algoritmos eficientes para contar el número de soluciones de la fórmula MSO en ese caso. ^{[ 8 ]}

El problema de satisfacibilidad para la lógica monádica de segundo orden es indecidible en general porque esta lógica engloba a la lógica de primer orden .

La teoría monádica de segundo orden del árbol binario completo infinito , denominada S2S , es decidible . ^{[ 9 ]} Como consecuencia de este resultado, las siguientes teorías son decidibles:

• La teoría monádica de segundo orden de los árboles.
• S1S, La teoría monádica de segundo orden con un sucesor (es decir, de )${\displaystyle \mathbb {N} }$
• WS2S y WS1S, que restringen la cuantificación a subconjuntos finitos (lógica monádica débil de segundo orden).
  • Al codificar binariamente los números naturales como subconjuntos finitos, la suma se puede definir incluso en WS1S.

Para cada una de estas teorías (S2S, S1S, WS2S, WS1S), la complejidad del problema de decisión no es elemental . ^{[ 5 ] [ 6 ]} Podrían obtenerse realizando una reducción del problema de vacuidad de los lenguajes libres de estrellas a WS1S. ^{[ 10 ]} Se sabe específicamente que WS1S es TOWER -completo. ^{[ 11 ]}

• Teoría de la complejidad descriptiva
• cálculo de predicados monádicos
• Lógica de segundo orden