Lógica de orden superior

En matemáticas y lógica, una lógica de orden superior (abreviada LOS) es una forma de lógica de predicados que se distingue de la lógica de primer orden por cuantificadores adicionales y, a veces, por su semántica lógica. Las lógicas de orden superior con su semántica estándar son más expresivas, pero sus propiedades son menos adecuadas que las de la lógica de primer orden desde la perspectiva de la teoría de modelos.

El término "lógica de orden superior" se usa comúnmente para significar lógica de predicados simples 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 también se pretende excluir los tipos polimórfico y dependiente.​

Alcance de la cuantificación

La lógica de primer orden cuantifica solo variables que varían sobre individuos; lógica de segundo orden, además, también cuantifica sobre conjuntos; La lógica de tercer orden también cuantifica sobre conjuntos de conjuntos, y así sucesivamente.

La lógica de orden superior es la unión de la lógica de primer, segundo, tercero-, ..., de orden n); "Es decir", la lógica de orden superior admite la cuantificación sobre conjuntos que están anidados arbitrariamente profundamente.

Semántica

Hay dos semánticas posibles para la lógica de orden superior.

En el "estándar" o "semántica 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. Por lo tanto, en semántica estándar, una vez que se especifica el conjunto de individuos, esto es suficiente para especificar todos los cuantificadores. LOS con semántica estándar es más expresivo que la lógica de primer orden. Por ejemplo, las LOS admiten axiomatizaciones del teorema de categoricidad de Morley 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, LOS con semántica estándar no admite una efectiva, sonido, y completo cálculo de prueba.​ Las propiedades de la teoría del modelo de LOS 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.​ El número de Löwenheim de lógica de primer orden, en contraste, es $\aleph _{0}$, 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 variar solo sobre un subconjunto del conjunto de potencias del conjunto de individuos. LOS con esta semántica es equivalente a la lógica de primer orden de muchos órdenes, en lugar de ser más fuerte que la lógica de primer orden. En particular, LOS 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 efectivo heredado de la lógica de primer orden.

Propiedades

Las lógicas de orden superior incluyen las ramificaciones de Church's teoría simple de tipos​ y las diversas formas de teoría intuicionista de tipos. Gérard Huet ha demostrado que unifibilidad es indecidible en un sabor de lógica de tercer orden teoría de tipos,​​​​ es decir, no puede haber ningún algoritmo para decidir si una ecuación arbitraria entre términos de segundo 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 es definible 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 de equisatisfacible para ella en lógica de segundo orden​

El término "lógica de orden superior" se asume en algún contexto para referirse a la lógica de orden superior "clásica". Sin embargo, también se ha estudiado la lógica de orden superior modal. Según varios lógicos, La prueba ontológica de Gödel se estudia mejor (desde una perspectiva técnica) en tal contexto.​

Véase también

• Lógica de orden cero (lógica proposicional)
• 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
• Lógica modal

Bibliografía

• Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed, Kluwer Academic Publishers, ISBN 1-4020-0763-9
• Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press., ISBN 0-19-825029-0
• Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0-631-20693-0
• Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0-521-35653-9
• Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3. 
• Benzmüller, Christoph; Miller, Dale (2014). «Automation of Higher-Order Logic». En Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John, eds. Handbook of the History of Logic, Volume 9: Computational Logic. Elsevier. ISBN 978-0-08-093067-1. 

Enlaces externos

• Andrews, Peter B, Church's Type Theory in Stanford Encyclopedia of Philosophy.
• Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
• Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of Philosophy, published Dec 20, 2007; substantive revision Mar 4, 2009.