Lógica de orden superior - Higher-order logic

En matemáticas y lógica , una lógica de orden superior es una forma de lógica de predicados 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 teóricas de modelos se comportan menos bien que las de la lógica de primer orden.

El término "lógica de orden superior", abreviado como HOL , se utiliza comúnmente para referirse a la lógica de predicado simple de orden superior . Aquí "simple" indica que el subyacente tipo teoría es la teoría de los tipos simples , también llamada la teoría simple de tipos (véase la teoría de Tipo ). 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 por Alfred North Whitehead y Bertrand Russell . Hoy en día, los tipos simples a veces también están destinados a excluir los tipos polimórficos y dependientes .

Alcance de cuantificación

La lógica de primer orden cuantifica solo las variables que se distribuyen entre los individuos; la lógica de segundo orden , además, también cuantifica sobreconjuntos; La lógica de tercer orden también cuantifica sobre conjuntos de conjuntos, etc.

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 forma arbitraria y profunda.

Semántica

Hay dos posibles semánticas 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 de potencias del conjunto de individuos. Así, en 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, según un resultado de Kurt Gödel , HOL con semántica estándar no admite un cálculo de prueba efectivo , sólido y completo . 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 lógica de segundo orden ya es mayor que el primer cardinal medible , si tal cardinal existe. En contraste, el número de Löwenheim de la lógica de primer orden 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 de potencias del conjunto de individuos. HOL con esta semántica es equivalente a la lógica de primer orden de muchos 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 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.

Ejemplos y propiedades

Las lógicas de orden superior incluyen las ramificaciones de la teoría de tipos simple de Church y las diversas formas de teoría de tipos intuicionista . Gérard Huet ha demostrado que la unificabilidad es indecidible en un tipo de teoría de tipos de lógica de tercer orden, es decir, no puede haber un algoritmo para decidir si una ecuación arbitraria entre términos de tercer orden (y mucho menos arbitrarios de orden superior) tiene una solución. .

Hasta una cierta noción de isomorfismo, la operación del conjunto de potencias se puede definir en lógica de segundo orden. Usando 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, uno puede encontrar una fórmula equisatisfactable para ella en lógica de segundo orden.

En algún contexto, se asume 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 tal contexto.

Ver también

• Lógica de primer orden
• Lógica de segundo orden
• Teoría de tipos
• Gramática de orden superior
• Programación lógica de orden superior
• HOL (asistente de pruebas)
• Lógica de muchos ordenamientos
• Cálculo lambda mecanografiado
• Lógica modal

Notas

Referencias

• Andrews, Peter B. (2002). Una introducción a la lógica matemática y la teoría de tipos: a la verdad a través de la prueba , 2da ed, Kluwer Academic Publishers, ISBN   1-4020-0763-9
• Stewart Shapiro , 1991, "Fundamentos sin fundacionalismo: un caso para la lógica de segundo orden". Prensa de la Universidad de Oxford., ISBN   0-19-825029-0
• Stewart Shapiro , 2001, "Lógica clásica II: Lógica de orden superior", en Lou Goble, ed., The Blackwell Guide to Philosophical Logic . Blackwell, ISBN   0-631-20693-0
• Lambek, J. y Scott, PJ, 1986. Introducción a la lógica categórica de orden superior , Cambridge University Press, ISBN   0-521-35653-9
• Jacobs, Bart (1999). Lógica categórica y teoría de tipos . Estudios de lógica y fundamentos de las matemáticas 141. Holanda del Norte, Elsevier. ISBN   0-444-50170-3 .
• Benzmüller, Christoph; Miller, Dale (2014). "Automatización de la lógica de orden superior". En Gabbay, Dov M .; Siekmann, Jörg H .; Woods, John (eds.). Manual de Historia de la Lógica, Volumen 9: Lógica Computacional . Elsevier. ISBN   978-0-08-093067-1 .

enlaces externos

• Andrews, Peter B, Teoría de tipos de Church en la Enciclopedia de Filosofía de Stanford .
• Miller, Dale, 1991, " Lógica: orden superior ", Enciclopedia de Inteligencia Artificial , 2ª ed.
• Herbert B. Enderton, Lógica de segundo orden y orden superior en la Enciclopedia de Filosofía de Stanford , publicado el 20 de diciembre de 2007; revisión sustantiva 4 de marzo de 2009.