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órica . De manera informal, una afirmación cuantificada " tal que " puede verse como una pregunta "¿Cuándo existe un tal que ?", y la afirmación sin cuantificadores puede verse como la respuesta a esa pregunta. ^[1]${\displaystyle \existe x}$${\displaystyle \ldots}$${\estilo de visualización x}$${\displaystyle \ldots}$

Una forma de clasificar las fórmulas es por la cantidad de cuantificación . Las fórmulas con menor profundidad de alternancia de cuantificadores se consideran 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 existe otra fórmula sin cuantificadores que es equivalente a ella ( módulo de esta teoría). ${\estilo de visualización \alpha}$${\displaystyle \alpha _{QF}}$

Un ejemplo de matemáticas de secundaria 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 \existe x\en \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 implica un cuantificador , mientras que la oración equivalente del lado derecho no. ${\displaystyle \existe x\en \mathbb {R} }$

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

El cuantificador eliminador 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 . ^[7]

La eliminación de cuantificadores también se puede utilizar 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 para cada ? 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 verdad de las oraciones sin cuantificadores . Las oraciones sin cuantificadores no tienen variables, por lo que a menudo se puede calcular su validez en una teoría dada, lo que permite el uso de algoritmos de eliminación de cuantificadores para decidir la validez de las oraciones. ${\displaystyle \alpha _{QF}}$${\estilo de visualización \alpha}$

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

Toda teoría de primer orden con eliminación de cuantificadores es modelo completo . Por el contrario, una teoría modelo completo, cuya teoría de consecuencias universales tiene la propiedad de amalgama , tiene eliminación de cuantificadores. ^[10]

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

Para demostrar de manera 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 cada fórmula de la forma:

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

donde cada uno 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 es una fórmula sin cuantificadores, podemos escribirla en forma normal disyuntiva$Estilo de visualización L_{i}}$${\estilo de visualización F}$

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

y utilizar el hecho de que

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

es equivalente a

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

Finalmente, para eliminar un cuantificador universal

${\displaystyle \paratodos xF}$

donde no tiene cuantificadores, lo transformamos en forma normal disyuntiva y usamos el hecho de que es equivalente a${\estilo de visualización F}$${\displaystyle \lno F}$${\displaystyle \paratodos xF}$${\displaystyle \lno \existe x.\lno F.}$

En la teoría de modelos temprana, se utilizó la eliminación de cuantificadores para demostrar que varias teorías poseen propiedades como decidibilidad y completitud . Una técnica común era demostrar primero que una teoría admite la eliminación de cuantificadores y luego demostrar la decidibilidad o completitud considerando solo las fórmulas sin cuantificadores. Esta técnica se puede utilizar para demostrar que la aritmética de Presburger es decidible.

Las teorías podían ser decidibles y 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 era una expansión de los números naturales aditivos que se demostró que era decidible. Siempre que una teoría sea decidible, y el lenguaje de sus fórmulas válidas sea contable , es posible extender la teoría con un número contable de relaciones para tener 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: Nullstellensatz para campos algebraicamente cerrados y para campos diferencialmente cerrados . ^{[ aclaración necesaria ]}

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