¿Por qué es deseable la eliminación de cuantificadores en una teoría determinada?

Question

Decimos que una teoría dada $T$ admite la QE en un idioma $\mathcal{L}$ si para cada $\mathcal{L}$ -existe un cuantificador libre equivalente $\mathcal{L}$ -fórmula. Es decir, para cada $\mathcal{L}$ -fórmula $\phi(x)$ , donde $x$ es una variable libre, existe un $\mathcal{L}$ -fórmula $\psi(x)$ para que $T\vDash\forall x\left(\phi(x)\iff\psi(x)\right)$ .

La forma en que interpreto esto es que para cualquier fórmula que $T$ implica que existe una fórmula equivalente libre de q que $T$ imples. En otras palabras, todas las consecuencias lógicas de $T$ son expresables q-libre.

Mi pregunta es entonces:

¿Por qué es ventajoso? ¿Cuál es la ventaja de que todas las consecuencias lógicas de una teoría sean expresables sin q?

La Wikipedia dice algo así como que admitir la QE simplifica el problema de decidibilidad. Pero, ¿no admiten todas las teorías la QE en un lenguaje suficientemente complejo? ¿Por qué es deseable ser decidible con respecto a un lenguaje pequeño (más simple)?

Answer 1

Tienes mucha razón en que podemos "meter con calzador" la eliminación de cuantificadores en cualquier teoría que queramos, añadiendo nuevos predicados para todas las fórmulas antiguas (esto se llama Morleyización si no recuerdo mal). Así que considerado en el vacío, no hay nada particularmente especial en la eliminación de cuantificadores.

La eliminación del cuantificador es útil en el contexto de las teorías cuyos fragmentos libres de cuantificadores ya tienen propiedades agradables - es decir, forma medio de un argumento, siendo la otra mitad el análisis del fragmento sin cuantificador de la teoría en cuestión para empezar. Para un buen ejemplo de esto, mire la prueba teórica del modelo de la Nullstellensatz La eliminación del cuantificador por sí sola no hace nada, pero en combinación con lo que ya sabemos (por ejemplo, por el teorema fundamental del álgebra) sobre las fórmulas sin cuantificador en campos algebraicamente cerrados nos da algo no trivial.

Answer 2

Voy a escribir esta respuesta desde una perspectiva de teoría de modelos y me centraré un poco más en por qué forzar la eliminación de cuantificadores mediante la Morleyización puede no ayudar a nuestra comprensión de la teoría en cuestión.

Dada una teoría particular $T$ uno de los pasos clave para entender $T$ es entender los subconjuntos definibles de $T$ . La eliminación del cuantificador en este contexto es extremadamente útil. En lugar de buscar fórmulas extremadamente complicadas, simplemente se ven fórmulas libres de cuantificadores.

Por ejemplo, la teoría del grafo aleatorio (en el lenguaje $L=\{E\}$ ) tiene la eliminación del cuantificador. Así que en lugar de intentar entender una fórmula extremadamente complicada $\varphi(\overline{x})$ Si el resultado es una fórmula con una alternancia de mil millones de cuantificadores, podemos sustituirla por una fórmula libre de cuantificadores, que en este caso simplemente acaba describiendo un grafo finito. Así que comprobar si $\varphi(\overline{x})$ se satisface con la tupla $\overline{a}$ de un modelo $M$ del gráfico aleatorio se reduce simplemente a comprobar si $\overline{a}$ tiene la estructura gráfica adecuada, ignorando esencialmente los mil millones de cuantificadores.

Este ejemplo también nos lleva a tu pregunta sobre forzar la eliminación del cuantificador a través de la Morleyización. Se puede hacer. Pero las fórmulas libres de cuantificadores obtenidas de esta manera pueden no tener una representación agradable que ayude a nuestra comprensión de la teoría. Por ejemplo, si llevamos a cabo la Morleyzación para la teoría aquí obtenemos que hay algún nuevo símbolo de relación $R_{\varphi}((\overline{x}))$ tal que para cualquier tupla $\overline{a}$ de un modelo $M$ del gráfico aleatorio $M\models\varphi(\overline{a})$ si y sólo si $M\models R_{\varphi}\overline{a}$ . Esto no aumenta realmente nuestra comprensión de cómo $\varphi$ se comporta o cómo evaluarlo.