Lógica de dos variables

En lógica matemática y ciencias de la computación , la lógica de dos variables es el fragmento de la lógica de primer orden donde las fórmulas se pueden escribir utilizando solo dos variables diferentes . ^[1] Este fragmento generalmente se estudia sin símbolos de función .

Decidibilidad

Algunos problemas importantes sobre la lógica de dos variables, como la satisfacibilidad y la satisfacibilidad finita , son decidibles . ^[2] Este resultado generaliza los resultados sobre la decidibilidad de fragmentos de la lógica de dos variables, como ciertas lógicas de descripción ; sin embargo, algunos fragmentos de la lógica de dos variables disfrutan de una complejidad computacional mucho menor para sus problemas de satisfacibilidad.

Por el contrario, para el fragmento de tres variables de la lógica de primer orden sin símbolos de función, la satisfacibilidad es indecidible. ^[3]

Cuantificadores de conteo

Se sabe que el fragmento de dos variables de la lógica de primer orden sin símbolos de función es decidible incluso con la adición de cuantificadores de conteo ^[4] y, por lo tanto, de cuantificación de unicidad . Este es un resultado más potente, ya que los cuantificadores de conteo para valores numéricos altos no son expresables en esa lógica.

Los cuantificadores de conteo en realidad mejoran la expresividad de las lógicas de variables finitas, ya que permiten decir que hay un nodo con vecinos, es decir . Sin cuantificadores de conteo, se necesitan variables para la misma fórmula. ${\displaystyle n}$ ${\displaystyle \Phi =\exists x\exists ^{\geq n}yE(x,y)}$ ${\displaystyle n+1}$

Conexión con el algoritmo Weisfeiler-Leman

Existe una fuerte conexión entre la lógica de dos variables y el algoritmo Weisfeiler-Leman (o de refinamiento de color ). Dados dos gráficos, entonces dos nodos cualesquiera tienen el mismo color estable en el refinamiento de color si y solo si tienen el mismo tipo, es decir, satisfacen las mismas fórmulas en la lógica de dos variables con conteo. ^[5] ${\displaystyle C^{2}}$

Referencias

1. L. Henkin. Sistemas lógicos que contienen sólo un número finito de símbolos , Informe, Departamento de Matemáticas, Universidad de Montreal, 1967
2. E. Grädel, PG Kolaitis y M. Vardi, Sobre el problema de decisión para la lógica de primer orden de dos variables , The Bulletin of Symbolic Logic, vol. 3, n.º 1 (marzo de 1997), págs. 53-69.
3. AS Kahr, Edward F. Moore y Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case , 1962, señalando que sus fórmulas ∀ ∃ ∀ utilizan solo tres variables.
4. E. Grädel, M. Otto y E. Rosen. La lógica de dos variables con conteo es decidible. , Actas del duodécimo simposio anual IEEE sobre lógica en informática, 1997.
5. Grohe, Martin. "Lógicas de variables finitas en la teoría de la complejidad descriptiva". Boletín de lógica simbólica 4.4 (1998): 345-398.