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 nombre «lógica de orden superior» se usa comúnmente para designar una 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 «teoría ramificada de tipos» postulada en los Principia Mathematica de Alfred North Whitehead y Bertrand Russell. A veces también se pretenden excluir los tipos polimórfico y dependiente.^[1]​

Alcance de la cuantificación

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

Una lógica de orden superior es la unión de la lógica de primer, segundo, tercero... hasta un orden n; es decir, la lógica de orden superior admite la cuantificación sobre conjuntos que están anidados arbitraria y profundamente.

Semántica

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

En la «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 define el conjunto de individuos, 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 un efectivo, sólido y completo cálculo de prueba.^[2]​ Las propiedades de los modelos 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.^[3]​ El número de Löwenheim de lógica de primer orden, en contraste, es ${\displaystyle \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, con un sistema de demostración completo, sólido y efectivo heredado de la lógica de primer orden.

Propiedades

Las lógicas de orden superior incluyen las ramificaciones de la teoría simple de tipos de Church^[4]​ y las diversas formas de teoría intuicionista de tipos. Gérard Huet ha demostrado que la unificación es indecidible en una forma de lógica de tercer orden cual 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 arbitrarios de orden superior) tiene una solución.

Casi hasta un isomorfismo, la operación del conjunto de potencias es definible en lógica de segundo orden. Gracias a esto, 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 equisatisfacible para ella en lógica de segundo orden^[9]​

El nombre «lógica de orden superior» en algún contexto parecería referir sólo 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.^[10]​

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

Referencias

1. Jacobs, 1999, capítulo 5
2. Shapiro 1991, p. 87.
3. Menachem Magidor y Jouko Väänänen. "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic", Informe No. 15 (2009/2010) del Instituto Mittag-Leffler.
4. Alonzo Church, Una formulación de la teoría simple de tipos, The Journal of Symbolic Logic 5(2):56–68 (1940)
5. Huet, Gérard P. (1973). «La indecidibilidad de la unificación en la lógica de tercer orden». Información y control 22 (3): 257-267. doi:10.1016/s0019-9958(73)90301-x.  Parámetro desconocido |doi-access= ignorado (ayuda)
6. Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,... ω (Ph.D.) (en francés). Université de Paris VII. 
7. Warren D. Goldfarb (1981). «The Undecidability of the Second-Order Unification Problem». Informática Teórica 13: 225-230. 
8. Huet, Gérard (2002). «Unificación de orden superior 30 años después». En Carreño; Muñoz; Tahar, S., eds. Actas, 15ª Conferencia Internacional TPLOS. LNCS 2410. Springer. pp. 3-12. 
9. ><.Entrada SEP en LOS
10. Fitting, Melvin (2002). Types, Tableaus, and Gödel's God. Springer Science & Business Media. p. 139. ISBN 978-1-4020-0604-3. «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 sobre las propiedades. [...] [AG96] mostró que uno podía ver una parte del argumento no como de segundo orden, sino como de tercer orden.» 

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.