Deducción natural

En lógica y teoría de la prueba , la deducción natural es un tipo de cálculo de prueba en el que el razonamiento lógico se expresa mediante reglas de inferencia estrechamente relacionadas con la forma "natural" de razonamiento. ^[1] Esto contrasta con los sistemas de estilo Hilbert , que en cambio utilizan axiomas tanto como sea posible para expresar las leyes lógicas del razonamiento deductivo .

La deducción natural surgió de un contexto de insatisfacción con las axiomatizaciones del razonamiento deductivo comunes a los sistemas de Hilbert , Frege y Russell (véase, por ejemplo, el sistema de Hilbert ). Dichas axiomatizaciones fueron las más famosas utilizadas por Russell y Whitehead en su tratado matemático Principia Mathematica . Inspirado por una serie de seminarios en Polonia en 1926 por Łukasiewicz que abogaban por un tratamiento más natural de la lógica, Jaśkowski hizo los primeros intentos de definir una deducción más natural, primero en 1929 utilizando una notación diagramática, y luego actualizando su propuesta en una secuencia de artículos en 1934 y 1935. ^[2] Sus propuestas llevaron a diferentes notaciones como el cálculo al estilo de Fitch (o diagramas de Fitch) o el método de Suppes para el cual Lemmon dio una variante ahora conocida como notación de Suppes-Lemmon .

La deducción natural en su forma moderna fue propuesta independientemente por el matemático alemán Gerhard Gentzen en 1933, en una disertación presentada en la facultad de ciencias matemáticas de la Universidad de Göttingen . ^[3] El término deducción natural (o más bien, su equivalente alemán natürliches Schließen ) fue acuñado en ese artículo:

Gentzen estaba motivado por el deseo de establecer la consistencia de la teoría de números . No pudo probar el resultado principal requerido para el resultado de consistencia, el teorema de eliminación de cortes —el Hauptsatz— directamente para la deducción natural. Por esta razón introdujo su sistema alternativo, el cálculo secuente , para el cual demostró el Hauptsatz tanto para la lógica clásica como para la intuicionista . En una serie de seminarios en 1961 y 1962, Prawitz dio un resumen completo de los cálculos de deducción natural y trasladó gran parte del trabajo de Gentzen con los cálculos secuentes al marco de la deducción natural. Su monografía de 1965 Deducción natural: un estudio teórico de la prueba ^[5] se convertiría en una obra de referencia sobre la deducción natural e incluía aplicaciones para la lógica modal y de segundo orden .

En la deducción natural, una proposición se deduce de una colección de premisas aplicando reglas de inferencia de forma repetida. El sistema presentado en este artículo es una variación menor de la formulación de Gentzen o Prawitz, pero con una mayor adherencia a la descripción de Martin-Löf de los juicios lógicos y los conectivos. ^[6]

La deducción natural ha tenido una gran variedad de estilos de notación, ^[7] lo que puede dificultar el reconocimiento de una demostración si no se está familiarizado con alguno de ellos. Para ayudar con esta situación, este artículo tiene una sección de Notación que explica cómo leer toda la notación que realmente utilizará. Esta sección simplemente explica la evolución histórica de los estilos de notación, la mayoría de los cuales no se pueden mostrar porque no hay ilustraciones disponibles bajo una licencia de derechos de autor pública ; se remite al lector a la SEP y la IEP para obtener imágenes.

• Gentzen inventó la deducción natural utilizando pruebas en forma de árbol (ver § Notación de árbol de Gentzen para más detalles).
• Jaśkowski cambió esto a una notación que usaba varios cuadros anidados. ^[7]
• Fitch modificó el método de Jaśkowski para dibujar las cajas, creando la notación Fitch . ^[7]
• 1940: En un libro de texto, Quine ^[8] indicó las dependencias antecedentes mediante números de línea entre corchetes, anticipándose a la notación de números de línea de Suppes de 1957.
• 1950: En un libro de texto, Quine (1982, pp. 241–255) demostró un método para utilizar uno o más asteriscos a la izquierda de cada línea de prueba para indicar dependencias. Esto es equivalente a las barras verticales de Kleene. (No está totalmente claro si la notación de asterisco de Quine apareció en la edición original de 1950 o se agregó en una edición posterior).
• 1957: Introducción a la demostración de teoremas de lógica práctica en un libro de texto de Suppes (1999, pp. 25-150). En él se indicaban las dependencias (es decir, las proposiciones antecedentes) mediante números de línea a la izquierda de cada línea.
• 1963: Stoll (1979, pp. 183–190, 215–219) utiliza conjuntos de números de línea para indicar dependencias antecedentes de las líneas de argumentos lógicos secuenciales basados ​​en reglas de inferencia de deducción natural.
• 1965: Todo el libro de texto de Lemmon (1965) es una introducción a las pruebas lógicas utilizando un método basado en el de Suppes , lo que ahora se conoce como notación de Suppes-Lemmon .
• 1967: En un libro de texto, Kleene (2002, pp. 50-58, 128-130) demostró brevemente dos tipos de pruebas de lógica práctica: un sistema que utiliza citas explícitas de proposiciones antecedentes a la izquierda de cada línea, y el otro sistema que utiliza barras verticales a la izquierda para indicar dependencias. ^[a]

A continuación se muestra una tabla con las variantes de notación más comunes para los conectivos lógicos .

Variantes notacionales de los conectivos ^{[9] [10]}

Conectivo	Símbolo
Y	${\estilo de visualización A\y B}$, , , ,${\displaystyle A\cdot B}$${\estilo de visualización AB}$${\estilo de visualización A\&B}$${\estilo de visualización A\&\&B}$
equivalente	${\displaystyle A\equiv B}$, ,${\displaystyle A\flecha izquierda derecha B}$${\displaystyle A\leftrightharpoons B}$
implica	${\displaystyle A\Flecha derecha B}$, ,${\displaystyle A\distorsión B}$${\displaystyle A\flecha derecha B}$
NAND	${\displaystyle A{\overline {\land }}B}$, ,${\estilo de visualización A\medio B}$${\displaystyle {\overline {A\cdot B}}}$
no equivalente	${\displaystyle A\no es \equiv B}$, ,${\displaystyle A\no \Flecha izquierda derecha B}$${\displaystyle A\nleftrightarrow B}$
NI	${\displaystyle A{\overline {\lor }}B}$, ,${\displaystyle A\flecha hacia abajo B}$${\displaystyle {\overline {A+B}}}$
NO	${\displaystyle \neg A}$, , ,${\estilo de visualización -A}$${\displaystyle {\overline {A}}}$${\displaystyle \sim A}$
O	${\displaystyle A\lo B}$, , ,${\displaystyle A+B}$${\displaystyle A\mid B}$${\displaystyle A\parallel B}$
XNOR	${\displaystyle A}$XNOR${\displaystyle B}$
XOR	${\displaystyle A{\underline {\lor }}B}$,${\displaystyle A\oplus B}$

Gentzen , que inventó la deducción natural, tenía su propio estilo de notación para los argumentos. Esto se ejemplificará con un argumento simple a continuación. Digamos que tenemos un argumento de ejemplo simple en lógica proposicional , como, por ejemplo, "si está lloviendo, entonces está nublado; está lloviendo; por lo tanto, está nublado". (Esto es en modus ponens ). Representando esto como una lista de proposiciones, como es común, tendríamos:

${\displaystyle 1)~P\to Q}$

${\displaystyle 2)~P}$

${\displaystyle \therefore ~Q}$

En la notación de Gentzen, ^[7] esto se escribiría así:

${\displaystyle {\frac {P\to Q,P}{Q}}}$

Las premisas se muestran sobre una línea, llamada línea de inferencia , ^{[11] [12]} separadas por una coma , que indica combinación de premisas. ^[13] La conclusión se escribe debajo de la línea de inferencia. ^[11] La línea de inferencia representa la consecuencia sintáctica , ^[11] a veces llamada consecuencia deductiva , ^[14] que también se simboliza con ⊢. ^{[15] [14]} Por lo tanto, lo anterior también se puede escribir en una línea como . (El torniquete, para la consecuencia sintáctica, tiene menor precedencia que la coma, que representa la combinación de premisas, que a su vez tiene menor precedencia que la flecha, utilizada para la implicación material; por lo que no se necesitan paréntesis para interpretar esta fórmula). ^[13]${\displaystyle P\to Q,P\vdash Q}$

La consecuencia sintáctica contrasta con la consecuencia semántica , ^[16] que se simboliza con ⊧. ^{[15] [14]} En este caso, la conclusión se sigue sintácticamente porque la deducción natural es un sistema de prueba sintáctica , que asume las reglas de inferencia como primitivas .

En gran parte de este artículo se utilizará el estilo de Gentzen. Las anotaciones de descarga de Gentzen utilizadas para internalizar juicios hipotéticos se pueden evitar representando las pruebas como un árbol de secuencias Γ ⊢A en lugar de un árbol de juicios de que A (es verdadero).

Muchos libros de texto utilizan la notación de Suppes-Lemmon , ^[7] por lo que este artículo también la dará, aunque por ahora, esto solo se incluye para la lógica proposicional , y el resto de la cobertura se da solo en estilo Gentzen. Una prueba , presentada de acuerdo con el estilo de notación de Suppes-Lemmon , es una secuencia de líneas que contienen oraciones, ^[17] donde cada oración es una suposición o el resultado de aplicar una regla de prueba a oraciones anteriores en la secuencia. ^[17] Cada línea de prueba se compone de una oración de prueba , junto con su anotación , su conjunto de suposiciones y el número de línea actual . ^[17] El conjunto de suposiciones enumera las suposiciones de las que depende la oración de prueba dada, a las que se hace referencia mediante los números de línea. ^[17] La ​​anotación especifica qué regla de prueba se aplicó y a qué líneas anteriores para producir la oración actual. ^[17] Aquí hay un ejemplo de prueba:

Prueba al estilo Suppes-Lemmon (primer ejemplo)

Conjunto de suposiciones	Número de línea	Oración de prueba	Anotación
1	1	${\displaystyle P\to Q}$	A
2	2	${\displaystyle -Q}$	A
3	3	${\displaystyle P}$	A
1 , 3	4	${\displaystyle Q}$	1 , 3 →E
1 , 2	5	${\displaystyle -P}$	2 , 4 RAA

Esta prueba será más clara cuando se especifiquen las reglas de inferencia y sus anotaciones apropiadas (véase § Reglas de inferencia proposicional (estilo Suppes-Lemmon).

Esta sección define la sintaxis formal de un lenguaje de lógica proposicional , contrastando las formas comunes de hacerlo con una forma de hacerlo al estilo Gentzen.

El lenguaje formal de un cálculo proposicional suele definirse mediante una definición recursiva , como ésta, de Bostock : ^[18]${\displaystyle {\mathcal {L}}}$

1. Cada letra-frase es una fórmula .
2. " " y " " son fórmulas.${\displaystyle \top }$${\displaystyle \bot }$
3. Si es una fórmula, también lo es .${\displaystyle \varphi }$${\displaystyle \neg \varphi }$
4. Si y son fórmulas, entonces también lo son , , , .${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle (\varphi \land \psi )}$${\displaystyle (\varphi \lor \psi )}$${\displaystyle (\varphi \to \psi )}$${\displaystyle (\varphi \leftrightarrow \psi )}$
5. Nada más es una fórmula.

Hay otras formas de hacerlo, como la gramática BNF . ^{[19] [20]}${\displaystyle \phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\land ~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi }$

También se puede dar una definición de sintaxis utilizando la notación de árbol de Gentzen, escribiendo fórmulas bien formadas debajo de la línea de inferencia y cualquier variable esquemática utilizada por esas fórmulas encima de ella. ^[20] Por ejemplo, el equivalente de las reglas 3 y 4, de la definición de Bostock anterior, se escribe de la siguiente manera:

${\displaystyle {\frac {\varphi }{(\neg \varphi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \lor \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \land \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \rightarrow \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \leftrightarrow \psi )}}}$.

Una convención de notación diferente considera la sintaxis del lenguaje como una gramática categorial con una única categoría "fórmula", denotada por el símbolo . Por lo tanto, todos los elementos de la sintaxis se introducen mediante categorizaciones, para las cuales la notación es , que significa " es una expresión para un objeto en la categoría ." ^[21] Las letras de la oración, entonces, se introducen mediante categorizaciones como ,  ,  , y así sucesivamente; ^[21] los conectores, a su vez, se definen mediante enunciados similares a los anteriores, pero utilizando la notación de categorización, como se ve a continuación:${\displaystyle {\mathcal {F}}}$${\displaystyle \varphi :{\mathcal {F}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {F}}}$${\displaystyle P:{\mathcal {F}}}$${\displaystyle Q:{\mathcal {F}}}$${\displaystyle R:{\mathcal {F}}}$

Conectivos definidos a través de una gramática categorial ^[21]

Conjunción (&)	Disyunción (∨)	Implicación (→)	Negación (¬)
${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\&(A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\vee (A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\supset (A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}}{\neg (A):{\mathcal {F}}}}}$

En el resto de este artículo, se utilizará la notación de categorización para cualquier declaración en notación Gentzen que defina la gramática del lenguaje; cualquier otra declaración en notación Gentzen será una inferencia, que afirmará que se sigue un consecuente en lugar de que una expresión es una fórmula bien formada.${\displaystyle \varphi :{\mathcal {F}}}$

La siguiente es una lista completa de reglas de inferencia primitivas para la deducción natural en la lógica proposicional clásica: ^[20]

Reglas de la lógica proposicional clásica

Reglas de introducción	Reglas de eliminación
${\displaystyle {\begin{array}{c}\varphi \qquad \psi \\\hline \varphi \wedge \psi \end{array}}(\wedge _{i})}$	${\displaystyle {\begin{array}{c}\varphi \wedge \psi \\\hline \varphi \end{array}}(\wedge _{e})}$
${\displaystyle {\begin{array}{c}\varphi \\\hline \varphi \vee \psi \end{array}}(\vee _{i})}$	${\displaystyle {\cfrac {\varphi \vee \psi \quad {\begin{matrix}[\varphi ]^{u}\\\vdots \\\chi \end{matrix}}\quad {\begin{matrix}[\psi ]^{v}\\\vdots \\\chi \end{matrix}}}{\chi }}\ \vee _{E^{u,v}}}$
${\displaystyle {\begin{array}{c}[\varphi ]^{u}\\\vdots \\\psi \\\hline \varphi \to \psi \end{array}}(\to _{i})\ u}$	${\displaystyle {\begin{array}{c}\varphi \qquad \varphi \to \psi \\\hline \psi \end{array}}(\to _{e})}$
${\displaystyle {\begin{array}{c}[\varphi ]^{u}\\\vdots \\\bot \\\hline \neg \varphi \end{array}}(\neg _{i})\ u}$	${\displaystyle {\begin{array}{c}\varphi \qquad \neg \varphi \\\hline \bot \end{array}}(\neg _{e})}$
	${\displaystyle {\begin{array}{c}[\neg \varphi ]^{u}\\\vdots \\\bot \\\hline \varphi \end{array}}({\text{PBC}})\ u}$

Esta tabla sigue la costumbre de utilizar letras griegas como esquemas , que pueden abarcar cualquier fórmula, en lugar de solo proposiciones atómicas. El nombre de una regla se da a la derecha de su árbol de fórmulas. Por ejemplo, la primera regla de introducción se llama , que es la abreviatura de "introducción de conjunción".${\displaystyle \wedge _{i}}$

Como ejemplo del uso de reglas de inferencia, considere la conmutatividad de la conjunción. Si A ∧ B , entonces B ∧ A ; esta derivación se puede obtener componiendo reglas de inferencia de tal manera que las premisas de una inferencia inferior coincidan con la conclusión de la siguiente inferencia superior.

Como segundo ejemplo, considere la derivación de " A ⊃ (B ⊃ (A ∧ B)) ":

Esta derivación completa no tiene premisas insatisfechas; sin embargo, las subderivaciones son hipotéticas. Por ejemplo, la derivación de " B ⊃ (A ∧ B) " es hipotética con antecedente " A " (llamado u ).

Las reglas de inferencia de deducción natural, debidas en última instancia a Gentzen , se dan a continuación. ^[22] Hay diez reglas primitivas de prueba, que son la regla de suposición , más cuatro pares de reglas de introducción y eliminación para los conectivos binarios, y la regla reductio ad adbsurdum . ^[17] El silogismo disyuntivo se puede utilizar como una alternativa más fácil a la ∨-eliminación adecuada, ^[17] y MTT y DN son reglas dadas comúnmente, ^[22] aunque no son primitivas. ^[17]

Lista de reglas de inferencia

Nombre de la regla	Nombres alternativos	Anotación	Conjunto de suposiciones	Declaración
Regla de suposiciones [22]	Asunción [17]	A [22] [17]	El número de línea actual. [17]	En cualquier etapa del argumento, introduzca una proposición como supuesto del argumento. [22] [17]
Introducción de conjunciones	Introducción del signo &, [22] [17] conjunción (CONJ) [17] [23]	m, n y yo [17] [22]	La unión de los conjuntos de supuestos en las líneas m y n . [17]	A partir de las líneas m y n , inferir . [22] [17]${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \varphi ~\&~\psi }$
Eliminación de conjunciones	Simplificación (S), [17] eliminación del ampersand [22] [17]	M&E [17] [22]	Lo mismo que en la línea m . [17]	A partir de la línea m , inferir y . [17] [22]${\displaystyle \varphi ~\&~\psi }$${\displaystyle \varphi }$${\displaystyle \psi }$
Introducción a la disyunción [22]	Adición (ADD) [17]	m ∨I [17] [22]	Lo mismo que en la línea m . [17]	A partir de la línea m , inferir , cualquiera que sea. [17] [22]${\displaystyle \varphi }$${\displaystyle \varphi \lor \psi }$${\displaystyle \psi }$
Eliminación de disyunción	Eliminación de cuñas, [22] dilema (DL) [23]	j,k,l,m,n ∨E [22]	Las rectas j,k,l,m,n . [22]	A partir de una línea j , y una suposición de una línea k , y una derivación de a partir de una línea l , y una suposición de una línea m , y una derivación de a partir de una línea n , inferir . [22]${\displaystyle \varphi \lor \psi }$${\displaystyle \varphi }$${\displaystyle \chi }$${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \chi }$${\displaystyle \psi }$${\displaystyle \chi }$
Silogismo disyuntivo	Eliminación de cuña (∨E), [17] modus tollendo ponens (MTP) [17]	m,n DS [17]	La unión de los conjuntos de supuestos en las líneas m y n . [17]	Desde la línea m y la línea n , inferir ; desde la línea m y la línea n , inferir . [17]${\displaystyle \varphi \lor \psi }$${\displaystyle -\varphi }$${\displaystyle \psi }$${\displaystyle \varphi \lor \psi }$${\displaystyle -\psi }$${\displaystyle \varphi }$
Eliminación de flechas [17]	Modus ponendo ponens (MPP), [22] [17] modus ponens (MP), [23] [17] eliminación condicional	m, n →E [17] [22]	La unión de los conjuntos de supuestos en las líneas m y n . [17]	A partir de la línea m y de la línea n , inferir . [17]${\displaystyle \varphi \to \psi }$${\displaystyle \varphi }$${\displaystyle \psi }$
Introducción de la flecha [17]	Prueba condicional (CP), [23] [22] [17] introducción condicional	n, →I (m) [17] [22]	Todo lo que se supone se establece en la línea n , excepto m , la línea donde se supuso el antecedente. [17]	A partir de la línea n , siguiendo el supuesto de la línea m , inferir . [17]${\displaystyle \psi }$${\displaystyle \varphi }$${\displaystyle \varphi \to \psi }$
Reducción al absurdo [22]	Prueba indirecta (PI), [17] introducción de la negación (−I), [17] eliminación de la negación (−E) [17]	m,  n  RAA  (k) [17]	La unión de los conjuntos de suposiciones en las líneas m y n , excluyendo k (la suposición negada). [17]	A partir de una oración y su negación [b] en las líneas m y n , infiera la negación de cualquier suposición que aparezca en la prueba (en la línea k ). [17]
Introducción de doble flecha [17]	Definición bicondicional ( Df ↔), [22] introducción bicondicional	m, n ↔ yo [17]	La unión de los conjuntos de supuestos en las líneas m y n . [17]	A partir de las líneas m y n , inferir . [17]${\displaystyle \varphi \to \psi }$${\displaystyle \psi \to \varphi }$${\displaystyle \varphi \leftrightarrow \psi }$
Eliminación de doble flecha [17]	Definición bicondicional ( Df ↔), [22] eliminación bicondicional	m ↔ E [17]	Lo mismo que en la línea m . [17]	A partir de la línea m , infiera o . [17]${\displaystyle \varphi \leftrightarrow \psi }$${\displaystyle \varphi \to \psi }$${\displaystyle \psi \to \varphi }$
Doble negación [22] [23]	Eliminación de doble negación	mDN [22]	Lo mismo que en la línea m . [22]	A partir de la línea m , inferir . [22]${\displaystyle --\varphi }$${\displaystyle \varphi }$
Modo de transporte de cargas [22]	Modus operandi (MT) [23]	m, n MTT [22]	La unión de los conjuntos de supuestos en las líneas m y n . [22]	A partir de la línea m y de la línea n , inferir . [22]${\displaystyle \varphi \to \psi }$${\displaystyle -\psi }$${\displaystyle -\varphi }$

Recordemos que ya se dio un ejemplo de demostración al introducir la notación § Suppes-Lemmon. Este es un segundo ejemplo.

Prueba al estilo Suppes-Lemmon (segundo ejemplo)

Conjunto de suposiciones	Número de línea	Oración de prueba	Anotación
1	1	${\displaystyle P\lor Q}$	A
2	2	${\displaystyle \neg P}$	A
3	3	${\displaystyle \neg P\to \neg Q}$	A
2 , 3	4	${\displaystyle \neg Q}$	2 , 3 →E
1 , 2 , 3	5	${\displaystyle P}$	1 , 4 y E
1 , 3	6	${\displaystyle P}$	2 , 5 RAA(2)
2 , 3	7	${\displaystyle \neg P}$	2 , 3 RAA(1)

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Se dice que una teoría es consistente si su falsedad no es demostrable (a partir de ninguna suposición) y es completa si cada teorema o su negación es demostrable utilizando las reglas de inferencia de la lógica. Estas son afirmaciones sobre la lógica en su totalidad y suelen estar vinculadas a alguna noción de modelo . Sin embargo, existen nociones locales de consistencia y completitud que son comprobaciones puramente sintácticas de las reglas de inferencia y no requieren apelaciones a modelos. La primera de ellas es la consistencia local, también conocida como reducibilidad local, que dice que cualquier derivación que contenga una introducción de un conectivo seguida inmediatamente por su eliminación puede convertirse en una derivación equivalente sin este rodeo. Es una comprobación de la fuerza de las reglas de eliminación: no deben ser tan fuertes como para incluir conocimiento que no esté ya contenido en sus premisas. Como ejemplo, considere las conjunciones.

${\displaystyle {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ }}u\qquad {\cfrac {}{B\ }}w}{A\wedge B\ }}\wedge _{I}}{A\ }}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ }}u}$

En el caso dual, la completitud local dice que las reglas de eliminación son lo suficientemente fuertes como para descomponer un conectivo en las formas adecuadas para su regla de introducción. Nuevamente para las conjunciones:

${\displaystyle {\cfrac {}{A\wedge B\ }}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ }}u}{A\ }}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ }}u}{B\ }}\wedge _{E2}}{A\wedge B\ }}\wedge _{I}\end{aligned}}}$

Estas nociones corresponden exactamente a la β-reducción (reducción beta) y a la η-conversión (conversión eta) en el cálculo lambda , utilizando el isomorfismo de Curry-Howard . Por completitud local, vemos que cada derivación puede convertirse en una derivación equivalente donde se introduce el conectivo principal. De hecho, si la derivación entera obedece a este orden de eliminaciones seguidas de introducciones, entonces se dice que es normal . En una derivación normal todas las eliminaciones ocurren por encima de las introducciones. En la mayoría de las lógicas, cada derivación tiene una derivación normal equivalente, llamada forma normal . La existencia de formas normales es generalmente difícil de probar utilizando solo la deducción natural, aunque tales explicaciones existen en la literatura, más notablemente por Dag Prawitz en 1961. ^[24] Es mucho más fácil mostrar esto indirectamente por medio de una presentación de cálculo secuente sin cortes .

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

La lógica de la sección anterior es un ejemplo de lógica de ordenación única , es decir , una lógica con un único tipo de objeto: proposiciones. Se han propuesto muchas extensiones de este marco simple; en esta sección lo ampliaremos con un segundo tipo de individuos o términos . Más precisamente, añadiremos una nueva categoría, "término", denotada . Fijaremos un conjunto numerable de variables , otro conjunto numerable de símbolos de función y construiremos términos con las siguientes reglas de formación:${\displaystyle {\mathcal {T}}}$${\displaystyle V}$${\displaystyle F}$

${\displaystyle {\frac {v\in V}{v:{\mathcal {T}}}}{\hbox{ var}}_{F}}$

y

${\displaystyle {\frac {f\in F\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{f(t_{1},t_{2},\cdots ,t_{n}):{\mathcal {T}}}}{\hbox{ app}}_{F}}$

Para las proposiciones, consideramos un tercer conjunto contable P de predicados , y definimos predicados atómicos sobre términos con la siguiente regla de formación:

${\displaystyle {\frac {\phi \in P\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{\phi (t_{1},t_{2},\cdots ,t_{n}):{\mathcal {F}}}}{\hbox{ pred}}_{F}}$

Las dos primeras reglas de formación proporcionan una definición de un término que es efectivamente la misma que la definida en el álgebra de términos y la teoría de modelos , aunque el enfoque de esos campos de estudio es bastante diferente de la deducción natural. La tercera regla de formación define efectivamente una fórmula atómica , como en la lógica de primer orden , y nuevamente en la teoría de modelos.

A estas se añaden un par de reglas de formación que definen la notación para proposiciones cuantificadas ; una para cuantificación universal (∀) y existencial (∃):

${\displaystyle {\frac {x\in V\qquad A:{\mathcal {F}}}{\forall x.A:{\mathcal {F}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A:{\mathcal {F}}}{\exists x.A:{\mathcal {F}}}}\;\exists _{F}}$

El cuantificador universal tiene las reglas de introducción y eliminación:

${\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a:{\mathcal {T}}}}{\text{ u}}\\\vdots \\{}[a/x]A\end{array}}{\forall x.A}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A\qquad t:{\mathcal {T}}}{[t/x]A}}\;\forall _{E}}$

El cuantificador existencial tiene las reglas de introducción y eliminación:

${\displaystyle {\frac {[t/x]A}{\exists x.A}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a:{\mathcal {T}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A\quad &C\\\end{array}}{C}}\exists _{E^{a,u,v}}}$

En estas reglas, la notación [ t / x ] A representa la sustitución de t por cada instancia (visible) de x en A , evitando la captura. ^[c] Como antes, los superíndices en el nombre representan los componentes que se descargan: el término a no puede ocurrir en la conclusión de ∀I (tales términos se conocen como variables propias o parámetros ), y las hipótesis nombradas u y v en ∃E se localizan en la segunda premisa en una derivación hipotética. Aunque la lógica proposicional de las secciones anteriores era decidible , agregar los cuantificadores hace que la lógica sea indecidible.

Hasta ahora, las extensiones cuantificadas son de primer orden : distinguen las proposiciones de los tipos de objetos sobre los que se cuantifican. La lógica de orden superior adopta un enfoque diferente y sólo tiene un único tipo de proposiciones. Los cuantificadores tienen como dominio de cuantificación el mismo tipo de proposiciones, como se refleja en las reglas de formación:

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\forall p.A:{\mathcal {F}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\exists p.A:{\mathcal {F}}}}\;\exists _{F^{u}}}$

El análisis de las formas de introducción y eliminación de la lógica de orden superior queda fuera del alcance de este artículo. Es posible estar en un punto intermedio entre la lógica de primer orden y la lógica de orden superior. Por ejemplo, la lógica de segundo orden tiene dos tipos de proposiciones: una que cuantifica sobre términos y la otra que cuantifica sobre proposiciones de la primera.

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Hasta ahora, la presentación de la deducción natural se ha centrado en la naturaleza de las proposiciones sin dar una definición formal de una prueba . Para formalizar la noción de prueba, modificamos ligeramente la presentación de las derivaciones hipotéticas. Etiquetamos los antecedentes con variables de prueba (de algún conjunto contable V de variables) y decoramos el sucedente con la prueba real. Los antecedentes o hipótesis se separan del sucedente por medio de un torniquete (⊢). Esta modificación a veces se conoce con el nombre de hipótesis localizadas . El siguiente diagrama resume el cambio.

──── u 1 ──── u 2 ... ──── u n J 1 J 2 J n ⋮ Yo

u 1 :J 1 , u 2 :J 2 , ..., u n :J n ⊢ J

El conjunto de hipótesis se escribirá como Γ cuando su composición exacta no sea relevante. Para hacer explícitas las pruebas, pasamos del juicio sin pruebas " A " a un juicio: "π es una prueba de (A) ", que se escribe simbólicamente como "π : A ". Siguiendo el enfoque estándar, las pruebas se especifican con sus propias reglas de formación para el juicio "π prueba ". La prueba más simple posible es el uso de una hipótesis etiquetada; en este caso, la evidencia es la etiqueta misma.

u ∈ V─────── prueba-Ftu prueba

───────────────────── hipnosisu:A ⊢ u : A

Reexaminemos algunos de los conectivos con pruebas explícitas. Para la conjunción, observamos la regla de introducción ∧I para descubrir la forma de las pruebas de conjunción: deben ser un par de pruebas de los dos conjuntivos. Así:

Prueba de π 1 Prueba de π 2──────────────────── par-F(π 1 , π 2 ) prueba

Γ ⊢ π 1  : A Γ ⊢ π 2  : B───────────────────────── ∧YoΓ ⊢ (π 1 , π 2 ) : A ∧ B

Las reglas de eliminación ∧E ₁ y ∧E ₂ seleccionan el conjunto izquierdo o el derecho; por lo tanto, las pruebas son un par de proyecciones: primera ( fst ) y segunda ( snd ).

prueba π─────────── fst -F fst π prueba

Γ ⊢ π : A ∧ B───────────── ∧E 1
Γ ⊢ primera π : A

prueba π─────────── snd -F snd π prueba

Γ ⊢ π : A ∧ B───────────── ∧E 2
Γ ⊢ snd π : B

Para la implicación, la forma introductoria localiza o vincula la hipótesis, escrita con λ; esto corresponde a la etiqueta descargada. En la regla, "Γ, u : A " representa el conjunto de hipótesis Γ, junto con la hipótesis adicional u .

prueba π──────────── λ-FPrueba de λu.π

Γ, u:A ⊢ π : B───────────────── ⊃YoΓ ⊢ λu.π : A ⊃ B

Prueba de π 1 Prueba de π 2─────────────────── aplicación-FPrueba de
π 1 π 2

Γ ⊢ π 1  : A ⊃ B Γ ⊢ π 2  : A──────────────────────────── ⊃EΓ ⊢ π 1 π 2  : B

Si se dispone de pruebas explícitamente, se pueden manipular y razonar sobre ellas. La operación clave en las pruebas es la sustitución de una prueba por un supuesto utilizado en otra prueba. Esto se conoce comúnmente como teorema de sustitución y se puede demostrar por inducción sobre la profundidad (o estructura) del segundo juicio.

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Si Γ ⊢ π ₁  : A y Γ, u : A ⊢ π ₂  : B , entonces Γ ⊢ [π ₁ / u ] π ₂  : B.

Hasta ahora, el juicio "Γ ⊢ π : A " ha tenido una interpretación puramente lógica. En la teoría de tipos , la visión lógica se cambia por una visión más computacional de los objetos. Las proposiciones en la interpretación lógica ahora se ven como tipos , y las demostraciones como programas en el cálculo lambda . Así, la interpretación de "π : A " es " el programa π tiene tipo A ". Los conectivos lógicos también reciben una lectura diferente: la conjunción se ve como producto (×), la implicación como la función flecha (→), etc. Sin embargo, las diferencias son solo cosméticas. La teoría de tipos tiene una presentación de deducción natural en términos de reglas de formación, introducción y eliminación; de hecho, el lector puede reconstruir fácilmente lo que se conoce como teoría de tipos simple a partir de las secciones anteriores.

La diferencia entre la lógica y la teoría de tipos es principalmente un cambio de enfoque de los tipos (proposiciones) a los programas (pruebas). La teoría de tipos está principalmente interesada en la convertibilidad o reducibilidad de los programas. Para cada tipo, hay programas canónicos de ese tipo que son irreducibles; estos se conocen como formas o valores canónicos . Si cada programa se puede reducir a una forma canónica, entonces se dice que la teoría de tipos es normalizadora (o débilmente normalizadora ). Si la forma canónica es única, entonces se dice que la teoría es fuertemente normalizadora . La normalizabilidad es una característica rara de la mayoría de las teorías de tipos no triviales, lo que es una gran desviación del mundo lógico. (Recuerde que casi cada derivación lógica tiene una derivación normal equivalente). Para esbozar la razón: en las teorías de tipos que admiten definiciones recursivas, es posible escribir programas que nunca se reducen a un valor; a tales programas de bucle generalmente se les puede dar cualquier tipo. En particular, el programa de bucle tiene tipo ⊥, aunque no hay una prueba lógica de "⊥". Por esta razón, las proposiciones como tipos; El paradigma de las pruebas como programas sólo funciona en una dirección, si es que funciona: interpretar una teoría de tipos como una lógica generalmente da como resultado una lógica inconsistente.

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Al igual que la lógica, la teoría de tipos tiene muchas extensiones y variantes, incluidas versiones de primer orden y de orden superior. Una rama, conocida como teoría de tipos dependientes , se utiliza en varios sistemas de demostración asistidos por ordenador . La teoría de tipos dependientes permite que los cuantificadores se extiendan a los propios programas. Estos tipos cuantificados se escriben como Π y Σ en lugar de ∀ y ∃, y tienen las siguientes reglas de formación:

Γ ⊢ Tipo A Γ, x:A ⊢ Tipo B───────────────────────────── Π-FΓ ⊢ Πx:A. Tipo B

Γ ⊢ Tipo A Γ, x:A ⊢ Tipo B──────────────────────────── Σ-FΓ ⊢ Σx:A. Tipo B

Estos tipos son generalizaciones de los tipos flecha y producto, respectivamente, como lo atestiguan sus reglas de introducción y eliminación.

Γ, x:A ⊢ π : B───────────────────── YoΓ ⊢ λx.π : Πx:A.B

Γ ⊢ π 1  : Πx:A. B Γ ⊢ π 2  : A───────────────────────────── ΠEΓ ⊢ π 1 π 2  : [π 2 /x] B

Γ ⊢ π 1  : A Γ, x:A ⊢ π 2  : B──────────────────────────────Γ ⊢ (π 1 , π 2 ) : Σx:A. B

Γ ⊢ π : Σx:A.B──────────────── ΣE 1
Γ ⊢ primera π : A

Γ ⊢ π : Σx:A.B──────────────────────── ΣE 2
Γ ⊢ snd π : [ fst π/x] B

La teoría de tipos dependientes en su máxima generalidad es muy poderosa: es capaz de expresar casi cualquier propiedad concebible de los programas directamente en los tipos del programa. Esta generalidad tiene un alto precio: o bien la comprobación de tipos es indecidible ( teoría de tipos extensional ), o bien el razonamiento extensional es más difícil ( teoría de tipos intensional ). Por esta razón, algunas teorías de tipos dependientes no permiten la cuantificación sobre programas arbitrarios, sino que se limitan a programas de un dominio de índice decidible dado , por ejemplo, números enteros, cadenas o programas lineales.

Dado que las teorías de tipos dependientes permiten que los tipos dependan de los programas, una pregunta natural que se plantea es si es posible que los programas dependan de los tipos, o de cualquier otra combinación. Hay muchos tipos de respuestas a estas preguntas. Un enfoque popular en la teoría de tipos es permitir que los programas se cuantifiquen sobre los tipos, también conocido como polimorfismo paramétrico ; de esto hay dos tipos principales: si los tipos y los programas se mantienen separados, entonces se obtiene un sistema algo más comportado llamado polimorfismo predicativo ; si la distinción entre programa y tipo se difumina, se obtiene el análogo teórico de tipos de la lógica de orden superior, también conocido como polimorfismo impredicativo . En la literatura se han considerado varias combinaciones de dependencia y polimorfismo, siendo la más famosa el cubo lambda de Henk Barendregt .

La intersección de la lógica y la teoría de tipos es un área de investigación amplia y activa. Las nuevas lógicas suelen formalizarse en un contexto teórico de tipos general, conocido como marco lógico . Los marcos lógicos modernos populares, como el cálculo de construcciones y el LF, se basan en la teoría de tipos dependientes de orden superior, con diversas compensaciones en términos de decidibilidad y poder expresivo. Estos marcos lógicos siempre se especifican como sistemas de deducción natural, lo que da testimonio de la versatilidad del enfoque de la deducción natural.

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Para simplificar, las lógicas presentadas hasta ahora han sido intuicionistas . La lógica clásica extiende la lógica intuicionista con un axioma adicional o principio de tercero excluido :

Para cualquier proposición p, la proposición p ∨ ¬p es verdadera.

Esta afirmación no es, obviamente, ni una introducción ni una eliminación; de hecho, implica dos conectivos distintos. El tratamiento original de Gentzen del tercero excluido prescribía una de las siguientes tres formulaciones (equivalentes), que ya estaban presentes en formas análogas en los sistemas de Hilbert y Heyting :

────────────── XM 1A ∨ ¬A

¬¬Un────────── XM 2A

──────── tú¬Un⋮p
────── XM 3 u, pA

(XM ₃ es simplemente XM ₂ expresado en términos de E.) Este tratamiento del medio excluido, además de ser objetable desde el punto de vista de un purista, introduce complicaciones adicionales en la definición de las formas normales.

Un tratamiento comparativamente más satisfactorio de la deducción natural clásica en términos de reglas de introducción y eliminación solamente fue propuesto por Parigot en 1992 en la forma de un cálculo lambda clásico llamado λμ . La idea clave de su enfoque fue reemplazar un juicio centrado en la verdad A con una noción más clásica, reminiscente del cálculo secuente : en forma localizada, en lugar de Γ ⊢ A , utilizó Γ ⊢ Δ, con Δ una colección de proposiciones similares a Γ. Γ fue tratado como una conjunción, y Δ como una disyunción. Esta estructura se toma esencialmente directamente de los cálculos secuentes clásicos , pero la innovación en λμ fue dar un significado computacional a las pruebas de deducción natural clásica en términos de un mecanismo callcc o throw/catch visto en LISP y sus descendientes. (Véase también: control de primera clase .)

Otra extensión importante fue para las lógicas modales y otras lógicas que necesitan más que el juicio básico de verdad. Estas fueron descritas por primera vez, para las lógicas modales aléticas S4 y S5 , en un estilo de deducción natural por Prawitz en 1965, ^[5] y desde entonces han acumulado una gran cantidad de trabajo relacionado. Para dar un ejemplo simple, la lógica modal S4 requiere un nuevo juicio, " A válido ", que es categórico con respecto a la verdad:

Si "A" (es verdadero) bajo ninguna suposición de que "B" (es verdadero), entonces "A es válido".

Este juicio categórico se internaliza como un conectivo unario ◻ A (léase " necesariamente A ") con las siguientes reglas de introducción y eliminación:

Una válida──────── ◻Yo◻ Un

◻ Un──────── ◻ESA

Obsérvese que la premisa " A válida " no tiene reglas definitorias; en su lugar, se utiliza la definición categórica de validez. Este modo se vuelve más claro en la forma localizada cuando las hipótesis son explícitas. Escribimos "Ω;Γ ⊢ A " donde Γ contiene las hipótesis verdaderas como antes, y Ω contiene las hipótesis válidas. A la derecha hay un solo juicio " A "; la validez no es necesaria aquí ya que "Ω ⊢ A válida " es por definición lo mismo que "Ω;⋅ ⊢ A ". Las formas de introducción y eliminación son entonces:

Ω;⋅ ⊢ π : A──────────────────── ◻YoΩ;⋅ ⊢ caja π : ◻ A

Ω;Γ ⊢ π : ◻ A────────────────────── ◻EΩ;Γ ⊢ desempaquetar π : A

Las hipótesis modales tienen su propia versión de la regla de hipótesis y del teorema de sustitución.

──────────────────────────────── válido-hipΩ, u: (A válido); Γ ⊢ u : A

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Si Ω;⋅ ⊢ π ₁  : A y Ω, u : ( A válida ); Γ ⊢ π ₂  : C , entonces Ω;Γ ⊢ [π ₁ / u ] π ₂  : C .

Este marco de separación de juicios en conjuntos distintos de hipótesis, también conocidos como contextos multizonales o poliádicos , es muy potente y extensible; se ha aplicado a muchas lógicas modales diferentes, y también a lógicas lineales y otras lógicas subestructurales , por dar algunos ejemplos. Sin embargo, relativamente pocos sistemas de lógica modal pueden formalizarse directamente en la deducción natural. Para dar caracterizaciones teóricas de prueba de estos sistemas, se utilizan extensiones como el etiquetado o los sistemas de inferencia profunda.

La adición de etiquetas a las fórmulas permite un control mucho más preciso de las condiciones bajo las cuales se aplican las reglas, lo que permite aplicar las técnicas más flexibles de los cuadros analíticos , como se ha hecho en el caso de la deducción etiquetada. Las etiquetas también permiten nombrar mundos en la semántica de Kripke; Simpson (1993) presenta una técnica influyente para convertir las condiciones marco de las lógicas modales en la semántica de Kripke en reglas de inferencia en una formalización de deducción natural de la lógica híbrida . Stouppa (2004) examina la aplicación de muchas teorías de prueba, como las hipersecuentes de Avron y Pottinger y la lógica de visualización de Belnap a lógicas modales como S5 y B.

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

El cálculo secuencial es la principal alternativa a la deducción natural como fundamento de la lógica matemática . En la deducción natural, el flujo de información es bidireccional: las reglas de eliminación hacen fluir la información hacia abajo por deconstrucción, y las reglas de introducción hacen fluir la información hacia arriba por ensamblaje. Por lo tanto, una prueba de deducción natural no tiene una lectura puramente de abajo hacia arriba o de arriba hacia abajo, lo que la hace inadecuada para la automatización en la búsqueda de pruebas. Para abordar este hecho, Gentzen propuso en 1935 su cálculo secuencial , aunque inicialmente lo concibió como un dispositivo técnico para aclarar la consistencia de la lógica de predicados . Kleene , en su influyente libro de 1952 Introducción a las metamatemáticas , dio la primera formulación del cálculo secuencial en el estilo moderno. ^[25]

En el cálculo consecuente, todas las reglas de inferencia tienen una lectura puramente ascendente. Las reglas de inferencia pueden aplicarse a elementos de ambos lados del torniquete . (Para diferenciarlas de la deducción natural, este artículo utiliza una doble flecha ⇒ en lugar de la flecha derecha ⊢ para los consecuentes). Las reglas de introducción de la deducción natural se consideran reglas derechas en el cálculo consecuente y son estructuralmente muy similares. Las reglas de eliminación, por otro lado, se convierten en reglas izquierdas en el cálculo consecuente. Para dar un ejemplo, considere la disyunción; las reglas derechas son familiares:

Γ ⇒ A───────── ∨R 1Γ ⇒ A ∨ B

Γ ⇒ B───────── ∨R 2Γ ⇒ A ∨ B

A la izquierda:

Γ, u:A ⇒ C Γ, v:B ⇒ C─────────────────────────── ∨LΓ, w: (A ∨ B) ⇒ C

Recordemos la regla ∨E de deducción natural en forma localizada:

Γ ⊢ A ∨ B Γ, u:A ⊢ C Γ, v:B ⊢ C─────────────────────────────────────── ∨EΓ ⊢ C

La proposición A ∨ B , que es la sucedente de una premisa en ∨E, se convierte en una hipótesis de la conclusión en la regla de la izquierda ∨L. Por lo tanto, las reglas de la izquierda pueden verse como una especie de regla de eliminación invertida. Esta observación puede ilustrarse de la siguiente manera:

────── hipnosis | | reglas de eliminacion | ↓ ────────────────────── ↑↓ conocer ↑ | | intro. reglas | conclusión

─────────────────────────── inicio ↑ ↑ | | | reglas de izquierda | reglas de derecha | | conclusión

En el cálculo secuencial, las reglas de izquierda y derecha se ejecutan al unísono hasta llegar al secuencial inicial , que corresponde al punto de encuentro de las reglas de eliminación e introducción en la deducción natural. Estas reglas iniciales son superficialmente similares a la regla de hipótesis de la deducción natural, pero en el cálculo secuencial describen una transposición o un apretón de manos de una proposición izquierda y una derecha:

────────── inicioΓ, u:A ⇒ A

La correspondencia entre el cálculo secuencial y la deducción natural es un par de teoremas de solidez y completitud, ambos demostrables mediante un argumento inductivo.

Solidez de ⇒ con respecto a ⊢

Si Γ ⇒ A , entonces Γ ⊢ A .

Completitud de ⇒ con respecto a ⊢

Si Γ ⊢ A , entonces Γ ⇒ A .

Estos teoremas dejan claro que el cálculo secuencial no cambia la noción de verdad, porque la misma colección de proposiciones sigue siendo verdadera. Por lo tanto, se pueden utilizar los mismos objetos de prueba que antes en las derivaciones del cálculo secuencial. Como ejemplo, consideremos las conjunciones. La regla correcta es prácticamente idéntica a la regla de introducción.

Γ ⇒ π 1  : A Γ ⇒ π 2  : B─────────────────────────── ∧RΓ ⇒ (π 1 , π 2 ) : A ∧ B

Γ ⊢ π 1  : A Γ ⊢ π 2  : B───────────────────────── ∧YoΓ ⊢ (π 1 , π 2 ) : A ∧ B

La regla de la izquierda, sin embargo, realiza algunas sustituciones adicionales que no se realizan en las reglas de eliminación correspondientes.

Γ, u:A ⇒ π : C──────────────────────────────── ∧L 1
Γ, v: (A ∧ B) ⇒ [ fst v/u] π : C

Γ ⊢ π : A ∧ B───────────── ∧E 1
Γ ⊢ primera π : A

Γ, u:B ⇒ π : C─────────────────────────────── ∧L 2
Γ, v: (A ∧ B) ⇒ [ snd v/u ] π : C

Γ ⊢ π : A ∧ B───────────── ∧E 2
Γ ⊢ snd π : B

Por lo tanto, los tipos de pruebas generadas en el cálculo secuencial son bastante diferentes de los de la deducción natural. El cálculo secuencial produce pruebas en lo que se conoce como la forma β-normal η-larga , que corresponde a una representación canónica de la forma normal de la prueba de deducción natural. Si uno intenta describir estas pruebas utilizando la propia deducción natural, se obtiene lo que se llama el cálculo de intercalación (descrito por primera vez por John Byrnes), que puede usarse para definir formalmente la noción de una forma normal para la deducción natural.

El teorema de sustitución de la deducción natural toma la forma de una regla estructural o teorema estructural conocido como corte en el cálculo secuencial.

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Si Γ ⇒ π ₁  : A y Γ, u : A ⇒ π ₂  : C , entonces Γ ⇒ [π ₁ /u] π ₂  : C .

En la mayoría de las lógicas bien comportadas, el corte es innecesario como regla de inferencia, aunque sigue siendo demostrable como un metateorema ; la superfluidad de la regla de corte se presenta generalmente como un proceso computacional, conocido como eliminación de corte . Esto tiene una aplicación interesante para la deducción natural; por lo general, es extremadamente tedioso demostrar ciertas propiedades directamente en la deducción natural debido a un número ilimitado de casos. Por ejemplo, considere mostrar que una proposición dada no es demostrable en la deducción natural. Un argumento inductivo simple falla debido a reglas como ∨E o E que pueden introducir proposiciones arbitrarias. Sin embargo, sabemos que el cálculo consecuente es completo con respecto a la deducción natural, por lo que es suficiente mostrar esta imposibilidad de demostración en el cálculo consecuente. Ahora bien, si el corte no está disponible como regla de inferencia, entonces todas las reglas consecuentes introducen un conectivo a la derecha o a la izquierda, por lo que la profundidad de una derivación consecuente está completamente limitada por los conectivos en la conclusión final. Por lo tanto, demostrar la imposibilidad de demostrar algo es mucho más fácil, porque sólo hay un número finito de casos a considerar, y cada caso está compuesto enteramente de subproposiciones de la conclusión. Un ejemplo sencillo de esto es el teorema de consistencia global : "⋅ ⊢ ⊥" no es demostrable. En la versión del cálculo secuencial, esto es manifiestamente cierto porque no hay ninguna regla que pueda tener "⋅ ⇒ ⊥" como conclusión. Los teóricos de la demostración a menudo prefieren trabajar en formulaciones de cálculo secuencial sin cortes debido a estas propiedades.

• Barker-Plummer, Dave; Barwise, Jon ; Etchemendy, John (2011). Prueba del lenguaje y lógica (2.ª ed.). Publicaciones CSLI. ISBN 978-1575866321.
• Gallier, Jean (2005). "Lógica constructiva. Parte I: Un tutorial sobre sistemas de prueba y cálculos λ tipificados" . Consultado el 12 de junio de 2014 .
• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift . 39 (2): 176–210. doi :10.1007/BF01201353. S2CID  121546341. (Traducción al español de Investigaciones sobre la deducción lógica en M. E. Szabo. Obras completas de Gerhard Gentzen. North-Holland Publishing Company, 1969.)
• Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift . 39 (3): 405–431. doi :10.1007/bf01201363. S2CID  186239837.
• Girard, Jean-Yves (1990). Pruebas y tipos. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, Inglaterra. Archivado desde el original el 4 de julio de 2016. Consultado el 20 de abril de 2006 .Traducido y con apéndices de Paul Taylor e Yves Lafont.
• Jaśkowski, Stanisław (1934). Sobre las reglas de suposiciones en lógica formal .Reimpreso en Lógica polaca 1920–39 , ed. Storrs McCall.
• Kleene, Stephen Cole (1980) [1952]. Introducción a las metamatemáticas (undécima edición). Holanda Septentrional. ISBN 978-0-7204-2103-3.
• Kleene, Stephen Cole (2009) [1952]. Introducción a las metamatemáticas . Ishi Press International. ISBN 978-0-923891-57-2.
• Kleene, Stephen Cole (2002) [1967]. Lógica matemática . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Lógica inicial . Thomas Nelson. ISBN 978-0-17-712040-4.
• Martin-Löf, Per (1996). "Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas" (PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11–60.Apuntes de conferencias de un curso breve en la Università degli Studi di Siena, abril de 1983.
• Pfenning, Frank; Davies, Rowan (2001). "Una reconstrucción crítica de la lógica modal" (PDF) . Estructuras matemáticas en informática . 11 (4): 511–540. CiteSeerX  10.1.1.43.1611 . doi :10.1017/S0960129501003322. S2CID  16467268.
• Prawitz, Dag (1965). Deducción natural: un estudio teórico de prueba . Acta Universitatis Stockholmiensis, Estudios de filosofía de Estocolmo 3. Estocolmo, Göteborg, Uppsala: Almqvist & Wicksell.
• Prawitz, Dag (2006) [1965]. Deducción natural: un estudio teórico de la prueba . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-44655-4.
• Quine, Willard Van Orman (1981) [1940]. Lógica matemática (edición revisada). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-55451-1.
• Quine, Willard Van Orman (1982) [1950]. Métodos de lógica (Cuarta edición). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-57176-1.
• Simpson, Alex (1993). La teoría de la prueba y la semántica de la lógica modal intuicionista (PDF) . Universidad de Edimburgo.Tesis doctoral.
• Stoll, Robert Roth (1979) [1963]. Teoría de conjuntos y lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-63829-4.
• Stouppa, Phiniki (2004). El diseño de teorías de prueba modales: el caso de S5 . Universidad de Dresde. CiteSeerX  10.1.1.140.1858 .Tesis de maestría.
• Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-40687-9.
• Van Dalen, Dirk (2013) [1980]. Lógica y Estructura . Universitext (5 ed.). Londres, Heidelberg, Nueva York, Dordrecht: Springer . doi :10.1007/978-1-4471-4558-5. ISBN 978-1-4471-4558-5.

• Laboreo, Daniel Clemente (agosto de 2004). «Introducción a la deducción natural» (PDF) .
• "Domino On Acid" . Consultado el 10 de diciembre de 2023 . La deducción natural visualizada como un juego de dominó
• Pelletier, Francis Jeffry. "Una historia de la deducción natural y los libros de texto de lógica elemental" (PDF) .
• Entrada de Pelletier, Francis Jeffry; Hazen, Allen, "Sistemas de deducción natural en lógica" en la Stanford Encyclopedia of Philosophy , 29 de octubre de 2021
• Levy, Michel. "Un demostrador proposicional".