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 teoría de la computación. Informalmente, una proposición cuantificada, por ejemplo "$\exists x$ tal que $\ldots$" puede verse como una pregunta: "¿Cuándo hay un $x$ tal que $\ldots$?",y la proposición sin cuantificadores puede verse como la respuesta a esa pregunta.​

Un criterio de clasificación de fórmulas es atendiendo a su cantidad de cuantificadores. Las fórmulas con menos cuantificadores anidados son más simples, siendo las fórmulas en las que no aparecen cuanficiadores las más sencillas. Una teoría lógica tiene eliminación de cuantificadores si para cada fórmula $\alpha$, existe otra fórmula $\alpha _{QF}$ sin cuantificadores que es equivalente a ella (módulo de ese teorema).

Ejemplos

"Un polinomio cuadrático de una sola variable tiene una raíz real si y solo si su discriminante no es negativo." Es decir:​

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

La proposición de la izquierda tiene un cuantificador: $\exists x\in \mathbb {R}$, mientras que la de la derecha no.

Otros ejemplos de teorías en las que se puede aplicar la eliminación de cuantificadores son Aritmética Presburger,​ Campos algebraicamente cerrados, campos reales cerrados,​​ atomless Boolean algebras, term algebras, orden lineal denso,​ grupos abelianos,​ grafos arbitrarios, así como muchas de sus combinaciones como el álgebra de Boole con la aritmética de Presburger, y term algebras con colas.

La eliminación de cuantificadores para la teoría de los números reales como un grupo ordenado aditivo es la eliminación de Fourier–Motzkin; para la teoría del campo de los números reales es el teorema de Tarski–Seidenberg.​

La eliminación de cuantificadores también se utiliza para mostrar que "combinando" teorías lógicas decidibles se da lugar a nuevas teorías lógicas decidibles.

Algoritmos y decidibilidad

Si una teoría tiene eliminación de cuantificadores, podemos formular la siguiente pregunta: ¿Hay algún método para determinar $\alpha _{QF}$ para cada $\alpha$? Si existe dicho método, se llamará algoritmo de eliminación de cuantificadores. Si existe dicho algoritmo, entonces la decidibilidad de esa teoría se reduce a evaluar la veracidad de las proposiciones sin cuantificadores. Dichas proposiciones no tienen variables, por lo que su validez en una teoría puede evaluarse, lo que permite el uso de algoritmos de eliminación de cuantificadores para saber si las proposiciones son decidibles.

Conceptos relacionados

Varias ideas de teorías de modelos están relacionadas con la eliminación de cuantificadores, y hay varias condiciones equivalentes.

Cualquier teoría lógica de primer orden con eliminación de cuantificadores es model complete. Por el contrario, una model-complete theory, cuya teoría de consecuencias universales cuenta con la amalgamation property, tiene eliminación de cuantificadores.​

Los modelos de la teoría de consecuencias universales de una teoría lógica $T$ son precisamente las subestructuras de los modelos de $T$.​ La teoría de órdenes lineales no tiene eliminación de cuantificadores. No obstante, la teoría de sus consecuencias universales tiene la propiedad de amalgamación.

Ideas básicas

Para demostrar de forma constructiva que una teoría tiene eliminación de cuantificadores, basta con mostrar que podemos eliminar un cuantificador existencial aplicado a una conjunción de literales. Es decir, mostrar que cualquier fórmula expresada de la siguiente forma:

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

donde cada $L_{i}$ es un literal, es equivalente a una fórmula sin cuantificadores. Suponiendo que sabemos cómo eliminar cuantificadores de una conjunción de literales, entonces si $F$ es una fórmula sin cuantificadores, podemos escribirla en forma normal disyuntiva:

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

y teniendo en cuenta que

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

es equivalente a

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

Finalmente, para eliminar un cuantificador universal

$\forall x.F$

donde $F$ no tiene cuantificadores, transformamos $\lnot F$ en forma normal disyuntiva, y aprovechamos que $\forall x.F$ es equivalente a $\lnot \exists x.\lnot F.$

Historia

En los principios de la teoría de modelos, la eliminación de cuantificadores se utilizaba para demostrar que varias teorías contaban con propiedades como la decidibilidad y completitud. Una técnica común era demostrar primero que una teoría admite la eliminación de cuantificadores y después demostrar la decidibilidad o completitud considerando únicamente las fórmulas sin cuantificadores. Esta técnica sirve para demostrar que la aritmética de Presburger es decidible.

Algunas teorías pueden ser decidibles y no admitir eliminación de cuantificadores. Estrictamente, la teoría de los números naturales aditivos no admitía eliminación de cuantificadores, pero era una expansión de los números naturales aditivos que se demostró que era decidible. Siempre que una teoría en un countable language es decidible, es posible extender su lenguaje con muchas relaciones para garantizar que admite la eliminación de cuantificadores (por ejemplo, se puede introducir un símbolo de relación para cada fórmula).

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

Véase también

• Elimination theory
• Simplificación

Referencias

• Viktor Kuncak and Martin Rinard. "Structural Subtyping of Non-Recursive Types is Decidable". In Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003.

• Datos: Q1849020