Eliminación de cuantificadores

Eliminación de cuantificadores - obtención, de acuerdo con una fórmula lógica dada , equivalente a ella, que no contiene cuantificadores . Las teorías que permiten la eliminación de cuantificadores para cualquier fórmula son de particular interés, ya que la presencia de un algoritmo de eliminación permite obtener una serie de resultados significativos sobre esta teoría.

Los procesos de búsqueda de algoritmos de eliminación de cuantificadores para varias teorías tienen características comunes, lo que nos permite hablar de ellos como un solo método. Tarski introdujo el nombre método de eliminación del cuantificador en 1935 , aunque Langford utilizó por primera vez consideraciones de este tipo en 1927 . El método de eliminación de cuantificadores es aplicable sólo a teorías de un tipo muy especial, y además, cada vez que se aplica este método a una nueva teoría, hay que realizar todas las demostraciones desde el principio, ya que el arsenal de resultados generales es muy pobre. Sin embargo, si se puede aplicar, este método resulta extremadamente útil, ya que proporciona información completa sobre una teoría dada. Por lo general, también conduce a una forma regular de decidir si un enunciado pertenece o no a una teoría dada; en otras palabras, proporciona una prueba de la decidibilidad de la teoría .

Teorías de primer orden

Una teoría de primer orden admite la eliminación de cuantificadores si para alguna fórmula (no necesariamente cerrada ) de esa teoría existe una fórmula que no contiene cuantificadores tal que , es decir, ambas fórmulas son equivalentes en todos los modelos de la teoría . $\mathcal{T}$ $\varphi$ $\psi$ $\mathcal{T}\modelos\varphi\leftrightarrow\psi$ $\mathcal{T}$

Las teorías de primer orden más importantes que permiten la eliminación de cuantificadores son la aritmética de Presburger , campos algebraicamente cerrados , campos reales cerrados ( teorema de Seidenberg-Tarski ), álgebras booleanas sin átomos , álgebra de términos , orden lineal denso , teoría de grupos abelianos , teoría de colas . En este caso, por ejemplo, en aritmética de enteros , la fórmula es equivalente a la fórmula , pero para la fórmula no hay fórmula equivalente que no contenga cuantificadores, es decir, la aritmética de enteros no permite la eliminación de cuantificadores. $\existe x(x\geqslant 0\land a+x=b)$ $b\geqslant a$ $\existir x (a = x\cdot b)$

Aproximación a la prueba

Para probar que la eliminación de cuantificadores es factible en esta teoría, basta demostrar que es posible eliminar el cuantificador existencial aplicado a la conjunción de literales , es decir, una fórmula de la forma:

{\displaystyle \existe x\bigwedge _{i=1}^{n}L_{i))

El cuantificador universal puede ser reemplazado por el cuantificador existencial, ya que es equivalente a . Además, la fórmula se puede escribir en forma normal disyuntiva y aprovechar el hecho de que: $\para todo xF$ $\lnot \existe x\lnot F$

\existe x\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}

equivalente a

\bigvee _{j=1}^{m}\existe x\bigwedge _{i=1}^{n}L_{ij}

Literatura

Keisler G., Chen Ch . Teoría de modelos. — M .: Mir, 1977.
N. K. Vereshchagin, A. Shen . 2. Lenguajes y Cálculo // Clases de Lógica Matemática y Teoría de Algoritmos. — M. : MTsNMO, 2012.