| Autor(es) | Gerhard Gentzen (1909–1945); Stanisław Jaśkowski (1906–1965); Dag Prawitz (n. 1936) |
| Fecha / periodo | 1934–1935 · Siglo XX · Alemania y Polonia |
| Tipo | Formal |
| Deriva de | Begriffsschrift y logicismo · Lógica intuicionista · Lógica de primer orden clásica · Formalismo y programa de Hilbert |
| Derivan de ella | Lógicas subestructurales y cálculo de Lambek · Lógica categórica y de topos · Teoría de tipos de Martin-Löf y correspondencia Curry–Howard · Lógica lineal |
| Tres leyes | Identidad: ✓ (secuente inicial \(A \vdash A\)) · No contradicción: ✓ (\(\neg(A \land \neg A)\) derivable en NJ, NK, LJ y LK) · Tercio excluso: matizado (✓ en NK y LK; ✗ en NJ y LJ, donde \(A \lor \neg A\) no es derivable) |
Los sistemas de Frege, Russell y Hilbert deducían a partir de muchos axiomas y una o dos reglas. Eran exactos, pero sus pruebas no se parecían al razonamiento matemático, que procede por suposiciones: «supongamos \(A\); entonces…; luego, si \(A\), entonces \(B\)». Gentzen y Jaśkowski invirtieron la proporción: casi sin axiomas, con muchas reglas, dos por cada conectiva, una para introducirla y otra para eliminarla. Gentzen añadió un segundo formalismo, el cálculo de secuentes, pensado para estudiar las pruebas como objetos. Su teorema principal, la eliminación del corte, muestra que toda prueba puede hacerse directa, sin rodeos. El gesto distintivo es hacer de la estructura de las pruebas, y no solo de sus conclusiones, el objeto de la lógica.
Deducción natural (Gentzen, Untersuchungen über das logische Schließen, 1934–1935; Jaśkowski, «On the rules of suppositions in formal logic», 1934). Reglas de NJ, en notación actual:
NK es NJ más el tercio excluso \(A \lor \neg A\) como axioma (o, en versiones posteriores, la reducción al absurdo clásica). Gentzen comenta que las introducciones son como definiciones de las conectivas, y que las eliminaciones solo explotan lo que la introducción establece.
Cálculo de secuentes. Un secuente \(\Gamma \vdash \Delta\) se lee: si todas las fórmulas de \(\Gamma\) son verdaderas, alguna de \(\Delta\) lo es. LK consta de:
LJ es LK con la restricción de que \(\Delta\) tenga a lo sumo una fórmula. Esa sola restricción separa la lógica intuicionista de la clásica: en LK, \(\vdash A, \neg A\) y luego \(\vdash A \lor \neg A\) se derivan con dos fórmulas a la derecha, algo que LJ prohíbe.
Hauptsatz. Toda prueba en LK o LJ puede transformarse en una prueba sin corte del mismo secuente. Consecuencias:
Normalización (Prawitz, Natural Deduction, 1965). Un «rodeo» es una introducción seguida inmediatamente de la eliminación de la misma conectiva. Prawitz mostró que toda derivación en NJ se reduce a una forma normal sin rodeos, y formuló el principio de inversión que subyace a la observación de Gentzen.
Ejemplo. Para probar \(A \to (B \to A)\): supongo \(A\); supongo \(B\); tengo \(A\); por \(\to\)I cancelo \(B\) y obtengo \(B \to A\); por \(\to\)I cancelo \(A\) y obtengo \(A \to (B \to A)\).
La deducción natural nace como reacción: Gentzen la presenta frente a los cálculos axiomáticos de Frege, Russell y Hilbert, que describe como alejados del razonamiento real. Jaśkowski respondía a una pregunta que Łukasiewicz planteó en su seminario de 1926 sobre cómo formalizar el método de las suposiciones. La lógica intuicionista es un punto de partida: NJ y LJ formalizan el cálculo de Heyting, y es la versión intuicionista la que Gentzen normaliza. El suelo común es la lógica de primer orden tal como la habían elaborado Hilbert y su escuela. Gentzen trabajó dentro del programa de Hilbert: el cálculo de secuentes es su instrumento, y la prueba de consistencia de la aritmética (1936) su fruto principal.
La descendencia es la teoría estructural de la prueba. Lambek formuló su cálculo como secuentes sin reglas estructurales y probó para él la eliminación del corte. Él mismo trató los sistemas de tipo Gentzen como categorías. Howard y Martin-Löf se basan en la deducción natural y la normalización de Prawitz para identificar pruebas con programas. La lógica lineal de Girard se formula a partir de LK suprimiendo debilitamiento y contracción. Como afinidades atribuidas: Corcoran (1972) y Smiley (1973) leen la silogística de Aristóteles como un sistema de deducción natural, y Bobzien (2019) compara el análisis estoico con la búsqueda hacia atrás de pruebas en cálculos de secuentes subestructurales.
Gentzen trabajó en Gotinga como asistente de Hilbert y murió en 1945 en una prisión de Praga. Sus sistemas pasaron a los manuales a través de Fitch, Suppes y Prawitz, y hoy son la forma estándar de enseñar lógica. Para la pregunta «¿una lógica o muchas?», su aportación es doble. Por una parte, muestra que la diferencia entre lógica clásica e intuicionista puede reducirse a una restricción estructural, el número de fórmulas a la derecha del secuente. Por otra, abre la vía de las lógicas subestructurales: quitando o limitando debilitamiento, contracción o intercambio se obtienen lógicas relevantes, lineales o de Lambek. El pluralismo aparece así como variación de las reglas estructurales sobre un fondo común de reglas lógicas, y la tesis de que las reglas de introducción fijan el significado de las conectivas alimenta la semántica inferencialista.