Eliminação de quantificadores

Eliminação de quantificadores é um conceito de simplificação usado na lógica matemática, teoria dos modelos, e ciência da computação teórica. Um meio de classificar fórmulas é pelo número de quantificadores. Fórmulas com menos alternância entre os quantificadores são consideradas mais simples, sendo a fórmula livre de quantificadores a mais simples. Uma teoria possui eliminação de quantificadores se para cada fórmula $\alpha$, existe outra fórmula $\alpha _{QF}$ sem quantificadores que é logicamente equivalente a ela.

Exemplos

Exemplos de teorias provadas decidíveis usando eliminação de quantificadores são aritmética de Presburger, teoria de um corpo algebricamente fechado numa dada característica, teoria de um corpo real fechado, álgebra booleana, álgebra de termos, teoria das ordens lineares densas, grafos aleatórios, além de muitas de suas combinações tais quais álgebra booleana com aritmética de Presburger, e álgebra de termos com teoria das filas.

A eliminação de quantificadores para a teoria dos números reais como um grupo ordenado com soma é a eliminação de Fourier–Motzkin; para a teoria dos números reais como corpo é o teorema de Tarski–Seidenberg.

Eliminação de quantificadores pode também ser usada para mostrar que "combinar" teorias decidíveis nos leva a novas teorias decidíveis.

Algoritmos e decidibilidade

Se uma teoria possui uma eliminação de quantificadores, então uma questão pode ser feita: Há um método de determinar $\alpha _{QF}$ para cada $\alpha$? Se há tal método, o chamaremos de algoritmo de eliminação de quantificadores. Se houver este algoritmo, então a decidibilidade para a teoria se reduz a decidir o valor verdade de sentenças livres de quantificadores. Sentenças livres de quantificadores não possuem variáveis, então sua validade em uma dada teoria pode quase sempre ser computada, o que justifica o uso do algoritmo da eliminação de quantificadores para decidir a validade de sentenças.

Conceitos relacionados

Várias ideias de teoria dos modelos são relacionadas a eliminação de quantificadores, e existem várias condições equivalentes.

Cada teoria com eliminação de quantificadores é uma teoria modelo-completa.

Uma teoria de primeira ordem T possui eliminação de quantificadores se e somente se para cada dois modelos quaisquer B e C de T e para qualquer subestrutura comum A de B em C, B e C são elementarmente equivalentes na linguagem de T com a adição de constantes de A. De fato, é suficiente aqui mostrar que qualquer sentença com somente quantificadores existenciais tem o mesmo valor verdade em B e C.

Ideia básica

Para mostrar construtivamente que uma teoria tem eliminação de quantificadores, é suficiente mostrar que podemos eliminar um quantificador existencial aplicado a uma conjunção de literais, isto é, mostrar que cada fórmula é da forma:

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

onde cada $L_{i}$ é um literal, é equivalente a uma fórmula livre de quantificadores. Suponha que sabemos como eliminar quantificadores de conjunções de fórmulas, então se $F$ for uma fórmula livre de quantificadores, podemos escrevê-la na forma normal disjuntiva

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

e usar o fato de que

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

é equivalente a

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

Finalmente, para eliminar um quantificador universal

$\forall x.F$

onde $F$ é livre de quantificadores, convertemos $\lnot F$ na forma normal disjuntiva, e usamos o fato de que $\forall x.F$ é equivalente a $\lnot \exists x.\lnot F.$

História

Na recente teoria dos modelos, eliminação de quantificadores foi usada para demonstrar que várias teorias possuem certas propriedades da teoria dos modelos como decidibilidade e completude. Uma técnica comum foi mostrar primeiro que uma teoria admite eliminação de quantificadores e posteriormente provar a decidibilidade ou completude considerando só as fórmulas livres de quantificadores. Esta técnica é usada para demonstrar que a aritmética de Presburger, i.e. a teoria dos números naturais com soma, é decidível.

Teorias podem ser decidíveis mesmo não admitindo eliminação de quantificadores. Estritamente falando, a teoria dos números naturais com soma não admite eliminação de quantificadores, mas foi uma expansão da teoria dos números naturais com soma que foi demonstrada decidível. Sempre que uma teoria em uma linguagem contável é decidível, é possível estender sua linguagem com várias relações contáveis para assegurar que ela admite eliminação de quantificadores (por exemplo, podemos introduzir um símbolo de relação para cada formula).

Exemplo: Nullstellensatz em ACF and DCF.

Referências

• Wilfrid Hodges. "Model Theory". Cambridge University Press. 1993.
• Viktor Kuncak and Martin Rinard. "Structural Subtyping of Non-Recursive Types is Decidable". In Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003.