Deducción Natural y Cálculo de Secuentes

La deducción natural y el cálculo de secuentes son los dos sistemas formales de estilo Gentzen que representan pruebas mediante reglas de introducción y eliminación para los conectivos lógicos, formando la maquinaria básica de la teoría estructural de la prueba.

Definition

La deducción natural deriva fórmulas a partir de suposiciones utilizando reglas de introducción y eliminación que reflejan el razonamiento informal, mientras que el cálculo de secuentes manipula secuentes, afirmaciones de que una lista de fórmulas implica otra, a través de reglas que actúan a la izquierda y a la derecha de una implicación.

Scope

Este tema cubre las reglas de la deducción natural con sus pares de introducción y eliminación, la estructura del cálculo de secuentes con sus reglas izquierdas y derechas y reglas estructurales, la normalización para la deducción natural, la relación entre los dos sistemas y sus variantes intuicionistas y clásicas.

Core questions

• ¿Cómo confieren significado las reglas de introducción y eliminación a los conectivos lógicos?
• ¿Qué es un secuente y cómo difieren sus reglas de las de la deducción natural?
• ¿Cómo simplifica la normalización las pruebas de deducción natural?
• ¿Cómo se relacionan las versiones clásica e intuicionista de estos cálculos?

Key theories

Reglas de introducción y eliminación

Cada conectivo se rige por reglas que lo introducen y reglas que lo explotan, y su armonía, que la eliminación recupera exactamente lo que la introducción aporta, expresa el significado del conectivo.

Teorema de normalización

Prawitz demostró que las pruebas de deducción natural pueden reducirse a una forma normal libre de rodeos donde una introducción es inmediatamente deshecha por una eliminación, el análogo de la deducción natural a la eliminación de cortes (cut-elimination).

Correspondencia de los dos cálculos

La deducción natural y el cálculo de secuentes prueban los mismos teoremas y pueden traducirse el uno al otro, correspondiendo las reglas izquierdas de los secuentes a las reglas de eliminación de la deducción natural.

Clinical relevance

Estos cálculos son los formatos estándar para estudiar las pruebas estructuralmente: la deducción natural subyace a la teoría de tipos y a los asistentes de prueba a través de la correspondencia pruebas-como-programas, mientras que el cálculo de secuentes, con su propiedad de subfórmula después de la eliminación de cortes (cut-elimination), es la base de la búsqueda automatizada de pruebas y los tableaux analíticos.

History

Gentzen introdujo tanto la deducción natural como el cálculo de secuentes en 1934 y 1935, ideando el cálculo de secuentes para obtener su teorema de eliminación de cortes después de encontrar la deducción natural más difícil de analizar. Prawitz revivió la deducción natural en 1965 con un estudio exhaustivo de normalización, y los sistemas se volvieron centrales para los desarrollos posteriores de pruebas-como-programas.

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

¿Cuál es la diferencia entre la deducción natural y el cálculo de secuentes?

La deducción natural trabaja con fórmulas bajo un contexto de suposiciones y utiliza reglas de eliminación, lo que se asemeja mucho a la prueba informal. El cálculo de secuentes trabaja con implicaciones explícitas y reemplaza las reglas de eliminación por reglas de introducción izquierda, un formato que hace transparente la eliminación de cortes (cut-elimination) y la propiedad de subfórmula.

¿Por qué es importante la normalización?

Una prueba normal no contiene rodeos y tiene la propiedad de subfórmula, por lo que cada fórmula en ella es una subfórmula de la conclusión o de las premisas. Esto restringe la forma de las pruebas, produce resultados de consistencia y, a través de la correspondencia pruebas-como-programas, corresponde a la evaluación de un programa a un valor.