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, por una semántica más sólida . Las lógicas de orden superior con su semántica estándar son más expresivas, pero sus propiedades teóricas de modelos se comportan menos 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 de predicados 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 . A veces, los tipos simples también pretenden excluir los tipos polimórficos y dependientes . [1]
La lógica de primer orden cuantifica sólo variables que abarcan individuos; 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 de conjuntos que están anidados de manera arbitrariamente profunda.
Hay dos semánticas posibles para la lógica de orden superior.
En la semántica estándar o completa , los cuantificadores de objetos de tipo superior abarcan todos los objetos posibles de ese tipo. Por ejemplo, un cuantificador sobre conjuntos de individuos abarca todo el conjunto de poderes del conjunto de individuos. Así, en semántica estándar, una vez especificado 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, según Kurt Gödel , HOL con semántica estándar no admite un cálculo de prueba eficaz , sólido y completo . [2] Las propiedades teóricas 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 mensurable , 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 de conjuntos de individuos pueden abarcar sólo un subconjunto del conjunto de poderes del conjunto de individuos. HOL con esta semántica es equivalente a la lógica de primer orden de muchos tipos , 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 teóricas de modelos de la lógica de primer orden y tiene un sistema de prueba completo, sólido y eficaz heredado de la lógica de primer orden.
La lógica de orden superior incluye las ramificaciones de la teoría simple de tipos de Church [4] y las diversas formas de teoría de tipos intuicionista . Gérard Huet ha demostrado que la unificabilidad es indecidible en una versión de teoría de tipos de la lógica de tercer orden, [5] [6] [7] [8] es decir, no puede haber ningún algoritmo para decidir si una ecuación arbitraria entre lógica de segundo orden (y mucho menos términos arbitrarios de orden superior) tiene una solución.
Hasta cierta noción de isomorfismo , la operación del conjunto de potencias 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 equisatisfactible para ella en la lógica de segundo orden. [9]
En algún contexto 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 ese contexto. [10]
El argumento de Gödel es modal y al menos de segundo orden, ya que en su definición de Dios hay una cuantificación explícita de las propiedades. [...] [AG96] demostró que se podía considerar una parte del argumento no como de segundo orden, sino como de tercer orden.