| Autor(es) | Ingebrigt Johansson (1904–1987); Andréi N. Kolmogórov (1903–1987) |
| Fecha / periodo | 1925–1937 · Siglo XX · Europa (Noruega, URSS) |
| Tipo | Formal |
| Deriva de | Lógica intuicionista |
| Derivan de ella | — |
| Tres leyes | Identidad: ✓ (\(A \to A\) es teorema) · No contradicción: ✓ (\(\neg(A \land \neg A)\) es teorema, aunque de \(A \land \neg A\) no se sigue cualquier cosa) · Tercio excluso: ✗ (\(A \lor \neg A\) no es teorema; sí lo es \(\neg\neg(A \lor \neg A)\)) |
La lógica intuicionista de Heyting conserva un principio que la interpretación constructiva justifica mal: de una contradicción se sigue cualquier proposición (ex falso quodlibet). Si demostrar una implicación es dar un método que transforme pruebas del antecedente en pruebas del consecuente, ¿qué método transforma una prueba de lo absurdo en una prueba de cualquier enunciado? Kolmogórov en 1925 y Johansson en 1937 dieron la respuesta más económica: suprimir ese principio. El gesto distintivo es tratar la negación como una implicación más, \(\neg A := A \to \bot\), sin atribuir al absurdo \(\bot\) ninguna propiedad especial. El resultado es la lógica más débil que conserva la lectura constructiva de todas las conectivas.
Kolmogórov («O principe tertium non datur», Matematicheskii Sbornik 32, 1925). Formaliza un fragmento con implicación y negación, el sistema B, con los axiomas
y modus ponens. Omite deliberadamente \(\neg A \to (A \to B)\). En el mismo artículo muestra que la matemática clásica puede traducirse a este sistema anteponiendo una doble negación a cada subfórmula: la primera traducción negativa.
Johansson («Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus», Compositio Mathematica 4, 1937). Parte de los axiomas de Heyting (1930) y suprime el axioma \(\neg A \to (A \to B)\). En formulación actual:
En deducción natural, es NJ sin la regla \(\bot\)E.
Qué se conserva. Son teoremas, entre otros:
Qué se pierde.
Ejemplo. De \(A\) y \(\neg A\) se obtiene \(\bot\) por modus ponens. De \(\bot\) y la suposición \(B\) se sigue \(\bot\); luego \(B \to \bot\), es decir, \(\neg B\). Pero no hay regla que lleve de \(\bot\) a \(B\) misma.
Semántica. Modelos de Kripke intuicionistas en que \(\bot\) se trata como una variable más: puede ser forzada en algunos mundos, siempre de forma persistente. En esos mundos «anormales» todas las negaciones son verdaderas, pero no todas las fórmulas. La lógica es decidible en su parte proposicional y tiene la propiedad de la disyunción.
La lógica minimal es una restricción del cálculo de Heyting (1930), obtenida al suprimir el ex falso. Johansson llegó a ella en su correspondencia con Heyting de 1935–1936, en la que discutía precisamente la justificación de ese axioma. Kolmogórov había llegado antes, y por su cuenta, a formalizar el fragmento de implicación y negación, dentro de un análisis crítico del tercio excluso que coincidía en lo esencial con Brouwer.
No se registran descendientes directos en el catálogo. Como afinidad, su debilitamiento de la explosión la acerca a las lógicas paraconsistentes, entre las que a veces se la clasifica. Es una clasificación posterior, no una transmisión: ni Kolmogórov ni Johansson pretendían tolerar contradicciones, sino ajustar la lógica a la interpretación constructiva.
La lógica minimal fue durante décadas una curiosidad técnica. Recobró interés por la teoría de la prueba, donde las traducciones negativas y el «truco de Friedman» (1978) la usan para extraer contenido constructivo de pruebas clásicas, y por el estudio de las negaciones constructivas y la paraconsistencia. Para la pregunta «¿una lógica o muchas?», muestra que dentro de una misma filosofía, la constructiva, hay desacuerdo sobre qué principios valen. El intuicionismo no fija una sola lógica: la clase de lógicas que admiten lectura constructiva tiene al menos dos miembros naturales, y la elección entre ellos depende de cómo se entienda el absurdo.