Espectro de una sentencia

En lógica matemática, el espectro de una oración es el conjunto de números naturales que ocurren como el tamaño de un modelo finito en el que una sentencia dada es verdadera.

Definición

Sea ψ una oración en la lógica de primer orden . El espectro de ψ es el conjunto de números naturales n tal que existe un modelo finito para ψ con n elementos.

Si el vocabulario para ψ consiste solo en símbolos relacionales, entonces ψ puede considerarse como una oración en la lógica existencial de segundo orden (ESOL) cuantificada sobre las relaciones, sobre el vocabulario vacío. Un espectro generalizado es el conjunto de modelos de una oración general de ESOL.

Ejemplos

• El espectro de la fórmula de primer orden.

$\exists z,o~\forall a,b,c~\exists d,e$

$a+z=a=z+a~\land ~a\cdot z=z=z\cdot a~\land ~a+d=z$

$\land ~a+b=b+a~\land ~a\cdot (b+c)=a\cdot b+a\cdot c~\land ~(a+b)+c=a+(b+c)$

$\land ~a\cdot o=a=o\cdot a~\land ~a\cdot e=o~\land ~(a\cdot b)\cdot c=a\cdot (b\cdot c)$

es $\{p^{n}\mid p{\text{ prime}},n\in \mathbb {N} \}$, el conjunto de potencias de un número primo. De hecho, con $z$ para $0$ y $o$ para $1$, esta sentencia describe el conjunto de campos; La cardinalidad de un campo finito es la potencia de un número primo.

• El espectro de la fórmula lógica monádica de segundo orden $\exists S,T~\forall x~\left\{x\in S\iff x\not \in T\land ~f(f(x))=x\land ~x\in S\iff f(x)\in T\right\}$ es el conjunto de números pares. En efecto, $f$ es una biyección entre $S$ y $T$ y $S$ y $T$ Son una partición del universo. Por lo tanto, la cardinalidad del universo es par.
• El conjunto de conjuntos finitos y co-finitos es el conjunto de espectros de lógica de primer orden con la relación sucesora.
• El conjunto de conjuntos periódicos en última instancia es el conjunto de espectros de lógica monádica de segundo orden con una función unaria. También es el conjunto de espectros de lógica monádica de segundo orden con la función sucesora.

Propiedades

El Teorema de Fagin es un resultado en una teoría de la complejidad descriptiva que establece que el conjunto de todas las propiedades expresables en la lógica existencial de segundo orden es precisamente la clase de complejidad NP. Esto es notable porque que es una caracterización de la clase NP que no invoca un modelo de cálculo como una máquina de Turing. El teorema fue probado por Ronald Fagin en 1973 en su tesis doctoral.

Equivalencia a las máquinas de Turing

Como corolario, Jones y Selman mostraron que un conjunto es un espectro si y solo si está en la clase de complejidad NEXP.​

Una dirección de la prueba es mostrar que, para cada fórmula de primer orden $\varphi$, el problema de determinar si existe un modelo de la fórmula de cardinalidad n es equivalente al problema de satisfacer una fórmula de polinomio de tamaño en n, que está en NP (n) y, por lo tanto, en NEXP de la entrada al problema (el número n en forma binaria, que es una cadena de tamaño log ( n )).

Esto se hace reemplazando cada cuantificador existencial en $\varphi$ con disyunción sobre todos los elementos en el modelo y reemplazando cada cuantificador universal con conjunción sobre todos los elementos en el modelo. Ahora cada predicado está en los elementos del modelo, y finalmente cada aparición de un predicado en elementos específicos se reemplaza por una nueva variable proposicional. La igualdad se reemplaza por sus valores de verdad de acuerdo con sus asignaciones.

Por ejemplo:

$\forall {x}\forall {y}\left(P(x)\wedge P(y)\right)\rightarrow (x=y)$

Para un modelo de cardinalidad 2 (es decir, n = 2) se reemplaza por

${\big (}\left(P(a_{1})\wedge P(a_{1})\right)\rightarrow (a_{1}=a_{1}){\big )}\wedge {\big (}\left(P(a_{1})\wedge P(a_{2})\right)\rightarrow (a_{1}=a_{2}){\big )}\wedge {\big (}\left(P(a_{2})\wedge P(a_{1})\right)\rightarrow (a_{2}=a_{1}){\big )}\wedge {\big (}\left(P(a_{2})\wedge P(a_{2})\right)\rightarrow (a_{2}=a_{2}){\big )}$

Que luego se reemplaza por ${\big (}\left(p_{1}\wedge p_{1}\right)\rightarrow \top {\big )}\wedge {\big (}\left(p_{1}\wedge p_{2}\right)\rightarrow \bot {\big )}\wedge {\big (}\left(p_{2}\wedge p_{1}\right)\rightarrow \bot {\big )}\wedge {\big (}\left(p_{2}\wedge p_{2}\right)\rightarrow \top {\big )}$

dónde $\top$ es verdad, $\bot$ es falsedad y $p_{1}$, $p_{2}$ son variables proposicionales En este caso particular, la última fórmula es equivalente a $\neg (p_{1}\wedge p_{2})$, que es satisfactoria.

La otra dirección de la prueba es mostrar que, para cada conjunto de cadenas binarias aceptadas por una máquina de Turing no determinista que se ejecuta en tiempo exponencial ( $2^{cx}$ para una entrada de longitud x), hay una fórmula de primer orden $\varphi$ tal que el conjunto de números representados por estas cadenas binarias son el espectro de $\varphi$ .

Jones y Selman mencionan que el espectro de fórmulas de primer orden sin igualdad es solo el conjunto de todos los números naturales no más pequeños que una mínima cardinalidad.

Otras propiedades

El conjunto de espectros de una teoría se cierra bajo unión, intersección, suma y multiplicación. En general, no se sabe si el conjunto de espectros de una teoría se cierra por complementación; Este es el llamado Problema de Asser.

Referencias

• Fagin, Ronald (1974). «Generalized First-Order Spectra and Polynomial-Time Recognizable Sets». En Karp, Richard M., ed. Complexity of Computation. Proc. Syp. App. Math. SIAM-AMS Proceedings 7. pp. 27-41. 
• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. doi:10.1007/3-540-68804-8.  Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. doi:10.1007/3-540-68804-8.  Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. doi:10.1007/3-540-68804-8. 
• Immerman, Neil (1999). Descriptive Complexity. Graduate Texts in Computer Science. New York: Springer-Verlag. pp. 113–119. ISBN 0-387-98600-6.  Immerman, Neil (1999). Descriptive Complexity. Graduate Texts in Computer Science. New York: Springer-Verlag. pp. 113–119. ISBN 0-387-98600-6.  Immerman, Neil (1999). Descriptive Complexity. Graduate Texts in Computer Science. New York: Springer-Verlag. pp. 113–119. ISBN 0-387-98600-6. 
• Durand, Arnaud; Jones, Neil; Markowsky, Johann; More, Malika (2012). «Fifty Years of the Spectrum Problem: Survey and New Results». Bulletin of Symbolic Logic 18 (4): 505-553. Bibcode:2009arXiv0907.5495D. arXiv:0907.5495. doi:10.2178/bsl.1804020. 

• Datos: Q97942961