Una técnica de cálculo de pruebas que deriva conclusiones de premisas aplicando reglas de introducción y eliminación para cada conectivo lógico y cuantificador; las pruebas se estructuran como cadenas de aplicaciones de reglas en lugar de instanciar esquemas axiomáticos.

Principio

Cada conectivo lógico y cuantificador tiene reglas complementarias de introducción y eliminación que permiten pasos locales que preservan el significado desde suposiciones hasta conclusiones.

Demostración

Para demostrar A ∧ B, se aplica la introducción de la conjunción (∧-intro) derivando separadamente A y B; para usar A ∧ B en la prueba, se aplica la eliminación de la conjunción (∧-elim) para obtener el conjunt necesario.

Aplicación incorrecta

Tratar las reglas de introducción o eliminación como heurísticas opcionales y omitir la descarga de supuestos temporales (por ejemplo no descargar una suposición en →-intro) produce pruebas inválidas o no cerradas.

Consecuencia

Bien aplicada, la deducción natural genera pruebas que reflejan el significado inferencial de los conectivos, facilita la legibilidad y la correspondencia con el razonamiento informal y permite procedimientos de normalización.

Inversión

La inversión es un cálculo axiomático que deriva teoremas desde un conjunto fijo de esquemas axiomáticos y pocas reglas de inferencia; en lugar de reglas locales de intro/elim, construye cadenas globales desde axiomas.

Límite

Se aplica principalmente a lógicas proposicionales y de primer orden con reglas de intro/elim bien definidas; sus extensiones (modales, subestructurales) requieren reglas adaptadas y pueden romper propiedades de normalización.

Tensión semántica

Compite con los sistemas hilbertianos: la deducción natural enfatiza el significado local de las reglas y la estructura de la prueba, mientras que Hilbert prioriza conjuntos mínimos de reglas y concisión en la derivabilidad.

Síntesis

La deducción natural es un marco de prueba basado en reglas donde cada operador lógico tiene reglas emparejadas que permiten construir y descomponer fórmulas paso a paso, produciendo pruebas que encarnan el papel inferencial de los operadores.