Eliminación de cuantificadores

Question

¿Qué significa que una teoría admite constructivo eliminación de cuantificadores?

Una teoría admite la eliminación de cuantificadores cuando cada fórmula de la teoría es equivalente a un quanifier fórmula libre, ¿verdad?

Pero lo que se quiere decir cuando usamos el término "constructiva" ?

Answer 1

Me gustaría interpretar esto significa que hay una computable procedimiento encontrar por cualquier fórmula $\varphi$ un cuantificador fórmula libre de $\varphi^*$ que es equivalente a que el modulo de la teoría.

Si la teoría de la $T$ es c.e. axiomatizable, entonces esto es equivalente a la ordinaria cuantificador de la eliminación, ya que si la teoría de la $T$ admite la eliminación de cuantificadores, entonces, dado cualquier $\varphi$ que puede buscar a través de todas las pruebas de $T$ hasta que nos encontramos con un cuantificador libre de $\varphi^*$ $T$- seguramente equivalente, y luego la salida de la primera de dichas $\varphi^*$ que nos encontramos. Así que si la teoría de la $T$ es c.e., entonces QE es el mismo constructivo QE.

Este hecho es a menudo importante para probar la decidability de una teoría. Si un c.e. teoría admite QE y el cuantificador libre de penas decidable valores de verdad, entonces es decidable, porque para cualquier frase, podemos buscar un cuantificador libre equivalente de la misma, mediante la búsqueda de pruebas, y decidir la verdad de que (trivial) la formulación, así decidir la teoría.

Pero si la teoría de la $T$ no es c.e., a continuación, podría ser un requisito más fuerte que el QE es eficaz. Si quieres, yo voy a tratar de hacer un ejemplo de una teoría que tiene QE, pero no constructiva QE.