Deducción natural

Deducción natural
La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostracionesmatemáticas.12 En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas deinferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla.2 Una demostración se contruye partiendo de supuestos y aplicando las reglas para llegar a laconclusión deseada.
La deducción natural fue introducida por Gerhard Gentzen en su trabajo Investigaciones sobre la inferencia lógica (Untersuchungenüber das logischeSchliessen), publicado en 1934-1935.2Reglas de inferencia
Conectivas
Conectiva Nombre de la regla Abreviación Formalización Cálculo de secuentes
Introducción de la negación
(véase reducción al absurdo)

Eliminación de lanegación
Introducción de la conjunción

Eliminación de la conjunción

Introducción de la disyunción

Eliminación de la disyunción
(véase silogismo disyuntivo)Introducción del condicional material
(véase teorema de la deducción)

Eliminación del condicional material
(véase modus ponens)

Introducción del bicondicional

Eliminacióndel bicondicional

Cuantificadores
Sea a una constante de individuo y t un término. Sea A(b/c) el resultado de reemplazar todas las apariciones de b en A por c. Luego:
Cuantificador Nombrede la regla Abreviación Formalización Cálculo de secuentes
Introducción del cuantificador universal

Eliminación del cuantificador universal

Introducción del cuantificadorexistencial

Eliminación del cuantificador existencial


Demostraciones
Ejemplo sencillo
A demostrar:
Paso Fórmula Razón
1 Supuesto.
2 Desde (1) por introducción de la disyunción....