En el estudio de las teorías formales en lógica matemática , los cuantificadores acotados (también conocidos como cuantificadores restringidos ) se incluyen con frecuencia en un lenguaje formal, además de los cuantificadores estándar "∀" y "∃". Los cuantificadores acotados se diferencian de "∀" y "∃" en que restringen el rango de la variable cuantificada. El estudio de los cuantificadores acotados se justifica por el hecho de que determinar si una oración con solo cuantificadores acotados es verdadera suele ser menos difícil que determinar si una oración arbitraria es verdadera.
Ejemplos
Algunos ejemplos de cuantificadores acotados en el contexto del análisis real son:
- - para todo x donde x es mayor que 0
- - existe un y donde y es menor que 0
- - para todo x donde x es un número real
- - todo número positivo es el cuadrado de un número negativo.
Cuantificadores acotados en aritmética
Supongamos que L es el lenguaje de la aritmética de Peano (el lenguaje de la aritmética de segundo orden o la aritmética en todos los tipos finitos también servirían). Hay dos tipos de cuantificadores acotados:yEstos cuantificadores vinculan la variable numérica n mediante un término numérico t que no contiene n, pero que puede tener otras variables libres. (Aquí, "términos numéricos" se refiere a términos como "1 + 1", "2", "2 × 3", " m + 3", etc.)
Estos cuantificadores se definen mediante las siguientes reglas (denota fórmulas):
Existen varias razones para el uso de estos cuantificadores.
- En las aplicaciones del lenguaje a la teoría de la computabilidad , como la jerarquía aritmética , los cuantificadores acotados no añaden complejidad. Sies un predicado decidible entoncesyTambién son decidibles.
- En aplicaciones al estudio de la aritmética de Peano , el hecho de que un conjunto particular pueda definirse solo con cuantificadores acotados puede tener consecuencias para la computabilidad del conjunto. Por ejemplo, existe una definición de primalidad que utiliza solo cuantificadores acotados: un número n es primo si y solo si no hay dos números estrictamente menores que n cuyo producto sea n . No existe una definición de primalidad sin cuantificadores en el lenguaje.Sin embargo, el hecho de que exista una fórmula cuantificadora acotada que defina la primalidad demuestra que la primalidad de cada número puede decidirse computacionalmente.
En general, una relación sobre números naturales se puede definir mediante una fórmula acotada si y solo si es computable en la jerarquía de tiempo lineal, que se define de forma similar a la jerarquía polinómica , pero con límites de tiempo lineales en lugar de polinómicos. Por consiguiente, todos los predicados definibles mediante una fórmula acotada son elementales de Kalmár , sensibles al contexto y recursivos primitivos .
En la jerarquía aritmética , una fórmula aritmética que contiene solo cuantificadores acotados se llama,, yEn ocasiones, se omite el superíndice 0.
Cuantificadores acotados en la teoría de conjuntos
Supongamos que L es el lenguajede la teoría de conjuntos de Zermelo-Fraenkel , donde la elipsis puede ser reemplazada por operaciones de formación de términos, como un símbolo para la operación de conjunto potencia . Hay dos cuantificadores acotados:yEstos cuantificadores vinculan la variable de conjunto x y contienen un término t que puede no mencionar x pero que puede tener otras variables libres.
La semántica de estos cuantificadores está determinada por las siguientes reglas:
Una fórmula ZF que contiene solo cuantificadores acotados se llama,, yEsto constituye la base de la jerarquía de Lévy , que se define de forma análoga a la jerarquía aritmética.
Los cuantificadores acotados son importantes en la teoría de conjuntos de Kripke-Platek y en la teoría constructiva de conjuntos , donde solo se incluye la separación Δ₀ . Es decir, incluye la separación para fórmulas con cuantificadores acotados únicamente, pero no para otras fórmulas. En KP, la motivación radica en que el hecho de que un conjunto x satisfaga una fórmula con cuantificadores acotados depende únicamente de la colección de conjuntos de rango cercano a x (ya que la operación de conjunto potencia solo puede aplicarse un número finito de veces para formar un término). En la teoría constructiva de conjuntos, la motivación se basa en principios predicativos .
Véase también
- Subtipificación : cuantificación acotada en la teoría de tipos.
- Sistema F <: — un cálculo lambda polimórfico tipado con cuantificación acotada
Referencias
- Cuantificador (lógica)
- Teoría de la demostración
- teoría de la computabilidad