Hispanopedia Wiki
Articulo de referencia

Lógica de orden superior

En matemáticas y lógica , la lógica de orden superior (abreviada HOL ) es una forma de lógica que se distingue de la lógica de primer orden por la adición de cuantificadores y, ...

Hispanopedia WikiContenido en espanolLectura gratuita

En matemáticas y lógica , la lógica de orden superior (abreviada HOL ) es una forma de lógica que se distingue de la lógica de primer orden por la adición de cuantificadores y, en ocasiones, por una semántica más rigurosa . Las lógicas de orden superior, con su semántica estándar, son más expresivas, pero sus propiedades de teoría de modelos son menos consistentes que las de la lógica de primer orden.

El término «lógica de orden superior» se usa comúnmente para referirse a la 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 la propusieron como una simplificación de la teoría ramificada de tipos especificada en los Principia Mathematica de Alfred North Whitehead y Bertrand Russell . A veces, el término «tipos simples» también excluye los tipos polimórficos y dependientes . [ 1 ]

Alcance de cuantificación

La lógica de primer orden cuantifica solo las variables que varían entre individuos; la lógica de segundo orden 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, tercer, ..., n- ésimo orden; es decir, la lógica de orden superior admite la cuantificación sobre conjuntos que están anidados a una profundidad arbitraria.

Semántica

Existen 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 potencia del conjunto de individuos. Por lo tanto, en la 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, 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, en cambio, es ℵ 0 , el cardinal infinito más pequeño.

En la semántica de Henkin , cada interpretación incluye un dominio independiente para cada tipo de orden superior. Así, por ejemplo, los cuantificadores sobre conjuntos de individuos pueden abarcar solo un subconjunto del conjunto potencia de dichos individuos. La lógica de orden superior (HOL) con esta semántica es equivalente a la lógica de primer orden multisortada , en lugar de ser más fuerte que esta. En particular, la HOL con semántica de Henkin posee todas las propiedades de teoría de modelos de la lógica de primer orden y cuenta con un sistema de demostración completo, sólido y eficaz heredado de ella.

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 la teoría de tipos intuicionista . Gérard Huet ha demostrado que la unificabilidad es indecidible en una variante de lógica de tercer orden basada en la teoría de tipos , [ 5 ] [ 6 ] [ 7 ] [ 8 ] es decir, no puede haber un algoritmo para decidir si una ecuación arbitraria entre términos de segundo orden (y mucho menos términos arbitrarios de orden superior) tiene solución.

Hasta cierto punto de isomorfismo , la operación de conjunto potencia es definible en lógica de segundo orden. Basándose en 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 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 demostración ontológica de Gödel se estudia mejor (desde una perspectiva técnica) en este contexto. [ 10 ]

Véase también

Notas

  1. ↑ Jacobs, 1999, capítulo 5
  2. ↑ Shapiro 1991, pág. 87.
  3. ↑ Menachem Magidor y Jouko Väänänen . " Sobre los números de Löwenheim-Skolem-Tarski para extensiones de la lógica de primer orden ", Informe nº 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". Information and Control . 22 (3): 257– 267. doi : 10.1016/s0019-9958(73)90301-x .
  6. ^ Huet, Gérard (septiembre de 1976). Resolución de ecuaciones en los idiomas de orden 1,2,... ω (Ph.D.) (en francés). Universidad de París VII.
  7. ↑ Warren D. Goldfarb (1981). "La indecidibilidad del problema de unificación de segundo orden" (PDF) . Theoretical Computer Science . 13 (2): 225– 230. doi : 10.1016/0304-3975(81)90040-2 .
  8. ↑ Huet, Gérard (2002). "Unificación de orden superior 30 años después" (PDF) . En Carreño, V.; Muñoz, C.; Tahar, S. (eds.). Actas de la XV Conferencia Internacional TPHOL . LNCS. Vol. 2410. Springer. pp. 3–12 .  
  9. ↑ entrada en HOL
  10. ↑ Fitting, Melvin (2002). Tipos, cuadros y el Dios de Gödel . Springer Science & Business Media. pág. 139. ISBN  978-1-4020-0604-3El 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] demostró que una parte del argumento podría considerarse no de segundo orden, sino de tercer orden.

Referencias

  • Andrews, Peter B. (2002). Introducción a la lógica matemática y la teoría de tipos: Hacia la verdad a través de la demostración , 2.ª ed., Kluwer Academic Publishers, ISBN 1-4020-0763-9
  • Stewart Shapiro , 1991, «Fundamentos sin fundacionalismo: Un argumento a favor de la lógica de segundo orden». Oxford University Press., 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, P.J., 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 en lógica y fundamentos de las matemáticas 141. North Holland, 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.