Deducción natural: definición, reglas e historia de la lógica matemática

Deducción natural: guía esencial — definición, reglas e historia de la lógica matemática; de Łukasiewicz y Jaśkowski a sus aplicaciones modernas.

La deducción natural es una rama de la lógica matemática desarrollada en Polonia en los años veinte y treinta. Su objetivo es expresar reglas de inferencia estrechamente relacionadas con la forma "natural" de razonar.

Estimulado por una serie de seminarios celebrados en Polonia en 1926 por Łukasiewicz que abogaban por un tratamiento más natural de la lógica, Jaśkowski realizó los primeros intentos de definir una deducción más natural. En 1929 sugirió por primera vez el uso de una notación diagramática, y posteriormente actualizó su propuesta en documentos de 1934 y 1935.

Definición e idea central

La deducción natural es un sistema formal para representar razonamientos mediante reglas que reflejan directamente cómo las personas introducen y usan conectivos lógicos en argumentos. Su principio fundamental es que cada conectivo tiene reglas de introducción (cómo obtener una fórmula con ese conectivo) y de eliminación (cómo explotar una fórmula que contiene ese conectivo).

En una presentación de deducción natural las pruebas se construyen a partir de suposiciones locales (hipótesis abiertas) y reglas que permiten:

• formular subpruebas o cajas donde se hacen suposiciones provisionales;
• disponer y descargar esas hipótesis cuando la regla lo permita (por ejemplo, para demostrar una implicación);
• obtener conclusiones finales en las que no quedan hipótesis abiertas no justificadas.

Reglas típicas (esquema)

A continuación se enumeran, en términos intuitivos, las reglas más comunes de la deducción natural. Las abreviaturas entre paréntesis indican la regla típica usada en la literatura:

• Implicación (→)
  • Introducción (→I): para demostrar A → B, asume A provisionalmente y, si puedes derivar B, descarga la suposición y concluye A → B.
  • Eliminación (→E): a partir de A y A → B se obtiene B (este paso corresponde a la regla de modus ponens).
• Conjunción (∧)
  • Introducción (∧I): si obtienes A y obtienes B, puedes concluir A ∧ B.
  • Eliminación (∧E): de A ∧ B puedes obtener A (o B) por separado.
• Disyunción (∨)
  • Introducción (∨I): de A puedes inferir A ∨ B (y simétricamente de B inferir A ∨ B).
  • Eliminación (∨E): si de A puedes inferir C y de B puedes inferir C, entonces de A ∨ B puedes inferir C (requiere razonamiento por casos con subpruebas).
• Negación y contradicción (¬, ⊥)
  • Negación como atajo: ¬A se puede tratar como A → ⊥, donde ⊥ denota contradicción.
  • Prueba por contradicción: si suponiendo A llegas a ⊥, puedes inferir ¬A.
• Cuantificadores (∀, ∃)
  • Introducción universal (∀I): para inferir ∀x P(x) la variable x no debe depender de hipótesis abiertas; suele requerirse una condición de variable eigen (x no libre en hipótesis abiertas).
  • Eliminación universal (∀E): de ∀x P(x) puedes inferir P(t) para cualquier término t apropiado.
  • Introducción existencial (∃I): de P(t) concluyes ∃x P(x).
  • Eliminación existencial (∃E): para usar ∃x P(x) asumes P(c) con una constante nueva c (no usada en otros supuestos) y, si puedes derivar C sin depender de c, entonces inferes C.

Presentaciones formales: Jaśkowski y Gentzen

Existen varias presentaciones equivalentes de la deducción natural. Dos de las más influyentes son:

• Notación de Jaśkowski: usa cajas o subpruebas delimitadas para indicar hipótesis provisionales y su descarga; es muy adecuada para la presentación lineal y pedagógica de pruebas.
• Presentación de Gentzen: introdujo una versión en forma de árbol y, más ampliamente, el cálculo de secuentes (sequent calculus). Gentzen formuló también resultados meta-teóricos fundamentales (como el teorema de eliminación del corte para secuentes) que están relacionados con la normalización en deducción natural.

Resultados meta-teóricos importantes

• Normalización: teoremas de normalización (p. ej. desarrollados por Dag Prawitz y otros) muestran que las pruebas en deducción natural pueden transformarse en formas normales sin "detours" redundantes. Esto es esencial para la semántica de las pruebas y para la teoría de la demostración.
• Consistencia y eliminación de cortes: la eliminación de cortes en el cálculo de secuentes de Gentzen y la normalización en deducción natural proporcionan herramientas para estudiar la consistencia y la estructura de las pruebas.
• Curry–Howard: la correspondencia Curry–Howard establece una doble interpretación entre pruebas en deducción natural (especialmente intuicionista) y programas en cálculo lambda, lo que vincula la lógica con la teoría de tipos y la informática teórica.

Ejemplo sencillo (intuitivo)

Demostrar B a partir de A y A → B:

• 1. A (hipótesis)
• 2. A → B (hipótesis)
• 3. B por (→E) de 1 y 2.

Demostrar A → B suponiendo A y obteniendo B más tarde corresponde a construir una subprueba donde A es hipótesis abierta y, al llegar a B, se aplica (→I) para descargar A y concluir A → B.

Aplicaciones y relevancia

La deducción natural es central en:

• enseñanza de la lógica formal, por su afinidad con el razonamiento informal;
• fundamentos de la matemática y teoría de la demostración;
• lenguajes de programación y verificación (a través de la correspondencia Curry–Howard y sistemas de tipos dependientes);
• herramientas de demostración automática e interactiva (donde las reglas de introducción y eliminación guían la construcción de pruebas asistidas).

Breve historia y evolución

La idea de modelar la inferencia de forma "natural" tomó fuerza en la década de 1920. Como se señaló, las charlas de Łukasiewicz en 1926 impulsaron a investigadores como Jan Łukasiewicz y posteriormente a Stanisław Jaśkowski a buscar notaciones y reglas que reflejasen el razonamiento humano. Jaśkowski propuso en 1929 una notación diagramática y refinó sus ideas en trabajos de principios de los años treinta. De manera independiente, Gerhard Gentzen desarrolló en los años 1934–1935 formulaciones de deducción natural y del cálculo de secuentes, aportando herramientas para el análisis meta-teórico de la lógica. En décadas posteriores, trabajos de Prawitz, Curry, Howard y otros ampliaron y conectaron la deducción natural con la semántica de pruebas y la informática teórica.

Conclusión

La deducción natural ofrece un marco formal que captura de manera directa la estructura del razonamiento lógico cotidiano mediante reglas de introducción y eliminación. Sus múltiples presentaciones (Jaśkowski, Gentzen, formalisaciones modernas) y sus conexiones con resultados meta-teóricos y con la informática teórica la convierten en una pieza fundamental de la lógica matemática moderna.

Búsqueda por letra