En matemáticas y lógica , una lógica de orden superior (abreviada HOL ) es una forma de lógica que se distingue de la lógica de primer orden por cuantificadores adicionales y, a veces, una semántica más fuerte . Las lógicas de orden superior con su semántica estándar son más expresivas, pero sus propiedades de teoría de modelos se comportan peor que las de la lógica de primer orden.
El término "lógica de orden superior" se utiliza comúnmente para referirse a la lógica predicativa simple de orden superior . Aquí, "simple" indica que la teoría de tipos subyacente es la teoría de tipos simples , también llamada teoría simple de tipos . Leon Chwistek y Frank P. Ramsey propusieron esto como una simplificación de la complicada y torpe teoría ramificada de tipos especificada en los Principia Mathematica de Alfred North Whitehead y Bertrand Russell . Los tipos simples a veces también se utilizan para excluir los tipos polimórficos y dependientes . [1]
La lógica de primer orden cuantifica sólo variables que abarcan individuos; la lógica de segundo orden también cuantifica conjuntos; la lógica de tercer orden también cuantifica conjuntos de conjuntos, y así sucesivamente.
La lógica de orden superior es la unión de la lógica de primer, segundo, tercer, ..., n -ésimo orden; es decir, la lógica de orden superior admite la cuantificación sobre conjuntos anidados de forma arbitrariamente profunda.
Hay dos semánticas posibles para la lógica de orden superior.
En la semántica estándar o completa , los cuantificadores sobre objetos de tipo superior abarcan todos los objetos posibles de ese tipo. Por ejemplo, un cuantificador sobre conjuntos de individuos abarca todo el conjunto potencia del conjunto de individuos. Por lo tanto, en la semántica estándar, una vez que se especifica el conjunto de individuos, esto es suficiente para especificar todos los cuantificadores. HOL con semántica estándar es más expresivo que la lógica de primer orden. Por ejemplo, HOL admite axiomatizaciones categóricas de los números naturales y de los números reales , que son imposibles con la lógica de primer orden. Sin embargo, por un resultado de Kurt Gödel , HOL con semántica estándar no admite un cálculo de prueba efectivo , sólido y completo . [2] Las propiedades de teoría de modelos de HOL con semántica estándar también son más complejas que las de la lógica de primer orden. Por ejemplo, el número de Löwenheim de la lógica de segundo orden ya es mayor que el primer cardinal medible , si tal cardinal existe. [3] El número de Löwenheim de la lógica de primer orden, por el contrario, es ℵ , el cardinal infinito más pequeño.
En la semántica de Henkin , se incluye un dominio separado en cada interpretación para cada tipo de orden superior. Así, por ejemplo, los cuantificadores sobre conjuntos de individuos pueden abarcar solo un subconjunto del conjunto potenciado del conjunto de individuos. HOL con esta semántica es equivalente a la lógica de primer orden de múltiples ordenamientos , en lugar de ser más fuerte que la lógica de primer orden. En particular, HOL con semántica de Henkin tiene todas las propiedades de teoría de modelos de la lógica de primer orden y tiene un sistema de prueba completo, sólido y efectivo heredado de la lógica de primer orden.
Las lógicas de orden superior incluyen las derivaciones de la teoría simple de tipos de Church [4] y las diversas formas de la teoría de tipos intuicionista . Gérard Huet ha demostrado que la unificación es indecidible en un tipo de lógica de tercer orden basado en la teoría de tipos, [5] [6] [7] [8] es decir, no puede haber ningún algoritmo para decidir si una ecuación arbitraria entre términos de segundo orden (y mucho menos de orden superior arbitrarios) tiene una solución.
Hasta un cierto grado de isomorfismo , la operación de conjunto potencia es definible en lógica de segundo orden. Utilizando esta observación, Jaakko Hintikka estableció en 1955 que la lógica de segundo orden puede simular lógicas de orden superior en el sentido de que para cada fórmula de una lógica de orden superior, se puede encontrar una fórmula equisatisfacible para ella en lógica de segundo orden. [9]
En algunos contextos se supone que el término "lógica de orden superior" se refiere a la lógica clásica de orden superior. Sin embargo, también se ha estudiado la lógica modal de orden superior. Según varios lógicos, la prueba ontológica de Gödel se estudia mejor (desde una perspectiva técnica) en un contexto de este tipo. [10]
El argumento de Gödel es modal y al menos de segundo orden, puesto que en su definición de Dios hay una cuantificación explícita sobre las propiedades. [...] [AG96] mostró que uno podría ver una parte del argumento no como de segundo orden, sino como de tercer orden.