La eliminación de cuantificadores es un concepto de simplificación utilizado en lógica matemática , teoría de modelos e informática teórica . De manera informal, una declaración cuantificada " tal que "puede verse como una pregunta" ¿Cuándo hay una tal que ? ", y la declaración sin cuantificadores puede verse como la respuesta a esa pregunta. [1]
Una forma de clasificar fórmulas es por la cantidad de cuantificación . Las fórmulas con menos profundidad de alternancia de cuantificadores se consideran más simples, y las fórmulas sin cuantificadores son las más simples. Una teoría tiene eliminación de cuantificadores si para cada fórmula, existe otra fórmula sin cuantificadores que sea equivalente a él ( módulo esta teoría).
Ejemplos de
Un ejemplo de matemáticas de la escuela secundaria dice que un polinomio cuadrático de una sola variable tiene una raíz real si y solo si su discriminante no es negativo: [1]
Aquí la oración del lado izquierdo implica un cuantificador , mientras que la oración equivalente de la derecha no lo hace.
Ejemplos de teorías que han demostrado ser decidibles mediante la eliminación de cuantificadores son la aritmética de Presburger , [2] campos algebraicamente cerrados , campos cerrados reales , [2] [3] álgebras booleanas sin átomos , álgebras de términos , órdenes lineales densos , [2] grupos abelianos , [ 4] gráficos aleatorios , así como muchas de sus combinaciones, como álgebra de Boole con aritmética de Presburger y álgebras de términos con colas .
El eliminador del cuantificador 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 campo de los números reales es el teorema de Tarski-Seidenberg . [2]
La eliminación del cuantificador también se puede utilizar para mostrar que la "combinación" de teorías decidibles conduce a nuevas teorías decidibles.
Algoritmos y decidibilidad
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 cuantificador . Si existe tal algoritmo, entonces la decidibilidad de la teoría se reduce a decidir la verdad de las oraciones libres de cuantificadores . Las oraciones sin cuantificadores no tienen variables, por lo que su validez en una teoría dada a menudo se puede calcular, lo que permite el uso de algoritmos de eliminación de cuantificadores para decidir la validez de las oraciones.
Conceptos relacionados
Varias ideas de la 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 un modelo completo . A la inversa, una teoría de modelo completo, cuya teoría de las consecuencias universales tiene la propiedad de amalgama , tiene eliminación de cuantificador. [5]
Los modelos de la teoría de las consecuencias universales de una teoría son precisamente las subestructuras de los modelos de. [5] 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 fusión.
Ideas basicas
Para mostrar constructivamente 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:
donde cada 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 sies una fórmula libre de cuantificadores, podemos escribirla en forma normal disyuntiva
y usa el hecho de que
es equivalente a
Finalmente, para eliminar un cuantificador universal
dónde es libre de cuantificadores, transformamos en forma normal disyuntiva, y utilice el hecho de que es equivalente a
Relación con la decidibilidad
En la teoría de modelos temprana, la eliminación de cuantificadores se utilizó para demostrar que varias teorías poseen propiedades como decidibilidad y completitud . Una técnica común fue mostrar primero que una teoría admite la eliminación de cuantificadores y luego probar la decidibilidad o la completitud considerando solo las fórmulas libres de cuantificadores. Esta técnica se puede utilizar para demostrar que la aritmética de Presburger es decidible.
Las teorías podrían ser decidibles pero no admitir la eliminación del cuantificador. Estrictamente hablando, la teoría de los números naturales aditivos no admitía la eliminación del cuantificador, pero fue una expansión de los números naturales aditivos la que demostró ser decidible. Siempre que una teoría es decidible, y el lenguaje de sus fórmulas válidas es contable , es posible extender la teoría con muchas relaciones contables para tener eliminación de cuantificador (por ejemplo, uno puede introducir, para cada fórmula de la teoría, un símbolo de relación que relaciona las variables libres de la fórmula). [ cita requerida ]
Ejemplo: Nullstellensatz para campos algebraicamente cerrados y para campos diferencialmente cerrados . [ aclaración necesaria ]
Ver también
- Descomposición algebraica cilíndrica
- Teoría de la eliminación
- Eliminación de conjunciones
Notas
- ↑ a b Brown, Christopher W. (31 de julio de 2002). "¿Qué es la eliminación del cuantificador" . Consultado el 30 de agosto de 2018 .
- ^ a b c d Grädel, Erich; Kolaitis, Phokion G .; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos en Informática Teórica. Una serie EATCS. Berlín: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 .
- ^ Fried, Michael D .; Jarden, Moshe (2008). Aritmética de campo . Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge. 11 (tercera edición revisada). Springer-Verlag . pag. 171. ISBN 978-3-540-77269-9. Zbl 1145.12001 .
- ^ Szmielew, W. (1955). "Propiedades elementales de los grupos abelianos" . Fundamenta Mathematicae . 41 (2): 203–271. doi : 10.4064 / fm-41-2-203-271 . Señor 0072131 .
- ↑ a b Hodges, Wilfrid (1993). Teoría de modelos. Prensa de la Universidad de Cambridge
Referencias
- Viktor Kuncak y Martin Rinard. " Subtipado estructural de tipos no recursivos es decidible ". En el Decimoctavo Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación, 2003.