Quantificador Delimitado

No estudo de teorias formais em lógica matemática, os quantificadores delimitados são muitas vezes adicionados para uma linguagem em adição aos quantificadores padrão "∀" e "∃". Quantificadores delimitados diferem de "∀" e "∃" em que os quantificadores delimitados restringem a gama da variável quantificada. O estudo de quantificadores delimitados é motivado pelo fato de determinar se uma sentença com apenas quantificadores delimitados é verdade, muitas vezes não é tão difícil quanto determinar se uma sentença arbitrária é verdade.

Exemplos de quantificadores delimitados no contexto da análise real incluem "∀x> 0", "∃y <0", e "∀x ε ℝ". Informalmente "∀x> 0" diz "para todos os x, onde x é maior do que 0", "∃y <0" diz que "existe um y, onde y é menor que 0" e "∀x ε ℝ" diz "para todo x em que x é um número real ". Por exemplo, "∀x> 0 ∃y <0 (x = y²)", diz "cada número positivo é o quadrado de um número negativo".

Quantificadores delimitados na aritmética

Suponha que L seja a linguagem da aritmética de Peano (a linguagem da aritmética de segunda ordem ou aritmética sobre todos os tipos finitos iriam funcionar também). Existem dois tipos de quantificadores delimitados: $\forall n<t$ and $\exists n<t$. Estes quantificadores vinculam uma variável número n e contêm um termo t numérico que pode não mencionar n, mas que pode ter outras variáveis livres. (Por "termos numéricos" aqui queremos dizer termos tais como "1 + 1", "2", "2 × 3", "m + 3", etc.)

Estes quantificadores são definidos pelas seguintes regras (\ phi denota fórmulas):

Há várias motivações para esses quantificadores.

• Em aplicações da linguagem de teoria da recursão, tais como a hierarquia da aritmética, quantificadores delimitados não acrescentam complexidade. Se $\phi$ é um predicado decidível, então $\exists n<t\,\phi$ e $\forall n<t\,\phi$ são decidívisl também.
• Em aplicações ao estudo da aritmética de Peano, fórmulas são, por vezes, demonstráveis com quantificadores delimitados mas improvável com quantificadores delimitados.

Por exemplo, existe uma definição de primalidade usando apenas quantificadores delimitados. Um número n é primo se, e somente se não houver dois números estritamente menor que n, cujo produto é n. Não existe uma definição sem quantificador de primalidade na línguagem $\langle 0,1,+,\times ,<,=\rangle$, no entanto. O fato de existir uma fórmula de quantificador delimitado de primalidade mostra que a primalidade de cada número pode ser decidida computacionalmente.

De um modo geral, uma relação de números naturais é definida por uma fórmula limitada, se e somente se, é computável na hierarquia de tempo-linear, a qual é definida de modo semelhante à hierarquia polinomial, mas com limites lineares de tempo em vez de polinomial. Consequentemente, todos os predicados definidos por uma fórmula limitada são Kalmár elementar, sensível ao contexto, e primitiva recursiva.

Na hierarquia aritmética, uma fórmula aritmética que contém apenas quantificadores delimitados é chamado $\Sigma _{0}^{0}$, $\Delta _{0}^{0}$, e $\Pi _{0}^{0}$. O expoente 0 as vezes é omitido.

Quantificadores delimitados na teoria dos conjuntos

Suponha que L seja a línguagem $\langle \in ,\ldots ,=\rangle$ da teoria dos conjuntos de Zermelo-Fraenkel, onde as reticências podem ser substituídas por operações de formação de termos, tais como um símbolo para a operação de conjunto das partes. Há dois quantificadores delimitados:$\forall x\in t$ and $\exists x\in t$. Estes quantificadores vinculam a variável x do conjunto e contêm um termo t que não pode mencionar x, mas que pode ter outras variáveis livres.

A semântica destes quantificadores é determinada pelas regras seguintes:

$\exists x\in t\ (\phi )\Leftrightarrow \exists x(x\in t\land \phi )$

$\forall x\in t\ (\phi )\Leftrightarrow \forall x(x\in t\rightarrow \phi )$

Uma fórmula ZF que contém apenas quantificadores delimitados é chamada $\Sigma _{0}$, $\Delta _{0}$, e $\Pi _{0}$. Isto forma a base da hierarquia de Levy, que é definida analogamente com a hierarquia da aritmética.

Quantificadores delimitados são importantes na teoria dos conjuntos de Kripke-Platek  e na teoria dos conjuntos construtiva, onde apenas Δ₀-separação está incluída. Ou seja, inclui separação para fórmulas com apenas quantificadores delimitados, mas não a separação de outras fórmulas. Em KP a motivação é o fato de que se um conjunto x satisfaz uma fórmula com quantificador delimitado, só depende da coleção de conjuntos que estão próximos ao posto de x (como a operação dos conjuntos de subconjuntos só pode ser aplicado um número finito de vezes para formar um termo). Na teoria dos conjuntos construtiva, isso é motivado por razões predicativas.

Ver também

• Subtyping — bounded quantification in type theory
• System F_<: — a polymorphic typed lambda calculus with bounded quantification

Referências

• Hinman, P. (2005). Fundamentals of Mathematical Logic. [S.l.]: A K Peters. ISBN 1-56881-262-0 
• Kunen, K. (1980). Set theory: An introduction to independence proofs. [S.l.]: Elsevier. ISBN 0-444-86839-9