En lógica matemática , un cuantificador de Lindström es un cuantificador poliádico generalizado . Los cuantificadores de Lindström generalizan cuantificadores de primer orden, como el cuantificador existencial , el cuantificador universal y los cuantificadores de conteo . Fueron introducidos por Per Lindström en 1966. Posteriormente se estudiaron por sus aplicaciones en lógica en informática y lenguajes de consulta de bases de datos .
Para facilitar la discusión, es necesario explicar algunas convenciones de notación. La expresión
para A una L -estructura (o L -modelo) en un lenguaje L , φ una L -fórmula, y una tupla de elementos del dominio dom( A ) de A . [ aclaración necesaria ] En otras palabras, denota una propiedad ( monádica ) definida en dom(A ). En general, donde x se reemplaza por una n -tupla de variables libres, denota una relación n -aria definida en dom( A ). Cada cuantificador se relativiza a una estructura, ya que cada cuantificador se ve como una familia de relaciones (entre relaciones) en esa estructura. Para un ejemplo concreto, tomemos los cuantificadores universales y existenciales ∀ y ∃, respectivamente. Sus condiciones de verdad se pueden especificar como
donde es el singleton cuyo único miembro es dom( A ), y es el conjunto de todos los subconjuntos no vacíos de dom( A ) (es decir, el conjunto potencia de dom( A ) menos el conjunto vacío). En otras palabras, cada cuantificador es una familia de propiedades en dom( A ), por lo que cada uno se llama cuantificador monádico . Cualquier cuantificador definido como una relación n > 0-aria entre propiedades en dom( A ) se llama monádico . Lindström introdujo los poliádicos que son relaciones n > 0-arias entre relaciones en dominios de estructuras.
Antes de continuar con la generalización de Lindström, observe que cualquier familia de propiedades en dom( A ) puede considerarse un cuantificador generalizado monádico. Por ejemplo, el cuantificador "hay exactamente n cosas tales que..." es una familia de subconjuntos del dominio de una estructura, cada uno de los cuales tiene una cardinalidad de tamaño n . Entonces, "hay exactamente 2 cosas tales que φ" es verdadero en A si y solo si el conjunto de cosas que son tales que φ es un miembro del conjunto de todos los subconjuntos de dom( A ) de tamaño 2.
Un cuantificador de Lindström es un cuantificador generalizado poliádico, por lo que en lugar de ser una relación entre subconjuntos del dominio, es una relación entre relaciones definidas en el dominio. Por ejemplo, el cuantificador se define semánticamente como
dónde
para una n -tupla de variables.
Los cuantificadores de Lindström se clasifican según la estructura numérica de sus parámetros. Por ejemplo, es un cuantificador de tipo (1,1), mientras que es un cuantificador de tipo (2). Un ejemplo de cuantificador de tipo (1,1) es el cuantificador de Hartig que prueba la equicardinalidad, es decir, la extensión de {A, B ⊆ M: |A| = |B|}. [ aclaración necesaria ] Un ejemplo de un cuantificador de tipo (4) es el cuantificador de Henkin .
El primer resultado en esta dirección lo obtuvo Lindström (1966), que demostró que un cuantificador de tipo (1,1) no era definible en términos de un cuantificador de tipo (1). Después de que Lauri Hella (1989) desarrollara una técnica general para demostrar la expresividad relativa de los cuantificadores, la jerarquía resultante resultó estar ordenada lexicográficamente por tipo de cuantificador:
Para cada tipo t , existe un cuantificador de ese tipo que no es definible en la lógica de primer orden extendida con cuantificadores que son de tipos menores que t .
Aunque Lindström había desarrollado sólo parcialmente la jerarquía de cuantificadores que ahora lleva su nombre, le bastó con observar que algunas propiedades interesantes de la lógica de primer orden se pierden cuando se extiende con ciertos cuantificadores generalizados. Por ejemplo, añadir un cuantificador del tipo "existen un número finito" da como resultado una pérdida de compacidad , mientras que añadir un cuantificador del tipo "existen un número incontable" a la lógica de primer orden da como resultado una lógica que ya no satisface el teorema de Löwenheim-Skolem . En 1969, Lindström demostró un resultado mucho más fuerte, ahora conocido como el teorema de Lindström , que afirma intuitivamente que la lógica de primer orden es la lógica "más fuerte" que tiene ambas propiedades.