Eliminación del cuantificador, $(\mathbb{R}, <)$

Question

Tengo una pregunta general sobre la eliminación de cuantificadores. ¿Qué tipos de fórmulas hay que observar?

Por ejemplo, dejemos que T sea la teoría de $(\mathbb{R}, <)$ y quiero mostrar, que esta teoría tiene eliminación de cuantificadores.

¿Qué tengo que hacer en general para probarlo? ¿Sólo hay fórmulas específicas que tengo que observar? ¿La eliminación del cuantificador tiene siempre los mismos pasos, de modo que siempre se observan las mismas fórmulas y se demuestra que son equivalentes a una fórmula sin cuantificador?

Gracias de antemano.

Edición: Ortografía mejorada.

Answer 1

Para demostrar la eliminación del cuantificador, basta con tratar las fórmulas que consisten en un único cuantificador existencial aplicado a una conjunción de fórmulas atómicas y atómicas negadas. Pero esa es, hasta donde yo sé, la única reducción general disponible. Después de eso, hay que considerar la teoría particular y hacer algo de trabajo real.

Answer 2

Hay "dos" métodos de prueba que conozco. Uno es el método clásico en el que se trata de eliminar activamente los cuantificadores de una fórmula. El otro es teórico de modelos y (para mí) más fácil de trabajar. Pero el profesor Blass tiene razón. Está casi garantizado que tendrás que ensuciarte las manos y trabajar explícitamente con la teoría.

Método sintáctico: En primer lugar, dejemos que $\{\alpha_i\}_{i=1}^n$ sea una colección de literales (una fórmula atómica, o la negación de una fórmula atómica). Entonces, $T$ tiene Q.E. en este lenguaje si para cada colección finita de $\alpha_i$ 's, tenemos $(\exists x)(\alpha_1 \wedge...\wedge \alpha_n)$ equivale a $\Delta$ donde $\Delta$ está libre de cuantificadores.

Prueba del método: Fuente - Diapositivas 4-5

Método semántico: Dejemos que $N,M$ sean dos cualesquiera $\omega-saturated$ modelos de $T$ . Sea $tp_{qf}(a_1,...,a_n)$ sea el tipo libre de cuantificador de $(a_1,...,a_n)$ sobre el conjunto vacío. Entonces $T$ tiene Q.E. si siempre:

Si $a_1,...,a_n\in N$ , $b_1,...,b_n \in M$ y $tp_{qf}(a_1,...,a_n) = tp_{qf}(b_1,...,b_n)$ entonces para cualquier $d \in N$ $\exists e \in M$ tal que $tp_{qf}(a_1,...,a_n,d) = tp_{qf}(b_1,...,b_n,e)$ .

Esencialmente, esto dice que siempre se pueden extender tipos finitos (libres de cuantificadores). Personalmente encuentro este método más fácil, pero al mismo tiempo, este método no es efectivo, es decir, no te da necesariamente un algoritmo para eliminar cuantificadores de una fórmula.

Prueba del método: Fuente - Páginas 22-23