| Autor(es) | L. E. J. Brouwer (1881–1966); Andréi N. Kolmogórov (1903–1987); Arend Heyting (1898–1980) |
| Fecha / periodo | 1907–1932 · Siglo XX · Europa (Países Bajos, URSS) |
| Tipo | Formal |
| Deriva de | Lógica trascendental (n.º 52) · Lógica fenomenológica |
| Derivan de ella | Lógica modal · Formalismo y programa de Hilbert · Lógica de Gödel–Dummett · Sintaxis lógica y principio de tolerancia · Deducción natural y cálculo de secuentes · Lógica minimal · Lógicas paraconsistentes · Lógica constructiva con negación fuerte · Lógica dialógica y semántica de juegos · Lógica categórica y de topos · Teoría de tipos de Martin-Löf y correspondencia Curry–Howard · Lógica de la demostrabilidad · Lógica lineal · Lógica de la justificación |
| Tres leyes | Identidad: ✓ (\(A \to A\) es teorema) · No contradicción: ✓ (\(\neg(A \land \neg A)\) es teorema) · Tercio excluso: ✗ (\(A \lor \neg A\) no es teorema, aunque sí lo es \(\neg\neg(A \lor \neg A)\)) |
Para Brouwer la matemática es una actividad mental de construcción, fundada en la intuición del paso del tiempo, y el lenguaje y la lógica son solo registros posteriores de esa actividad. De ahí se sigue que afirmar un enunciado es afirmar que se dispone de una construcción que lo prueba. En «De onbetrouwbaarheid der logische principes» («La falta de fiabilidad de los principios lógicos», 1908) sostuvo que el tercio excluso se había abstraído de colecciones finitas, donde puede comprobarse caso a caso, y se había extendido sin justificación a las infinitas. La lógica intuicionista es la codificación de las inferencias que siguen siendo válidas bajo esa lectura constructiva. Su gesto distintivo es cambiar el significado de las conectivas, no su número: la verdad deja de ser correspondencia bivalente y pasa a ser demostrabilidad.
Interpretación BHK (Brouwer, Heyting, Kolmogórov). Heyting (1930–1934) y Kolmogórov (1932, como cálculo de problemas) fijaron el significado de las conectivas por lo que cuenta como prueba:
Cálculo de Heyting (1930). Una axiomatización estándar con modus ponens como regla:
Para los cuantificadores: \(\forall x\, A(x) \to A(t)\) y \(A(t) \to \exists x\, A(x)\), con las reglas de generalización: de \(B \to A(x)\) se infiere \(B \to \forall x\, A(x)\), y de \(A(x) \to B\) se infiere \(\exists x\, A(x) \to B\), si \(x\) no está libre en \(B\). Añadiendo \(A \lor \neg A\) o \(\neg\neg A \to A\) se obtiene la lógica clásica.
Qué se pierde y qué se conserva. Dejan de ser teoremas \(A \lor \neg A\), \(\neg\neg A \to A\), la ley de Peirce \(((A \to B) \to A) \to A\), \(\neg(A \land B) \to \neg A \lor \neg B\), \((A \to B) \lor (B \to A)\) y \(\neg\forall x\, \neg A(x) \to \exists x\, A(x)\). Siguen valiendo \(A \to \neg\neg A\), \(\neg\neg\neg A \to \neg A\), \(\neg(A \lor B) \leftrightarrow \neg A \land \neg B\) y \(\neg\neg(A \lor \neg A)\). La reducción al absurdo solo prueba negaciones: de que \(A\) lleve a contradicción se sigue \(\neg A\), pero de que \(\neg A\) lleve a contradicción no se sigue \(A\). A cambio se ganan la propiedad disyuntiva (si \(\vdash A \lor B\), entonces \(\vdash A\) o \(\vdash B\); Gentzen, 1935) y la existencial (si \(\vdash \exists x\, A(x)\), hay un término \(t\) con \(\vdash A(t)\)).
Relaciones con la lógica clásica. Glivenko (1929) probó que una fórmula proposicional \(A\) es teorema clásico si y solo si \(\neg\neg A\) es teorema intuicionista. Kolmogórov (1925), Gödel y Gentzen (1933) dieron traducciones negativas que incrustan la lógica y la aritmética clásicas en las intuicionistas. En este sentido la lógica intuicionista distingue más, no menos, que la clásica.
Semánticas. Gödel (1932) probó que ninguna matriz finita caracteriza la lógica intuicionista proposicional; Jaśkowski (1936) dio una matriz infinita. Stone y Tarski (1937–1938) la interpretaron en los abiertos de un espacio topológico, con \(\neg A\) como el interior del complemento. Beth (1956) y Kripke (1965) dieron semánticas de modelos arbóreos. En la de Kripke un modelo es un conjunto parcialmente ordenado de estados de información, con valoraciones que se conservan hacia arriba:
Ejemplo: con dos estados \(w \leq v\) y \(p\) verdadero solo en \(v\), el estado \(w\) no fuerza \(p\). Tampoco fuerza \(\neg p\), porque \(v\) fuerza \(p\). Así \(w\) no fuerza \(p \lor \neg p\).
Metateoría. El cálculo proposicional es correcto y completo respecto de las semánticas de Kripke y topológica, y es decidible (PSPACE-completo, Statman 1979). El de predicados es completo respecto de la semántica de Kripke e indecidible.
Brouwer toma de Kant la aprioridad de la intuición del tiempo, pero rechaza la del espacio, que la geometría no euclídea habría desacreditado. De esa intuición pura del tiempo, la «bi-unidad», deriva los números naturales y el continuo. Heyting (1931) expuso la lógica intuicionista en términos husserlianos: una proposición expresa una intención y su prueba es el cumplimiento de esa intención.
Es la lógica no clásica con descendencia más numerosa. Gödel (1933) la tradujo a la lógica modal y aisló así S4, lo que introdujo además la lectura de □ como demostrabilidad. El programa de Hilbert nació en parte como respuesta a Brouwer y a Weyl, y el principio de tolerancia de Carnap quiso disolver su disputa con la matemática clásica. Gentzen formalizó el cálculo de Heyting en NJ y LJ. Johansson (1937) suprimió el ex falso para obtener la lógica minimal; Gödel y Dummett la extendieron con \((A \to B) \lor (B \to A)\); Nelson (1949) le añadió una negación fuerte; da Costa partió de su fragmento positivo para su sistema paraconsistente Cω. Lorenzen buscó justificarla con juegos de diálogo. La lógica interna de un topos es intuicionista. Martin-Löf y la correspondencia Curry–Howard hacen explícita la interpretación BHK, y la lógica de la justificación le da una semántica de pruebas. La lógica lineal surge de descomponer la implicación intuicionista en la semántica del Sistema F.
La disputa entre Brouwer y Hilbert en los años veinte, la Grundlagenstreit, fue la mayor controversia sobre los fundamentos de la matemática del siglo. Terminó con la exclusión de Brouwer del consejo de los Mathematische Annalen (1928). Pero la lógica intuicionista sobrevivió a su derrota institucional y se convirtió en la lógica de la computación constructiva. Para la pregunta «¿una lógica o muchas?», es el caso central. Fue la primera rival de la lógica clásica con una motivación filosófica explícita, no solo técnica. Además, plantea el problema en su forma más aguda. Si el intuicionista y el clásico discrepan sobre \(A \lor \neg A\), ¿discrepan sobre la misma ley o sus conectivas significan cosas distintas? La pregunta de Quine sobre el «cambio de significado» y la defensa de Dummett del intuicionismo como teoría del significado parten de aquí.