Sé que en algunos casos simples de eliminación de cuantificadores que he visto, uno termina viendo que el proceso de eliminación de cuantificadores dio como resultado la capacidad de mostrar la decidibilidad. ¿Es esto cierto en general? Leí que los campos algebraicamente cerrados son decidibles y en un lugar separado admiten la eliminación de cuantificadores, pero no sé si la decidibilidad de ACF se debe a QE Gracias
Respuesta
¿Demasiados anuncios?
Demostrando que una de primer orden de la teoría de la $T$ admite cuantificador de eliminación es a menudo un gran paso hacia demostrando decidability, pero no es toda la historia. Una vez que hayas probado cuantificador de eliminación, usted sabe, en particular, que cada frase $S$ en el idioma de $T$ es equivalente a un cuantificador libre de pena de $S'$. Que sugiere la siguiente decisión pseudo-algoritmo para $T$: Dada como entrada una frase $S$ (por lo que se supone que decidir si $S$ es comprobable en $T$), encontrar el equivalente cuantificador libre de $S'$ y comprobar si eso es comprobable en $T$; debido a la equivalencia, $S$ será comprobable en $T$ si y sólo si $S'$ es. Hay dos razones por las que este pseudo-algoritmo puede no ser un auténtico algoritmo, es decir, las palabras "encontrar" y "verificación". Deja que me ocupe de ellos.
Para hacer el pseudo-algoritmo en un algoritmo, usted necesita ser capaz de algorithimically calcular $S'$ al $S$ es dado. Esto no es problema si te dan una computable (o incluso sólo computably enumerable) axiomatization de $T$, porque entonces usted puede simplemente una búsqueda sistemática a través de todas las pruebas de $T$ hasta que encuentre uno cuya conclusión que tiene la forma de $S\iff S'$ $S'$ cuantificador. (A menudo, no hay necesidad de buscar a través de las pruebas, debido a que el argumento que muestra cuantificador de la eliminación ya puede contener un algoritmo de conversión de $S$$S'$.) Pero para totalmente salvaje $T$, sin una decente axiomatization, es posible que todos los $S$ tiene un equivalente $S'$, pero no hay algoritmo para encontrar una adecuada $S'$ al $S$ es dado. Resumen: Usted necesita efectivo cuantificador de la eliminación, lo que significa que el cuantificador fórmula libre de cuya existencia está garantizada por el cuantificador de la eliminación puede ser a través de algoritmos encontrados.
Segundo, una vez que el deseado cuantificador libre de pena de $S'$, usted necesita a través de algoritmos de verificación si es comprobable en $T$. De nuevo, esto no es problema en niza de los casos, debido a que generalmente hay muy pocas posibilidades de $S'$. Tenga en cuenta que $S'$ no puede contener ninguna de las variables --- no tiene variables libres porque es una frase, y no tiene variables vinculadas porque es cuantificador. En muchos de primer orden de los idiomas, esta drásticamente los límites de lo $S'$ puede ser. Por ejemplo, en el lenguaje de los campos (constantes 0 y 1, binarias, operaciones de campo, y la igualdad), $S'$ tiene que ser un proposicional combinación de las ecuaciones entre expresiones racionales construido a partir de 0 y 1. En tales casos, la decisión provability de $S'$ es generalmente trivial, pero para totalmente salvaje $T$, no puede haber ninguna algoritmo para esta tarea. Resumen: Se necesita un algoritmo de decisión para la provability en $T$ de cuantificador libre de penas.
Si usted tiene cuantificador de la eliminación de más el extra de información en los resúmenes al final de los párrafos anteriores, a continuación, el pseudo-algoritmo se convierte en un auténtico algoritmo de decisión.
Sin ese tipo de información extra, cuantificador de eliminación no podría hacer ningún bien en absoluto. De hecho, dado que ninguna de primer orden de la teoría de la $T$, puede incrustar en un cuantificador-eliminable teoría de la $T^+$ mediante la adición de que el lenguaje de los nuevos símbolos de predicado, una $n$-ary predicado $P_\phi$ para cada fórmula $\phi(x_1,\dots,x_n)$, con axiomas $P_\phi(x_1,\dots,x_n)\iff\phi(x_1,\dots,x_n)$. Que hace que $T^+$ trivialmente cuantificador-eliminable, pero no más decidable que el original $T$. (La construcción de la $T^+$ es a veces llamado "Morleyizing" $T$. Además de las objeciones que tienen algunas personas para "ize" verbos, este nombre para una trivialidad podría ser considerado un insulto a Michael Morley.)
