Forma normal (deducción natural)

En lógica matemática y teoría de la demostración, una derivación en forma normal, en el contexto de la deducción natural, se refiere a una demostración que no contiene rodeos, es decir, pasos en los que primero se introduce una fórmula y luego se elimina inmediatamente.

El concepto de normalización en la deducción natural fue introducido por Dag Prawitz en la década de 1960 como parte de un esfuerzo general para analizar la estructura de las demostraciones y eliminar pasos de razonamiento innecesarios. ^{[ 1 ]} El teorema de normalización asociado establece que toda derivación en la deducción natural puede transformarse en forma normal.

La deducción natural es un sistema de lógica formal que utiliza reglas de introducción y eliminación para cada conector lógico. Las reglas de introducción describen cómo construir una fórmula de una forma particular, mientras que las reglas de eliminación describen cómo inferir información a partir de dichas fórmulas. Una derivación está en forma normal si no contiene ninguna fórmula que sea a la vez:

• la conclusión de una regla de introducción, y
• la premisa principal de una regla de eliminación.

Se dice que una derivación que contiene dicha estructura incluye un desvío . La normalización implica transformar una derivación para eliminar todos esos desvíos, produciendo así una demostración que refleja directamente las dependencias lógicas de la conclusión con respecto a los supuestos.

Otra definición de derivación normal en lógica clásica es: ^{[ 2 ]}

Una derivación en NK es normal si todas las premisas principales de las reglas E son suposiciones.

El teorema de normalización para la deducción natural establece que:

Toda derivación en deducción natural puede convertirse en una derivación en forma normal.

Este resultado fue demostrado por primera vez por Dag Prawitz en 1965. ^{[ 1 ]} El proceso de normalización generalmente implica identificar y eliminar fórmulas máximas —fórmulas introducidas e inmediatamente eliminadas— a través de una secuencia de pasos de reducción local.

La normalización tiene varias consecuencias importantes:

• Esto implica la propiedad de subfórmula : cualquier fórmula que aparezca en la demostración es una subfórmula de las suposiciones o de la conclusión.
• Garantiza la coherencia del sistema: no se deriva ninguna contradicción de la ausencia de supuestos.
• Admite contenido constructivo en lógica: las demostraciones corresponden a construcciones o cálculos explícitos.

Una derivación que incluye un desvío: ${\displaystyle A\rightarrow A}$

1. [A] (suposición) 2. A → A (→ introducción, descarga 1) 3. [A] (suposición) 4. A (→ eliminación de 2 y 3) 

Esto introduce y luego elimina inmediatamente una implicación. Una derivación normal es:

1. [A] 2. A → A (→ introducción) 

Una derivación que incluye un desvío: ${\displaystyle A,B\vdash A}$

${\displaystyle {\frac {{\frac {A\quad B}{A\land B}}[\land {\text{I}}]}{A}}[\land {\text{E}}]\quad \Rightarrow \quad A}$

La eliminación es innecesaria si ya está disponible. ${\displaystyle A}$

La normalización es fundamental en varias áreas de la lógica y la informática:

• En la teoría de la demostración , garantiza que los sistemas lógicos tengan metapropiedades deseables, como la consistencia y la propiedad de subfórmula.
• En la teoría de tipos , constituye la base de la solidez y la completitud de los algoritmos de verificación de tipos.
• En los asistentes de demostración (por ejemplo , Rocq , Agda ), la normalización se utiliza para verificar que las demostraciones formales sean constructivas y terminantes.
• En la programación funcional , el proceso de normalización corresponde a estrategias de evaluación para cálculos lambda tipados .

• Deducción natural
• Correspondencia entre Curry y Howard
• Teorema de eliminación de cortes
• Cálculo de secuencias

• Prawitz, Dag (1965). Deducción natural: un estudio teórico de prueba (tesis). Estudios de Filosofía de Estocolmo. vol. 3. Estocolmo: Almqvist & Wiksell.
• Prawitz, Dag (2006) [1965]. Deducción natural: un estudio teórico de la demostración (reimpresión de la tesis de 1965). Mineola, Nueva York: Dover Publications . ISBN 9780486446554OCLC 61296001​ ​
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998]. Lecciones sobre el isomorfismo de Curry-Howard . Estudios en lógica y fundamentos de las matemáticas. Vol. 149. Elsevier Science . CiteSeerX  10.1.1.17.7385 . ISBN 978-0-444-52077-7.
• Troelstra, AS; Schwichtenberg, H. (2000). Teoría básica de la demostración . Cambridge University Press. ISBN 9780521779111.
• von Plato, Jan (2013). Elementos del razonamiento lógico (1.ª ed.). Cambridge: Cambridge University Press . ISBN 978-1-107-03659-8.