En el estudio de las teorías formales en lógica matemática , los cuantificadores acotados a menudo se incluyen en un lenguaje formal además de los cuantificadores estándar "∀" y "∃". Los cuantificadores acotados difieren de "∀" y "∃" en que los cuantificadores acotados restringen el rango de la variable cuantificada. El estudio de los cuantificadores limitados está motivado por el hecho de que determinar si una oración con solo cuantificadores limitados es verdadera a menudo no es tan difícil como determinar si una oración arbitraria es verdadera.
Ejemplos de
Ejemplos de cuantificadores acotados en el contexto del análisis real incluyen:
- - para todo x donde x es mayor que 0
- - existe una 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 funcionaría). Hay dos tipos de cuantificadores acotados: y . Estos cuantificadores unen la variable numérica ny contienen un término numérico t que puede no mencionar n pero que puede tener otras variables libres. ("Términos numéricos" aquí significa términos como "1 + 1", "2", "2 × 3", " m + 3", etc.)
Estos cuantificadores se definen mediante las siguientes reglas ( denota fórmulas):
Hay varias motivaciones para estos cuantificadores.
- En aplicaciones del lenguaje a la teoría de la recursividad , como la jerarquía aritmética , los cuantificadores acotados no añaden complejidad. Si es un predicado decidible entonces y son decidibles también.
- En aplicaciones al estudio de la aritmética de Peano , el hecho de que un conjunto particular pueda definirse con solo cuantificadores acotados puede tener consecuencias para la computabilidad del conjunto. Por ejemplo, existe una definición de primalidad que usa solo cuantificadores acotados: un número n es primo si y solo si no hay dos números estrictamente menores que n cuyo producto es n . No existe una definición de primalidad libre de cuantificadores en el lenguaje, sin emabargo. El hecho de que exista una fórmula cuantificadora acotada que define la primacía muestra que la primacía de cada número se puede decidir computablemente.
En general, una relación de números naturales se puede definir mediante una fórmula acotada si y solo si se puede calcular en la jerarquía de tiempo lineal, que se define de manera similar a la jerarquía de polinomios , pero con límites de tiempo lineales en lugar de polinomios. En consecuencia, todos los predicados definibles por 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, , y . A veces se omite el superíndice 0.
Cuantificadores acotados en la teoría de conjuntos
Supongamos que L es el idiomade 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 powerset. Hay dos cuantificadores acotados: y . Estos cuantificadores unen 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 , , y . Esto forma 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 de conjuntos constructiva , donde solo se incluye la separación Δ 0 . Es decir, incluye separación para fórmulas con cuantificadores limitados, pero no separación para otras fórmulas. En KP, la motivación es el hecho de que el hecho de que un conjunto x satisfaga una fórmula de cuantificador acotado solo depende de la colección de conjuntos que tienen un rango cercano ax (ya que la operación de conjunto de potencias solo se puede aplicar un número finito de veces para formar un término). En la teoría de conjuntos constructiva, está motivada por motivos predicativos .
Ver también
- Subtipado : cuantificación acotada en teoría de tipos
- Sistema F <: - un cálculo lambda de tipo polimórfico con cuantificación acotada
Referencias
- Hinman, P. (2005). Fundamentos de Lógica Matemática . AK Peters. ISBN 1-56881-262-0.
- Kunen, K. (1980). Teoría de conjuntos: introducción a las pruebas de independencia . Elsevier. ISBN 0-444-86839-9.