eliminación de cuantificadores

La eliminación de cuantificadores es un concepto de simplificación utilizado en lógica matemática , teoría de modelos y ciencias de la computación teóricas . De manera informal, una declaración cuantificada "${\displaystyle \exists x}$de tal manera que  ..." puede verse como una pregunta "¿Cuándo hay una${\displaystyle x}$de tal manera que  ...?", y la afirmación sin cuantificadores puede considerarse la respuesta a esa pregunta. ^{[ 1 ]}

Una forma de clasificar las fórmulas es por la cantidad de cuantificación . Se piensa que las fórmulas con menor profundidad de alternancia de cuantificadores son más simples, siendo las fórmulas sin cuantificadores las más simples. Una teoría tiene eliminación de cuantificadores si para cada fórmula${\displaystyle \alpha }$, existe otra fórmula${\displaystyle \alpha _{QF}}$sin cuantificadores que sea equivalente a ello ( módulo esta teoría).

Un ejemplo de matemáticas dice que un polinomio cuadrático de una sola variable tiene una raíz real si y solo si su discriminante es no negativo: ^{[ 1 ]}

$${\displaystyle \exists x\in \mathbb {R} .(a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0}$$

Aquí, la oración del lado izquierdo incluye un cuantificador.${\displaystyle \exists x\in \mathbb {R} }$, mientras que la oración equivalente de la derecha no lo hace.

Ejemplos de teorías que se han demostrado decidibles mediante la eliminación de cuantificadores son la aritmética de Presburger , ^{[ 2 ] [ 3 ] [ 4 ] [ 5 ] [ 6 ] [ 7 ]} la aritmética de Skolem , ^{[ 8 ]} los campos algebraicamente cerrados , los campos reales cerrados , ^{[ 9 ] [ 10 ]} las álgebras booleanas sin átomos , las álgebras de términos , los órdenes lineales densos , ^{[ 9 ]} los grupos abelianos , ^{[ 11 ]} los grafos de Rado , así como muchas de sus combinaciones, como el álgebra booleana con la aritmética de Presburger y las álgebras de términos con colas .

La eliminación de cuantificadores para la teoría de los números reales como un grupo aditivo ordenado es la eliminación de Fourier-Motzkin ; para la teoría del cuerpo de los números reales es el teorema de Tarski-Seidenberg . ^{[ 9 ]}

La eliminación de cuantificadores también puede utilizarse para demostrar que la "combinación" de teorías decidibles conduce a nuevas teorías decidibles (véase el teorema de Feferman-Vaught ).

Si una teoría tiene eliminación de cuantificadores, entonces se puede abordar una pregunta específica: ¿Existe un método para determinar?${\displaystyle \alpha _{QF}}$para cada${\displaystyle \alpha }$Si existe tal método, lo llamamos algoritmo de eliminación de cuantificadores . Si existe tal algoritmo, entonces la decidibilidad de la teoría se reduce a decidir la veracidad de las oraciones sin cuantificadores .

Diversas ideas de la teoría de modelos están relacionadas con la eliminación de cuantificadores, y existen diversas condiciones equivalentes.

Toda teoría de primer orden con eliminación de cuantificadores es modelo-completa . Recíprocamente, una teoría modelo-completa, cuya teoría de consecuencias universales tiene la propiedad de amalgamación , tiene eliminación de cuantificadores. ^{[ 12 ]}

Los modelos de la teoría de las consecuencias universales de una teoría${\displaystyle T}$son precisamente las subestructuras de los modelos de${\displaystyle T}$. ^{[ 12 ]} La teoría de los órdenes lineales no tiene eliminación de cuantificadores. Sin embargo, la teoría de sus consecuencias universales tiene la propiedad de amalgama.

Para demostrar de manera constructiva que una teoría tiene eliminación de cuantificadores, basta con demostrar que podemos eliminar un cuantificador existencial aplicado a una conjunción de literales , es decir, demostrar que cada fórmula de la forma:

$${\displaystyle \exists x.\bigwedge _{i=1}^{n}L_{i}}$$

donde cada${\displaystyle L_{i}}$es un literal, es equivalente a una fórmula sin cuantificadores. De hecho, supongamos que sabemos cómo eliminar los cuantificadores de las conjunciones de literales, entonces si${\displaystyle F}$es una fórmula sin cuantificadores, podemos escribirla en forma normal disyuntiva.

$${\displaystyle \bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij},}$$

y utilice el hecho de que

$${\displaystyle \exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}}$$

es equivalente a

$${\displaystyle \bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}.}$$

Finalmente, para eliminar un cuantificador universal

$${\displaystyle \forall xF}$$

dónde${\displaystyle F}$no tiene cuantificador, transformamos ${\displaystyle \lnot F}$en forma normal disyuntiva y utilizar el hecho de que${\displaystyle \forall xF}$ es equivalente a${\displaystyle \lnot \exists x.\lnot F.}$

En los inicios de la teoría de modelos, la eliminación de cuantificadores se utilizaba para demostrar que diversas teorías poseen propiedades como la decidibilidad y la completitud . Una técnica común consistía en demostrar primero que una teoría admite la eliminación de cuantificadores y, posteriormente, probar la decidibilidad o la completitud considerando únicamente las fórmulas sin cuantificadores. Esta técnica puede utilizarse para demostrar que la aritmética de Presburger es decidible.

Las teorías pueden ser decidibles pero no admitir la eliminación de cuantificadores. Estrictamente hablando, la teoría de los números naturales aditivos no admitía la eliminación de cuantificadores, pero se demostró que una extensión de los números naturales aditivos era decidible. Siempre que una teoría sea decidible y el lenguaje de sus fórmulas válidas sea numerable , es posible extenderla con una cantidad numerable de relaciones para que admita la eliminación de cuantificadores (por ejemplo, se puede introducir, para cada fórmula de la teoría, un símbolo de relación que relacione las variables libres de la fórmula).

Ejemplo: Teorema de los ceros para cuerpos algebraicamente cerrados y para cuerpos diferencialmente cerrados .

• Descomposición algebraica cilíndrica
• Teoría de la eliminación
• eliminación de conjunciones