Eliminación de cuantificadores

Técnica de simplificación en lógica matemática.

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

Una forma de clasificar las fórmulas es por la cantidad de cuantificación . Las fórmulas con menos 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 esta teoría). ${\displaystyle \alpha }$ ${\displaystyle \alpha _{QF}}$

Ejemplos

Un ejemplo de matemáticas de secundaria dice que un polinomio cuadrático de una sola variable tiene una raíz real si y sólo si su discriminante no es 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 implica un cuantificador , mientras que la oración equivalente del lado derecho no. ${\displaystyle \exists x\in \mathbb {R} }$

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

El eliminador de cuantificadores para la teoría de los números reales como grupo aditivo ordenado es la eliminación de Fourier-Motzkin ; para la teoría del campo de números reales es el teorema de Tarski-Seidenberg . ^[7]

La eliminación de cuantificadores también se puede utilizar para demostrar que "combinar" teorías decidibles conduce a nuevas teorías decidibles (ver teorema de Feferman-Vaught ).

Algoritmos y decidibilidad

Si una teoría tiene eliminación de cuantificadores, entonces se puede abordar una pregunta específica: ¿Existe un método de determinación para cada uno ? 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 libres de cuantificadores . Las oraciones sin cuantificadores no tienen variables, por lo que a menudo se puede calcular su validez en una teoría determinada, lo que permite el uso de algoritmos de eliminación de cuantificadores para decidir la validez de las oraciones. ${\displaystyle \alpha _{QF}}$ ${\displaystyle \alpha }$

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 . Por el contrario, una teoría de 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 los órdenes lineales no tiene eliminación de cuantificadores. Sin embargo, la teoría de sus consecuencias universales tiene la propiedad de amalgama. ${\displaystyle T}$ ${\displaystyle T}$

Ideas básicas

Para demostrar constructivamente que una teoría tiene eliminación de cuantificadores, basta 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 uno es un literal, equivale a una fórmula sin cuantificadores. De hecho, supongamos que sabemos cómo eliminar cuantificadores de conjunciones de literales, entonces, si es una fórmula sin cuantificadores, podemos escribirla en forma normal disyuntiva. ${\displaystyle L_{i}}$ ${\displaystyle F}$

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

y utilizar 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 x.F}$

donde está libre de cuantificadores, lo transformamos a la forma normal disyuntiva y usamos el hecho de que es equivalente a ${\displaystyle F}$ ${\displaystyle \lnot F}$ ${\displaystyle \forall x.F}$ ${\displaystyle \lnot \exists x.\lnot F.}$

Relación con la decidibilidad

En las primeras teorías de modelos, la eliminación de cuantificadores se utilizaba para demostrar que varias teorías poseen propiedades como decidibilidad y completitud . Una técnica común era mostrar primero que una teoría admite la eliminación de cuantificadores y luego demostrar la decidibilidad o la integridad considerando sólo las fórmulas sin 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 de cuantificadores. Estrictamente hablando, la teoría de los números naturales aditivos no admitía la eliminación de cuantificadores, sino que era una expansión de los números naturales aditivos la que demostraba 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 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 relaciona las variables libres de la fórmula).

Ejemplo: Nullstellensatz para campos algebraicamente cerrados y para campos diferencialmente cerrados . ^{[ se necesita aclaración ]}

Ver también

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

Notas

1. Brown 2002.
2. Presburgo 1929.
3. Mente: aritmética básica de Presburger - - no admite eliminación de cuantificadores. Nipkow (2010): "La aritmética de Presburger necesita un predicado de divisibilidad (o congruencia) '|' para permitir la eliminación del cuantificador". ${\displaystyle \langle \mathbb {N} ,+,0,1\rangle }$
4. Grädel y col. (2007, p. 20) definen la aritmética de Presburger como . Esta extensión sí admite eliminación de cuantificadores. ${\displaystyle \langle \mathbb {N} ,+,<,0,1,(\equiv _{k})_{k>0}\rangle {\text{ where }}x\equiv _{k}y{\text{ iff }}x=y(\mod {k})}$
5. Monje 2012, pag. 240.
6. Enderton 2001, pág. 188.
7. Grädel et al. 2007.
8. Fried y Jardín 2008, pag. 171.
9. Szmielew 1955, página 229 describe "el método de eliminación de la cuantificación".
10. Hodges 1993.

Referencias

• Brown, Christopher W. (31 de julio de 2002). "¿Qué es la eliminación de cuantificadores?" . Consultado el 30 de agosto de 2023 .

• Cooper, DC (1972). Meltzer, Bernard ; Michie, Donald (eds.). "Demostración de teoremas en aritmética sin multiplicación" (PDF) . Inteligencia de las máquinas . 7 . Edimburgo: Edinburgh University Press: 91–99 . Consultado el 30 de agosto de 2023 .

• Enderton, Herbert (2001). Una introducción matemática a la lógica (2ª ed.). Boston, MA: Prensa académica . ISBN 978-0-12-238452-3.

• Frito, Michael D.; Jarden, Moshe (2008). Aritmética de campo . Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Seguir. vol. 11 (3ª edición revisada). Springer-Verlag . ISBN 978-3-540-77269-9. Zbl  1145.12001.

• Grädel, Erich; Kolaitis, Phokion G .; Libkin, Leónidas ; Martín, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Ydé; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos de Informática Teórica. Una serie EATCS. Berlín: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl  1133.03001.

• Hodges, Wilfrid (1993). Teoría de modelos . Enciclopedia de Matemáticas y sus Aplicaciones. vol. 42. Prensa de la Universidad de Cambridge . doi :10.1017/CBO9780511551574. ISBN 9780521304429.

• Kuncak, Viktor; Rinard, Martín (2003). "La subtipificación estructural de tipos no recursivos es decidible" (PDF) . 18.º Simposio anual de lógica en informática del IEEE, 2003. Actas . págs. 96-107. doi :10.1109/LICS.2003.1210049. ISBN 0-7695-1884-2. S2CID  14182674.

• Monje, J. Donald (2012). Lógica Matemática (Textos de Graduado en Matemáticas (37)) (Reimpresión en tapa blanda de la 1ª ed. original, edición de 1976). Saltador. ISBN 9781468494549.

• Nipkow, Tobías (2010). "Eliminación de cuantificadores lineales" (PDF) . Revista de razonamiento automatizado . 45 (2): 189–212. doi :10.1007/s10817-010-9183-0. S2CID  14279141 . Consultado el 12 de noviembre de 2022 .

• Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem ​​die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa : 92–101., ver Stansifer (1984) para una traducción al inglés.

• Stansifer, Ryan (septiembre de 1984). Artículo de Presburger sobre aritmética de enteros: comentarios y traducción (PDF) (Informe técnico). vol. TR84-639. Ithaca, Nueva York: Departamento de Ciencias de la Computación, Universidad de Cornell.

• Szmielew, Wanda (1955). "Propiedades elementales de los grupos abelianos". Fundamentos Mathematicae . 41 (2): 203–271. doi : 10.4064/fm-41-2-203-271 . SEÑOR  0072131.

• Jeannerod, Nicolás; Treinen, Ralf. Decidir la teoría de primer orden de un álgebra de árboles de características con actualizaciones . Conferencia conjunta internacional sobre razonamiento automatizado (IJCAR). doi :10.1007/978-3-319-94205-6_29.

• Sturm, Thomas (2017). "Un estudio de algunos métodos para la eliminación, decisión y satisfacibilidad de cuantificadores reales y sus aplicaciones". Matemáticas en Informática . 11 (3–4): 483–502. doi : 10.1007/s11786-017-0319-z . hdl : 11858/00-001M-0000-002C-A3B5-B .