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 demostraciones matemáticas.
[2] Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada.
La deducción natural fue introducida por Gerhard Gentzen en su trabajo Investigaciones sobre la inferencia lógica (Untersuchungen über das logische Schliessen), publicado en 1934-1935.
[2] Sea a una constante de individuo y t un término.
Para obtener cada una de estas subfórmulas, cuyas conectivas principales son condicionales materiales, se debe suponer el antecedente e intentar derivar el consecuente.