| Autor(es) | Alonzo Church (1903–1995); Leon Chwistek (1884–1944); Frank P. Ramsey (1903–1930) |
| Fecha / periodo | 1921–1940 · Siglo XX · Estados Unidos y Europa |
| Tipo | Formal |
| Deriva de | Begriffsschrift y logicismo · Teoría de tipos de Principia Mathematica · Lógica del Tractatus · Cálculo lambda |
| Derivan de ella | Lógica categórica y de topos · Teoría de tipos de Martin-Löf y correspondencia Curry–Howard · Semántica de Montague · Lógica plural |
| Tres leyes | Identidad: ✓ (definible a lo Leibniz: \(a = b\) si \(\forall F(Fa \to Fb)\)) · No contradicción: ✓ (clásica) · Tercio excluso: ✓ (clásico; el tipo de los valores de verdad tiene exactamente dos elementos) |
La lógica de orden superior cuantifica no solo sobre individuos, sino sobre propiedades, relaciones, funciones y funciones de funciones. Permite formular en el lenguaje lógico nociones como «toda propiedad hereditaria», la inducción matemática o la identidad por indiscernibilidad. El problema que resuelve la teoría simple de tipos es cómo tener ese poder expresivo sin paradojas. La respuesta es clasificar todas las expresiones en tipos y prohibir que una función se aplique a sí misma. El gesto distintivo de Church (1940) es hacer de la abstracción λ el único mecanismo de ligadura de variables: cuantificadores, clases y descripciones se obtienen aplicando constantes a abstracciones.
Tipos (Church, «A Formulation of the Simple Theory of Types», 1940):
Un predicado de individuos tiene tipo \((o\iota)\); una propiedad de tales predicados, tipo \((o(o\iota))\). La expresión \(x\,x\) no está bien formada, porque el argumento tendría que tener a la vez un tipo y el tipo de las funciones sobre él. Así se bloquean la paradoja de Russell y sus variantes.
Términos. Variables y constantes de cada tipo; aplicación \(F\,A\) (si \(F\) es de tipo \((\alpha\beta)\) y \(A\) de tipo \(\beta\), el resultado es de tipo \(\alpha\)); abstracción \(\lambda x_\beta . A_\alpha\), de tipo \((\alpha\beta)\). Las fórmulas son los términos de tipo \(o\).
Constantes lógicas. Church toma \(\neg\), \(\lor\), un cuantificador \(\Pi\) para cada tipo y un operador de descripción o selección \(\iota\) para cada tipo. El cuantificador se define por abstracción: \(\forall x\, A\) abrevia \(\Pi(\lambda x . A)\), es decir, «la propiedad \(\lambda x . A\) es universal».
Axiomas (en sustancia):
Reglas. Cambio de variables ligadas (conversión α), conversión β en ambos sentidos, \((\lambda x . A)\,B\) por \(A[B/x]\), sustitución, modus ponens y generalización.
Comprensión. No hace falta como axioma aparte: para cualquier fórmula \(A\), el término \(\lambda x . A\) existe, y por conversión β se obtiene \(\exists F \forall x (F\,x \leftrightarrow A)\).
Semántica estándar. El dominio de \((\alpha\beta)\) es el conjunto de todas las funciones de \(D_\beta\) en \(D_\alpha\). Con ella la lógica es muy expresiva: la aritmética de Peano de segundo orden es categórica (Dedekind), y la finitud y la numerabilidad son definibles. El precio es alto:
Modelos generales (Henkin, «Completeness in the Theory of Types», 1950). Si se permite que \(D_{(\alpha\beta)}\) contenga solo algunas funciones, con tal de que sea cerrado bajo lo que los términos definen, el cálculo de Church es completo. En esa semántica vuelven la compacidad y Löwenheim–Skolem: la lógica de orden superior así interpretada se comporta como una teoría de primer orden con varios géneros.
Desarrollos. Andrews (sistema \(Q_0\), 1963) mostró que basta la igualdad en cada tipo como única constante lógica. Los demostradores HOL, Isabelle/HOL y PVS implementan variantes de la teoría de Church.
Qué se gana y qué se pierde. Se gana expresividad: la identidad es definible, y lo son también la inducción y el cierre transitivo. Se pierde la axiomatizabilidad completa de la semántica estándar. Quine lo resumió con dureza: la lógica de segundo orden sería «teoría de conjuntos disfrazada».
La lógica de orden superior nace en la Begriffsschrift (1879): Frege cuantifica sobre funciones y define la herencia en una serie con un cuantificador sobre propiedades. De él toma Church la jerarquía de niveles funcionales, y de Principia Mathematica la idea de tipos. Chwistek (1921) y Ramsey (1926) mostraron que la ramificación de los tipos de Russell y el axioma de reducibilidad solo hacían falta para las paradojas semánticas («el mentiroso»), no para las lógicas («Russell»). Ramsey justificó el abandono de la ramificación con la noción de tautología del Tractatus: las funciones proposicionales pueden entenderse extensionalmente. Hilbert y Ackermann (1928) llamaron «cálculo funcional ampliado» a esta lógica y la hicieron objeto de estudio metamatemático. Church, por último, la unió a su cálculo λ, del que tomó la abstracción como principio único de ligadura.
La descendencia es amplia. Lambek y Scott relacionaron la teoría de tipos de orden superior con los topos. Martin-Löf reelaboró en clave constructiva el cálculo λ tipado de Church. Montague construyó su lógica intensional ampliando los tipos de Church con índices de mundos y tiempos. La lógica plural, en fin, reinterpreta la lógica monádica de segundo orden como cuantificación plural sobre individuos, para evitar el compromiso con conjuntos.
En los años treinta la lógica de orden superior era la lógica de referencia (Gödel y Tarski trabajan en ella). Tras la guerra perdió la primacía ante la lógica de primer orden, más dócil metateóricamente, por el peso de los teoremas de completitud y compacidad y por la crítica de Quine. Revivió en informática, en la semántica formal del lenguaje natural y en la filosofía de las matemáticas. Para la pregunta «¿una lógica o muchas?», el caso es central: la frontera entre lógica y matemática depende de la semántica que se adopte. Con modelos estándar la lógica de segundo orden fija las estructuras matemáticas, pero no admite un cálculo completo; con modelos generales admite un cálculo completo, pero pierde ese poder. No hay una respuesta neutral sobre cuál es «la» lógica.