Eliminació de quantificadors

L'eliminació de quantificadors és un concepte de simplificació utilitzat en la lògica matemàtica, la teoria de models i la informàtica teòrica. Informalment, una declaració quantificada " $\exists x$ tal que $\ldots$ " es pot veure com una pregunta "Quan hi ha un $x$ tal que $\ldots$ ?", i l'enunciat sense quantificadors es pot veure com la resposta a aquesta pregunta.

Una manera de classificar les fórmules és per la quantitat de quantificació. Les fórmules amb menys profunditat d'alternança de quantificadors es consideren més simples, amb les fórmules sense quantificadors com les més simples. Una teoria té eliminació de quantificadors si per a cada fórmula $\alpha$, existeix una altra fórmula $\alpha _{QF}$ sense quantificadors que li siguin equivalents (mòdul aquesta teoria).

Exemples

Un exemple de les matemàtiques diu que un polinomi quadràtic d' una sola variable té una arrel real si i només si el seu discriminant no és negatiu:

$\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í l'oració del costat esquerre implica un quantificador $\exists x\in \mathbb {R}$, mentre que la frase equivalent de la dreta no.

Exemples de teories que s'han demostrat que són determinables mitjançant l'eliminació de quantificadors són l'aritmètica de Presburger, camps tancats algebraicament, camps tancats reals, àlgebres booleanes sense àtoms, àlgebra de termes, ordres lineals densos, grups abelià, gràfics aleatoris, així com moltes de les seves combinacions com ara àlgebra de Boole amb aritmètica de Presburger i àlgebres de termes amb cues.

L'eliminador de quantificadors per a la teoria dels nombres reals com a grup additiu ordenat és l'eliminació de Fourier-Motzkin ; per a la teoria del camp dels nombres reals és el teorema de Tarski-Seidenberg.

L'eliminació de quantificadors també es pot utilitzar per demostrar que "combinar" teories decidibles condueix a noves teories decidibles (vegeu el teorema de Feferman-Vaught).

Algorismes i decidibilitat

Si una teoria té eliminació de quantificadors, llavors es pot abordar una pregunta específica: hi ha un mètode per determinar $\alpha _{QF}$ per a cadascun $\alpha$ ? Si existeix aquest mètode, l'anomenem algorisme d'eliminació de quantificadors. Si hi ha un algorisme d'aquest tipus, aleshores la decisió de la teoria es redueix a decidir la veritat de les oracions lliures de quantificadors. Les oracions lliures de quantificadors no tenen variables, de manera que sovint es pot calcular la seva validesa en una teoria determinada, cosa que permet l'ús d'algorismes d'eliminació de quantificadors per decidir la validesa de les frases.

Conceptes relacionats

Diverses idees teòriques de models estan relacionades amb l'eliminació de quantificadors, i hi ha diverses condicions equivalents.

Tota teoria de primer ordre amb eliminació de quantificadors és model complet. Per contra, una teoria del model complet, la teoria de les conseqüències universals de la qual té la propietat d'amalgamació, té eliminació del quantificador.

Els models de la teoria de les conseqüències universals d'una teoria $T$ són precisament les subestructures dels models de $T$. La teoria d'ordres lineals no té eliminació de quantificadors. Tanmateix, la teoria de les seves conseqüències universals té la propietat d'amalgamació.

Idees bàsiques

Per demostrar constructivament que una teoria té eliminació de quantificadors, n'hi ha prou amb demostrar que podem eliminar un quantificador existencial aplicat a una conjunció de literals, és a dir, demostrar que cada fórmula de la forma:

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

on cadascun $L_{i}$ és un literal, és equivalent a una fórmula sense quantificador. De fet, suposem que sabem com eliminar els quantificadors de les conjuncions de literals, llavors si $F$ és una fórmula lliure de quantificador, podem escriure-la en forma normal disjuntiva

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

i utilitzar el fet que

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

és equivalent a

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

Finalment, eliminar un quantificador universal

$\forall x.F$

on $F$ està lliure de quantificadors, ens transformem $\lnot F$ en forma normal disjuntiva, i utilitzeu el fet que $\forall x.F$ és equivalent a $\lnot \exists x.\lnot F.$

Relació amb la decidibilitat

A la teoria primerenca de models, l'eliminació de quantificadors es va utilitzar per demostrar que diverses teories posseeixen propietats com la decidibilitat i la integritat. Una tècnica comuna va ser mostrar primer que una teoria admet l'eliminació de quantificadors i després demostrar la capacitat de decidir o la integritat considerant només les fórmules lliures de quantificadors. Aquesta tècnica es pot utilitzar per demostrar que l'aritmètica de Presburger és decidible.

Les teories podrien ser decidibles però no admeten l'eliminació de quantificadors. En sentit estricte, la teoria dels nombres naturals additius no admetia l'eliminació de quantificadors, però era una expansió dels nombres naturals additius que es va demostrar que era decidible. Sempre que una teoria és decidible, i el llenguatge de les seves fórmules vàlides és comptable, és possible estendre la teoria amb moltes relacions comptables per tenir eliminació del quantificador (per exemple, es pot introduir, per a cada fórmula de la teoria, un símbol de relació que relaciona les variables lliures de la fórmula)

Exemple: Nullstellensatz per a camps tancats algebraicament i per a camps tancats diferencialment.