Pregunta de seguimiento sobre fórmulas de primer orden en idiomas de primer orden y fórmulas abiertas.

Question

Esta es una pregunta de seguimiento a mi pregunta aquí. Voy a reproducir el contenido de mi pregunta original de la siguiente manera.

Para cualquiera de primer orden de la fórmula $X$ en el primer orden de lenguaje $\langle 0, S, \le\rangle$ (posiblemente con variables libres) no necesariamente existe otro abierto fórmula $Y$ de manera tal que la equivalencia $X \equiv Y$ que es verdad en el conjunto de todos no negativos números enteros?

Noé Schweber da la siguiente respuesta aquí, que voy a reproducir la siguiente manera.

Sí, esto es cierto. La estructura de $(\mathbb{N}; 0, S, \le)$ admite eliminación de cuantificadores, y la prueba de esto es a través de la inducción de la complejidad de $X$. Para un ejemplo de una prueba, a ver esta, que pasa a través de la prueba de eliminación de cuantificadores para una versión de la aritmética de Presburger.

Mi nueva pregunta es, hace una declaración similar para mantener el idioma $\langle 0, \le\rangle$?

Answer 1

No, no. El conjunto $\{1\}$ es definible en que la estructura es el conjunto de $x$ tal que $$x\not=0\wedge \forall y(y\le x\implies [y=0 \vee y=x]).$$ sin Embargo, no es difícil mostrar que es no definible por un cuantificador fórmula libre (no hay muchos sets que son definibles por un cuantificador fórmula libre en esta estructura; vea si usted puede encontrar todos ellos, y demostrar que su lista es exhaustiva!). A grandes rasgos, la razón es que este idioma no tiene suficiente términos.

Por cierto, tenga en cuenta que la función sucesor es definible en este idioma ($S(x)=y$ fib $x\le y$$\neg y\le x$$\forall z[x\le z\wedge z\le y\implies x=z\vee z=y]$); la combinación de esta con la observación de la pregunta anterior que $(\mathbb{N}; 0, \le, S)$ no han eliminación de cuantificadores, se obtienen dos hechos interesantes:

• Definibles expansiones de teorías sin eliminación de cuantificadores pueden "ganar" eliminación de cuantificadores. (Por el contrario, no es difícil demostrar que una vez que han eliminación de cuantificadores, usted no pierde al pasar a definible de expansión.)

• Dado que la función sucesor es definible por una fórmula con un cuantificador, cada definibles relación en $(\mathbb{N}; 0, \le)$ es definible por una combinación Booleana existencial de fórmulas; así que, mientras no tengamos eliminación de cuantificadores, el cuantificador de la jerarquía de hace colapso - pero no de inmediato.