Una clase de sistemas lógicos que extiende la cuantificación a predicados, funciones y entidades de tipo superior (funciones de funciones, predicados de predicados, etc.), permitiendo razonar sobre objetos de tipo superior y posibilitando la formalización directa de conceptos matemáticos y semánticos no fácilmente expresables en lógicas de orden inferior.

Principio

La lógica de orden superior organiza los objetos en una jerarquía tipada y permite cuantificación en tipos arbitrariamente altos; la semántica puede darse en dominios de tipos superiores plenos o mediante semántica general al estilo Henkin, y la elección determina las propiedades proof-teóricas y modelo-teóricas.

Demostración

En un entorno de orden superior se puede cuantificar sobre conjuntos de conjuntos o sobre funcionales: por ejemplo, formalizar la semántica de un lenguaje de programación tipado suele requerir cuantificar sobre predicados sobre funciones, lo que la lógica de orden superior expresa directa y limpiamente en la disciplina de tipos.

Aplicación incorrecta

Asumir completitud, decidibilidad o axiomatizabilidad efectiva para la lógica de orden superior plena como si fuera de primer orden es incorrecto; los axiomas de comprensión no restringidos conducen a inconsistencia a menos que se restrinjan cuidadosamente o se formulen dentro de un marco teórico de tipos consistente.

Consecuencia

Los marcos de orden superior ofrecen gran comodidad expresiva, permitiendo la formalización directa de matemáticas, semántica de lenguajes y construcciones categóricas o de teoría de conjuntos, pero típicamente renuncian a garantías metalógicas deseables y aumentan la complejidad de la interpretación semántica.

Inversión

Restringir la lógica de orden superior a fragmentos, a un nivel finito de tipos o a semántica Henkin recupera muchas ventajas proof-teóricas de la lógica de primer orden; por el contrario, insistir en semántica plena de tipos superiores maximiza la expresividad a costa de fragilidad metalógica.

Límite

La lógica de orden superior presupone una disciplina de tipos y puede excluir construcciones no tipadas o impredicativas salvo que se permitan explícitamente; sus meta-propiedades y axiomas admisibles dependen de si se utiliza semántica plena, semántica Henkin o una fundamentación constructiva/teórico-de-tipos.

Tensión semántica

Existe tensión entre el deseo de un lenguaje rico que internalice la práctica matemática (favoreciendo semántica plena expresiva) y la demanda de control sintáctico y resultados meta-teóricos (favoreciendo fragmentos restringidos o enfoques estilo Henkin).

Síntesis

La Lógica De Orden Superior es una extensión tipada de la sintaxis lógica que lleva la cuantificación y el razonamiento a predicados y entidades de tipo superior, ofreciendo medios potentes para expresar matemáticas y semántica mientras obliga a decisiones explícitas sobre tipos y semántica que determinan si se prioriza expresividad o comportamiento meta-teórico deseable.