Cálculo secuencial

En lógica matemática , el cálculo consecuente es un estilo de argumentación lógica formal en el que cada línea de una prueba es una tautología condicional (llamada consecuente por Gerhard Gentzen ) en lugar de una tautología incondicional. Cada tautología condicional se infiere de otras tautologías condicionales en líneas anteriores en un argumento formal de acuerdo con reglas y procedimientos de inferencia , dando una mejor aproximación al estilo natural de deducción utilizado por los matemáticos que el estilo anterior de lógica formal de David Hilbert , en el que cada línea era una tautología incondicional. Pueden existir distinciones más sutiles; por ejemplo, las proposiciones pueden depender implícitamente de axiomas no lógicos . En ese caso, los consecuentes significan teoremas condicionales de una teoría de primer orden en lugar de tautologías condicionales.

El cálculo secuencial es uno de los varios estilos existentes de cálculo de prueba para expresar argumentos lógicos línea por línea.

• Estilo Hilbert . Toda línea es una tautología (o teorema) incondicional.
• Estilo Gentzen. Cada línea es una tautología condicional (o teorema) con cero o más condiciones a la izquierda.
  • Deducción natural . Toda línea (condicional) tiene exactamente una proposición afirmada a la derecha.
  • Cálculo secuencial. Toda línea (condicional) tiene cero o más proposiciones afirmadas a la derecha.

En otras palabras, los sistemas de deducción natural y cálculo secuencial son tipos particulares y distintos de sistemas de estilo Gentzen. Los sistemas de estilo Hilbert suelen tener una cantidad muy pequeña de reglas de inferencia y se basan más en conjuntos de axiomas. Los sistemas de estilo Gentzen suelen tener muy pocos axiomas, si es que tienen alguno, y se basan más en conjuntos de reglas.

Los sistemas de estilo Gentzen tienen importantes ventajas prácticas y teóricas en comparación con los sistemas de estilo Hilbert. Por ejemplo, tanto los sistemas de deducción natural como los de cálculo secuencial facilitan la eliminación e introducción de cuantificadores universales y existenciales , de modo que las expresiones lógicas no cuantificadas se pueden manipular de acuerdo con las reglas mucho más simples del cálculo proposicional . En un argumento típico, se eliminan los cuantificadores, luego se aplica el cálculo proposicional a las expresiones no cuantificadas (que normalmente contienen variables libres ) y luego se reintroducen los cuantificadores. Esto es muy similar a la forma en que los matemáticos llevan a cabo las demostraciones matemáticas en la práctica. Las demostraciones de cálculo de predicados son generalmente mucho más fáciles de descubrir con este enfoque y, a menudo, son más breves. Los sistemas de deducción natural son más adecuados para la demostración práctica de teoremas. Los sistemas de cálculo secuencial son más adecuados para el análisis teórico.

En teoría de la prueba y lógica matemática , el cálculo secuencial es una familia de sistemas formales que comparten un cierto estilo de inferencia y ciertas propiedades formales. Los primeros sistemas de cálculo secuencial, LK y LJ , fueron introducidos en 1934/1935 por Gerhard Gentzen ^[1] como una herramienta para estudiar la deducción natural en lógica de primer orden (en versiones clásica e intuicionista , respectivamente). El llamado "Teorema principal" ( Hauptsatz ) de Gentzen sobre LK y LJ fue el teorema de eliminación de cortes , ^{[2] [3]} un resultado con consecuencias metateóricas de largo alcance , incluida la consistencia . Gentzen demostró aún más el poder y la flexibilidad de esta técnica unos años más tarde, aplicando un argumento de eliminación de cortes para dar una prueba (transfinita) de la consistencia de la aritmética de Peano , en respuesta sorprendente a los teoremas de incompletitud de Gödel . Desde este trabajo temprano, los cálculos secuenciales, también llamados sistemas de Gentzen , ^{[4] [5] [6] [7]} y los conceptos generales relacionados con ellos, se han aplicado ampliamente en los campos de la teoría de la prueba, la lógica matemática y la deducción automatizada .

Una forma de clasificar los diferentes estilos de sistemas de deducción es observar la forma de los juicios en el sistema, es decir , qué cosas pueden aparecer como conclusión de una (sub)prueba. La forma de juicio más simple se utiliza en los sistemas de deducción de estilo Hilbert , donde un juicio tiene la forma

${\estilo de visualización B}$

donde es cualquier fórmula de lógica de primer orden (o cualquier lógica a la que se aplique el sistema de deducción, p. ej ., cálculo proposicional o una lógica de orden superior o una lógica modal ). Los teoremas son aquellas fórmulas que aparecen como juicio final en una prueba válida. Un sistema de estilo Hilbert no necesita distinción entre fórmulas y juicios; hacemos una aquí únicamente para comparar con los casos que siguen.${\estilo de visualización B}$

El precio que se paga por la sintaxis simple de un sistema de estilo Hilbert es que las demostraciones formales completas tienden a ser extremadamente largas. Los argumentos concretos sobre las demostraciones en un sistema de este tipo casi siempre apelan al teorema de deducción . Esto lleva a la idea de incluir el teorema de deducción como una regla formal en el sistema, lo que sucede en la deducción natural .

En la deducción natural, los juicios tienen la forma

${\displaystyle A_{1},A_{2},\ldots ,A_{n}\vdash B}$

donde las 's y son nuevamente fórmulas y . En otras palabras, un juicio consiste en una lista (posiblemente vacía) de fórmulas en el lado izquierdo de un símbolo de torniquete " ", con una única fórmula en el lado derecho, ^{[8] [9] [10]} (aunque las permutaciones de las 's a menudo son irrelevantes). Los teoremas son aquellas fórmulas tales que (con un lado izquierdo vacío) es la conclusión de una prueba válida. (En algunas presentaciones de la deducción natural, las s y el torniquete no se escriben explícitamente; en su lugar, se utiliza una notación bidimensional de la que se pueden inferir).$Estilo de visualización A_{i}}$${\estilo de visualización B}$${\displaystyle n\geq 0}$${\estilo de visualización \vdash}$$Estilo de visualización A_{i}}$${\estilo de visualización B}$${\displaystyle \vdash B}$$Estilo de visualización A_{i}}$

La semántica estándar de un juicio en la deducción natural es que afirma que siempre que ^[11] , , etc., sean todos verdaderos, también serán verdaderos. Los juicios$Estilo de visualización A_{1}$${\displaystyle A_{2}}$${\displaystyle B}$

${\displaystyle A_{1},\ldots ,A_{n}\vdash B}$

y

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B}$

son equivalentes en el sentido fuerte de que una prueba de cualquiera de ellos puede extenderse a una prueba del otro.

Finalmente, el cálculo secuencial generaliza la forma de un juicio de deducción natural a

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

un objeto sintáctico llamado consecuente. Las fórmulas del lado izquierdo del torniquete se llaman antecedente y las fórmulas del lado derecho se llaman sucedente o consecuente ; juntas se llaman cedentes o consecuentes . ^[12] Nuevamente, y son fórmulas, y y son números enteros no negativos, es decir, el lado izquierdo o el lado derecho (o ninguno o ambos) pueden estar vacíos. Como en la deducción natural, los teoremas son aquellos donde es la conclusión de una prueba válida.${\displaystyle A_{i}}$${\displaystyle B_{i}}$${\displaystyle n}$${\displaystyle k}$${\displaystyle B}$${\displaystyle \vdash B}$

La semántica estándar de un consecuente es una afirmación de que siempre que cada uno sea verdadero, al menos uno también será verdadero. ^[13] Por lo tanto, el consecuente vacío, que tiene ambos cedentes vacíos, es falso. ^[14] Una forma de expresar esto es que una coma a la izquierda del torniquete debe considerarse como un "y", y una coma a la derecha del torniquete debe considerarse como un "o" (inclusivo). Los consecuentes${\displaystyle A_{i}}$ ${\displaystyle B_{i}}$

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}}$

y

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})}$

son equivalentes en el sentido fuerte de que una prueba de cualquiera de los consecuentes puede extenderse a una prueba del otro consecuente.

A primera vista, esta extensión de la forma del juicio puede parecer una complicación extraña: no está motivada por una deficiencia obvia de la deducción natural y, al principio, resulta confuso que la coma parezca significar cosas completamente diferentes en los dos lados del torniquete. Sin embargo, en un contexto clásico , la semántica del consecuente también puede expresarse (por tautología proposicional) como

${\displaystyle \vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}}$

(al menos una de las A es falsa, o una de las B es verdadera)

o como

${\displaystyle \vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})}$

(no puede ser el caso que todas las A sean verdaderas y todas las B sean falsas).

En estas formulaciones, la única diferencia entre las fórmulas de ambos lados del torniquete es que se niega uno de los lados. Por lo tanto, cambiar la izquierda por la derecha en un consecuente corresponde a negar todas las fórmulas constituyentes. Esto significa que una simetría como las leyes de De Morgan , que se manifiesta como una negación lógica en el nivel semántico, se traduce directamente en una simetría izquierda-derecha de los consecuentes y, de hecho, las reglas de inferencia en el cálculo de consecuentes para tratar la conjunción (∧) son imágenes especulares de las que tratan la disyunción (∨).

Muchos lógicos creen ^{[ cita requerida ]} que esta presentación simétrica ofrece una visión más profunda de la estructura de la lógica que otros estilos de sistemas de prueba, donde la dualidad clásica de la negación no es tan evidente en las reglas.

Gentzen afirmó una clara distinción entre sus sistemas de deducción natural de salida única (NK y NJ) y sus sistemas de cálculo secuencial de salida múltiple (LK y LJ). Escribió que el sistema de deducción natural intuicionista NJ era algo feo. ^[15] Dijo que el papel especial del tercero excluido en el sistema clásico de deducción natural NK se elimina en el sistema clásico de cálculo secuencial LK. ^[16] Dijo que el cálculo secuencial LJ dio más simetría que la deducción natural NJ en el caso de la lógica intuicionista, como también en el caso de la lógica clásica (LK versus NK). ^[17] Luego dijo que además de estas razones, el cálculo secuencial con múltiples fórmulas sucedentes está destinado particularmente a su teorema principal ("Hauptsatz"). ^[18]

La palabra "sequent" proviene de la palabra "Sequenz" que aparece en el artículo de Gentzen de 1934. ^[1] Kleene hace el siguiente comentario sobre la traducción al inglés: "Gentzen dice 'Sequenz', que nosotros traducimos como 'sequent', porque ya hemos usado 'sequence' para cualquier sucesión de objetos, donde la palabra alemana es 'Folge'". ^[19]

El cálculo secuencial puede considerarse una herramienta para demostrar fórmulas en lógica proposicional , similar al método de tablas analíticas . Proporciona una serie de pasos que permiten reducir el problema de demostrar una fórmula lógica a fórmulas cada vez más simples hasta llegar a fórmulas triviales. ^[20]

Considere la siguiente fórmula:

${\displaystyle ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

Esto se escribe de la siguiente forma, donde la proposición que necesita demostrarse está a la derecha del símbolo del torniquete :${\displaystyle \vdash }$

${\displaystyle \vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

Ahora bien, en lugar de probar esto a partir de los axiomas, basta suponer la premisa de la implicación y luego tratar de probar su conclusión. ^[21] De aquí se pasa a la siguiente sucesión:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r}$

Nuevamente el lado derecho incluye una implicación, cuya premisa puede asumirse además, de modo que solo es necesario probar su conclusión:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r}$

Dado que se supone que los argumentos del lado izquierdo están relacionados por la conjunción , esto se puede reemplazar por lo siguiente:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r}$

Esto equivale a probar la conclusión en ambos casos de la disyunción en el primer argumento de la izquierda. Por lo tanto, podemos dividir el consecuente en dos, donde ahora tenemos que probar cada uno por separado:

${\displaystyle p\rightarrow r,p,q\vdash r}$

${\displaystyle q\rightarrow r,p,q\vdash r}$

En el caso del primer juicio, reescribimos como y dividimos nuevamente el secuencial para obtener:${\displaystyle p\rightarrow r}$${\displaystyle \lnot p\lor r}$

${\displaystyle \lnot p,p,q\vdash r}$

${\displaystyle r,p,q\vdash r}$

El segundo secuenciador está hecho; el primer secuenciador se puede simplificar aún más:

${\displaystyle p,q\vdash p,r}$

Este proceso puede continuar hasta que solo haya fórmulas atómicas en cada lado. El proceso puede describirse gráficamente mediante un árbol con raíces , como se muestra a la derecha. La raíz del árbol es la fórmula que deseamos demostrar; las hojas consisten solo en fórmulas atómicas. El árbol se conoce como árbol de reducción . ^{[20] [22]}

Los elementos situados a la izquierda del torniquete se entienden conectados por conjunción, y los situados a la derecha por disyunción. Por lo tanto, cuando ambos consisten únicamente en símbolos atómicos, el consecuente se acepta axiomáticamente (y siempre es verdadero) si y solo si al menos uno de los símbolos de la derecha también aparece a la izquierda.

A continuación se presentan las reglas por las que se avanza a lo largo del árbol. Siempre que un consecuente se divide en dos, el vértice del árbol tiene dos vértices secundarios y el árbol se ramifica. Además, se puede cambiar libremente el orden de los argumentos en cada lado; Γ y Δ representan posibles argumentos adicionales. ^[20]

El término habitual para la línea horizontal utilizada en los diseños de estilo Gentzen para la deducción natural es línea de inferencia . ^[23]

Izquierda	Bien
${\displaystyle L\land {\text{rule: }}\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}}$	${\displaystyle R\land {\text{rule: }}{\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}}$
${\displaystyle L\lor {\text{rule: }}{\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\lor {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}}$
${\displaystyle L\rightarrow {\text{rule: }}{\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\rightarrow {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}}$
${\displaystyle L\lnot {\text{rule: }}\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}}$	${\displaystyle R\lnot {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}}$
Axioma: ${\displaystyle \Gamma ,A\vdash \Delta ,A}$

A partir de cualquier fórmula de lógica proposicional, mediante una serie de pasos, se puede procesar el lado derecho del torniquete hasta que incluya solo símbolos atómicos. Luego, se hace lo mismo con el lado izquierdo. Dado que cada operador lógico aparece en una de las reglas anteriores y es eliminado por la regla, el proceso termina cuando no quedan operadores lógicos: La fórmula ha sido descompuesta .

Así, las secuencias de las hojas de los árboles incluyen sólo símbolos atómicos, que son demostrables mediante el axioma o no, dependiendo de si uno de los símbolos de la derecha también aparece en el de la izquierda.

Es fácil ver que los pasos del árbol preservan el valor de verdad semántico de las fórmulas implicadas en ellos, y que se entiende que existe conjunción entre las diferentes ramas del árbol cuando hay una división. También es obvio que un axioma es demostrable si y sólo si es verdadero para cada asignación de valores de verdad a los símbolos atómicos. Por lo tanto, este sistema es sólido y completo para la lógica proposicional clásica.

El cálculo secuencial está relacionado con otras axiomatizaciones del cálculo proposicional clásico, como el cálculo proposicional de Frege o la axiomatización de Jan Łukasiewicz (que en sí misma forma parte del sistema estándar de Hilbert ): Cada fórmula que se puede demostrar en estas tiene un árbol de reducción. Esto se puede mostrar de la siguiente manera: Cada prueba en el cálculo proposicional utiliza solo axiomas y reglas de inferencia. Cada uso de un esquema axiomático produce una fórmula lógica verdadera y, por lo tanto, se puede demostrar en el cálculo secuencial; a continuación se muestran ejemplos de estos. La única regla de inferencia en los sistemas mencionados anteriormente es el modus ponens , que se implementa mediante la regla de corte.

Esta sección presenta las reglas del cálculo secuencial LK (que significa Logistische Kalkül) introducidas por Gentzen en 1934. ^[24] Una prueba (formal) en este cálculo es una secuencia finita de secuencias, donde cada una de las secuencias es derivable de secuencias que aparecen antes en la secuencia usando una de las reglas siguientes.

Se utilizará la siguiente notación:

• ${\displaystyle \vdash }$Conocido como el torniquete , separa las suposiciones de la izquierda de las proposiciones de la derecha.
• ${\displaystyle A}$y denotan fórmulas de lógica de predicados de primer orden (también se puede restringir esto a la lógica proposicional),${\displaystyle B}$
• ${\displaystyle \Gamma ,\Delta ,\Sigma }$, y son secuencias finitas (posiblemente vacías) de fórmulas (de hecho, el orden de las fórmulas no importa; ver § Reglas estructurales), llamadas contextos,${\displaystyle \Pi }$
  • Cuando está a la izquierda de , la secuencia de fórmulas se considera de forma conjuntiva (se supone que todas se cumplen al mismo tiempo),${\displaystyle \vdash }$
  • mientras que a la derecha de , la secuencia de fórmulas se considera disyuntivamente (al menos una de las fórmulas debe cumplirse para cualquier asignación de variables),${\displaystyle \vdash }$
• ${\displaystyle t}$denota un término arbitrario,
• ${\displaystyle x}$y denotar variables.${\displaystyle y}$
• Se dice que una variable ocurre libre dentro de una fórmula si no está limitada por cuantificadores o .${\displaystyle \forall }$${\displaystyle \exists }$
• ${\displaystyle A[t/x]}$denota la fórmula que se obtiene al sustituir el término por cada ocurrencia libre de la variable en fórmula con la restricción de que el término debe ser libre para la variable en (es decir, ninguna ocurrencia de ninguna variable en queda limitada en ).${\displaystyle t}$${\displaystyle x}$${\displaystyle A}$${\displaystyle t}$${\displaystyle x}$${\displaystyle A}$${\displaystyle t}$${\displaystyle A[t/x]}$
• ${\displaystyle WL}$, , , , , : Estos seis representan las dos versiones de cada una de las tres reglas estructurales; una para usar a la izquierda ('L') de un , y la otra a su derecha ('R'). Las reglas se abrevian 'W' para debilitamiento (izquierda/derecha) , 'C' para contracción y 'P' para permutación .${\displaystyle WR}$${\displaystyle CL}$${\displaystyle CR}$${\displaystyle PL}$${\displaystyle PR}$${\displaystyle \vdash }$

Obsérvese que, a diferencia de las reglas para avanzar a lo largo del árbol de reducción presentadas anteriormente, las siguientes reglas sirven para avanzar en direcciones opuestas, de axiomas a teoremas. Por lo tanto, son imágenes especulares exactas de las reglas anteriores, excepto que aquí no se supone implícitamente la simetría y se añaden reglas relativas a la cuantificación .

Axioma	Cortar
${\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})}$

Reglas lógicas de izquierda	Reglas lógicas correctas
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})}$
${\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})}$	${\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})}$
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}\quad ({\lor }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma \vdash B,\Delta }{\Gamma \vdash A\land B,\Delta }}\quad ({\land }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)}$
${\displaystyle {\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)}$
${\displaystyle {\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)}$

Reglas estructurales de izquierda	Reglas estructurales correctas
${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})}$
${\displaystyle {\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})}$	${\displaystyle {\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})}$
${\displaystyle {\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})}$

Restricciones: En las reglas y , la variable no debe aparecer libre en ningún lugar de los respectivos secuenciales inferiores.${\displaystyle ({\forall }R)}$${\displaystyle ({\exists }L)}$${\displaystyle y}$

Las reglas anteriores se pueden dividir en dos grandes grupos: reglas lógicas y reglas estructurales . Cada una de las reglas lógicas introduce una nueva fórmula lógica ya sea a la izquierda o a la derecha del torniquete . Por el contrario, las reglas estructurales operan sobre la estructura de los consecuentes, ignorando la forma exacta de las fórmulas. Las dos excepciones a este esquema general son el axioma de identidad (I) y la regla de (Corte).${\displaystyle \vdash }$

Aunque se enuncia de forma formal, las reglas anteriores permiten una lectura muy intuitiva en términos de lógica clásica. Consideremos, por ejemplo, la regla . Dice que, siempre que se pueda probar que se puede concluir a partir de alguna secuencia de fórmulas que contienen , entonces también se puede concluir a partir del supuesto (más fuerte) que se cumple. Del mismo modo, la regla establece que, si y son suficientes para concluir , entonces a partir de solo uno todavía se puede concluir o debe ser falso, es decir, se cumple. Todas las reglas se pueden interpretar de esta manera.${\displaystyle ({\land }L_{1})}$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle \Delta }$${\displaystyle A\land B}$${\displaystyle ({\neg }R)}$${\displaystyle \Gamma }$${\displaystyle A}$${\displaystyle \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle {\neg }A}$

Para tener una idea intuitiva de las reglas de cuantificación, considere la regla . Por supuesto, concluir que se cumple solo por el hecho de que es verdadera no es posible en general. Sin embargo, si la variable y no se menciona en otra parte (es decir, todavía se puede elegir libremente, sin influir en las otras fórmulas), entonces se puede suponer que se cumple para cualquier valor de y. Las otras reglas deberían ser bastante sencillas.${\displaystyle ({\forall }R)}$${\displaystyle \forall {x}A}$${\displaystyle A[y/x]}$${\displaystyle A[y/x]}$

En lugar de ver las reglas como descripciones de derivaciones legales en lógica de predicados, también se las puede considerar como instrucciones para la construcción de una prueba para un enunciado dado. En este caso, las reglas se pueden leer de abajo a arriba; por ejemplo, dice que, para probar que se sigue de los supuestos y , basta con probar que se puede concluir de y se puede concluir de , respectivamente. Nótese que, dado algún antecedente, no está claro cómo se debe dividir en y . Sin embargo, solo hay un número finito de posibilidades para verificar ya que el antecedente por supuesto es finito. Esto también ilustra cómo la teoría de la prueba puede verse como operando sobre las pruebas de manera combinatoria: dadas pruebas para y , se puede construir una prueba para .${\displaystyle ({\land }R)}$${\displaystyle A\land B}$${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle A}$${\displaystyle \Gamma }$${\displaystyle B}$${\displaystyle \Sigma }$${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\land B}$

Cuando se busca una prueba, la mayoría de las reglas ofrecen recetas más o menos directas de cómo hacerlo. La regla de corte es diferente: establece que, cuando se puede concluir una fórmula y esta fórmula también puede servir como premisa para concluir otras afirmaciones, entonces se puede "cortar" la fórmula y unir las derivaciones respectivas. Al construir una prueba de abajo a arriba, esto crea el problema de adivinar (ya que no aparece en absoluto a continuación). El teorema de eliminación de corte es, por lo tanto, crucial para las aplicaciones del cálculo de secuencias en la deducción automática : establece que todos los usos de la regla de corte se pueden eliminar de una prueba, lo que implica que a cualquier secuencia demostrable se le puede dar una prueba sin cortes .${\displaystyle A}$${\displaystyle A}$${\displaystyle A}$

La segunda regla, que es un tanto especial, es el axioma de identidad (I). La lectura intuitiva de este axioma es obvia: toda fórmula se prueba a sí misma. Al igual que la regla de corte, el axioma de identidad es un tanto redundante: la completitud de los consecuentes iniciales atómicos establece que la regla puede restringirse a las fórmulas atómicas sin ninguna pérdida de demostrabilidad.

Obsérvese que todas las reglas tienen sus correspondientes pares espejo, excepto las de implicación. Esto refleja el hecho de que el lenguaje habitual de la lógica de primer orden no incluye el conectivo "no está implícito por", que sería el dual de implicación de De Morgan. Añadir un conectivo de este tipo a sus reglas naturales haría que el cálculo fuera completamente simétrico de izquierda a derecha.${\displaystyle \not \leftarrow }$

De aquí la derivación de " ", conocida como Ley del tercero excluido ( tertium non datur en latín).${\displaystyle \vdash A\lor \lnot A}$

		${\displaystyle (I)}$
${\displaystyle A\vdash A}$
		${\displaystyle (\lnot R)}$
${\displaystyle \vdash \lnot A,A}$
		${\displaystyle (\lor R_{2})}$
${\displaystyle \vdash A\lor \lnot A,A}$
		${\displaystyle (PR)}$
${\displaystyle \vdash A,A\lor \lnot A}$
		${\displaystyle (\lor R_{1})}$
${\displaystyle \vdash A\lor \lnot A,A\lor \lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \vdash A\lor \lnot A}$

A continuación se presenta la prueba de un hecho simple que involucra cuantificadores. Nótese que el recíproco no es cierto y su falsedad se puede ver al intentar derivarlo de abajo hacia arriba, porque una variable libre existente no se puede usar en sustitución en las reglas y .${\displaystyle (\forall R)}$${\displaystyle (\exists L)}$

		${\displaystyle (I)}$
${\displaystyle p(x,y)\vdash p(x,y)}$
		${\displaystyle (\forall L)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash p(x,y)}$
		${\displaystyle (\exists R)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\exists L)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\forall R)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)}$

Para algo más interesante, probaremos . Es fácil encontrar la derivación, lo que ejemplifica la utilidad de LK en la demostración automatizada.${\displaystyle {\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}}$

${\displaystyle (I)}$ ${\displaystyle A\vdash A}$     ${\displaystyle (\lnot R)}$ ${\displaystyle \vdash \lnot A,A}$     ${\displaystyle (PR)}$ ${\displaystyle \vdash A,\lnot A}$            ${\displaystyle (I)}$ ${\displaystyle B\vdash B}$     ${\displaystyle (WR)}$ ${\displaystyle B\vdash B,C}$            ${\displaystyle (I)}$ ${\displaystyle C\vdash C}$     ${\displaystyle (WR)}$ ${\displaystyle C\vdash B,C}$         ${\displaystyle (\lor L)}$ ${\displaystyle B\lor C\vdash B,C}$     ${\displaystyle (PR)}$ ${\displaystyle B\lor C\vdash C,B}$     ${\displaystyle (\lnot L)}$ ${\displaystyle B\lor C,\lnot C\vdash B}$              ${\displaystyle (I)}$ ${\displaystyle \lnot A\vdash \lnot A}$         ${\displaystyle (\rightarrow L)}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A}$     ${\displaystyle (\land L_{1})}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A}$     ${\displaystyle (\land L_{2})}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (CL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A}$		${\displaystyle (\rightarrow L)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A}$
		${\displaystyle (PL)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$

Estas derivaciones también enfatizan la estructura estrictamente formal del cálculo consecuente. Por ejemplo, las reglas lógicas definidas anteriormente siempre actúan sobre una fórmula inmediatamente adyacente al torniquete, de modo que las reglas de permutación son necesarias. Nótese, sin embargo, que esto es en parte un artefacto de la presentación, en el estilo original de Gentzen. Una simplificación común implica el uso de conjuntos múltiples de fórmulas en la interpretación del consecuente, en lugar de secuencias, eliminando la necesidad de una regla de permutación explícita. Esto corresponde a cambiar la conmutatividad de los supuestos y las derivaciones fuera del cálculo consecuente, mientras que LK la incorpora dentro del propio sistema.

Para ciertas formulaciones (es decir, variantes) del cálculo secuencial, una prueba en dicho cálculo es isomorfa a una tabla analítica cerrada e invertida . ^[25]

Las reglas estructurales merecen una discusión adicional.

El debilitamiento (W) permite la adición de elementos arbitrarios a una secuencia. Intuitivamente, esto está permitido en el antecedente porque siempre podemos restringir el alcance de nuestra prueba (si todos los autos tienen ruedas, entonces es seguro decir que todos los autos negros tienen ruedas); y en el sucedente porque siempre podemos permitir conclusiones alternativas (si todos los autos tienen ruedas, entonces es seguro decir que todos los autos tienen ruedas o alas).

La contracción (C) y la permutación (P) aseguran que no importe ni el orden (P) ni la multiplicidad de ocurrencias (C) de los elementos de las secuencias. Por lo tanto, en lugar de secuencias, también se podrían considerar conjuntos .

Sin embargo, el esfuerzo adicional que supone utilizar secuencias está justificado, ya que se pueden omitir parte o la totalidad de las reglas estructurales, obteniéndose así las denominadas lógicas subestructurales .

Se puede demostrar que este sistema de reglas es sólido y completo con respecto a la lógica de primer orden, es decir, un enunciado se sigue semánticamente de un conjunto de premisas si y sólo si el consecuente puede derivarse mediante las reglas anteriores. ^[26]${\displaystyle A}$${\displaystyle \Gamma }$ ${\displaystyle (\Gamma \vDash A)}$ ${\displaystyle \Gamma \vdash A}$

En el cálculo de sucesiones, la regla de corte es admisible . Este resultado también se conoce como Hauptsatz de Gentzen ("Teorema principal"). ^{[2] [3]}

Las reglas anteriores se pueden modificar de varias maneras:

Existe cierta libertad de elección respecto de los detalles técnicos de cómo se formalizan los secuentes y las reglas estructurales sin cambiar los secuentes que deriva el sistema.

En primer lugar, como se mencionó anteriormente, los secuenciales pueden considerarse conjuntos o multiconjuntos . En este caso, las reglas para permutar y (cuando se utilizan conjuntos) las fórmulas de contracción son innecesarias.

La regla de debilitamiento se vuelve admisible si se modifica el axioma (I) para derivar cualquier consecuente de la forma . Cualquier debilitamiento que aparezca en una derivación puede entonces trasladarse al principio de la demostración. Este puede ser un cambio conveniente cuando se construyen demostraciones de abajo hacia arriba.${\displaystyle \Gamma ,A\vdash A,\Delta }$

También se puede cambiar si las reglas con más de una premisa comparten el mismo contexto para cada una de esas premisas o dividen sus contextos entre ellas: por ejemplo, pueden formularse como${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.}$

La contracción y el debilitamiento hacen que esta versión de la regla sea interderivable con la versión anterior, aunque en su ausencia, como en la lógica lineal , estas reglas definen conectivos diferentes.

Se puede introducir , la constante de absurdo que representa lo falso , con el axioma:${\displaystyle \bot }$

${\displaystyle {\cfrac {}{\bot \vdash \quad }}}$

O si, como se ha descrito anteriormente, el debilitamiento ha de ser una regla admisible, entonces con el axioma:

${\displaystyle {\cfrac {}{\Gamma ,\bot \vdash \Delta }}}$

Con , la negación puede subsumirse como un caso especial de implicación, a través de la definición .${\displaystyle \bot }$${\displaystyle (\neg A)\iff (A\to \bot )}$

Alternativamente, se puede restringir o prohibir el uso de algunas de las reglas estructurales. Esto produce una variedad de sistemas de lógica subestructural . Por lo general, son más débiles que la lógica de primer orden ( es decir , tienen menos teoremas) y, por lo tanto, no son completos con respecto a la semántica estándar de la lógica de primer orden. Sin embargo, tienen otras propiedades interesantes que han dado lugar a aplicaciones en la informática teórica y la inteligencia artificial .

Sorprendentemente, algunos pequeños cambios en las reglas de LK son suficientes para convertirla en un sistema de prueba para la lógica intuicionista . ^[27] Para ello, hay que restringir a los consecuentes con como máximo una fórmula en el lado derecho, ^[28] y modificar las reglas para mantener esta invariancia. Por ejemplo, se reformula de la siguiente manera (donde C es una fórmula arbitraria):${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,A\lor B\vdash C}}\quad ({\lor }L)}$

El sistema resultante se llama LJ. Es sólido y completo con respecto a la lógica intuicionista y admite una prueba de eliminación de cortes similar. Esto se puede utilizar para demostrar las propiedades de disyunción y existencia .

De hecho, las únicas reglas en LK que necesitan restringirse a consecuentes de fórmula única son , (que puede verse como un caso especial de , como se describió anteriormente) y . Cuando los consecuentes de fórmulas múltiples se interpretan como disyunciones, todas las demás reglas de inferencia de LK son derivables en LJ, mientras que las reglas y se convierten en${\displaystyle ({\to }R)}$${\displaystyle (\neg R)}$${\displaystyle {\to }R}$${\displaystyle ({\forall }R)}$${\displaystyle ({\to }R)}$${\displaystyle ({\forall }R)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}}$

y (cuando no aparece libre en el secuente inferior)${\displaystyle y}$

${\displaystyle {\cfrac {\Gamma \vdash A[y/x]\lor C}{\Gamma \vdash (\forall xA)\lor C}}.}$

Estas reglas no son intuitivamente válidas.

• Cálculo circular
• Cálculo secuencial anidado
• Resolución (lógica)
• Teoría de la prueba

• Buss, Samuel R. (1998). "Introducción a la teoría de la prueba". En Samuel R. Buss (ed.). Manual de teoría de la prueba. Elsevier. págs. 1–78. ISBN 0-444-89840-9.
• Curry, Haskell Brooks (1977) [1963]. Fundamentos de lógica matemática . Nueva York: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift . 39 (2): 176–210. doi :10.1007/BF01201353. S2CID  121546341.
• 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 ; Paul Taylor; Yves Lafont (1990) [1989]. Pruebas y tipos . Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7). ISBN 0-521-37181-3.
• Hilbert, David ; Bernays, Paul (1970) [1939]. Grundlagen der Mathematik II (Segunda ed.). Berlín, Nueva York: Springer-Verlag. ISBN 978-3-642-86897-9.
• 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 0-17-712040-1.
• Mancosu, Paolo; Galvan, Sergio; Zach, Richard (2021). Introducción a la teoría de la demostración: normalización, eliminación de cortes y demostraciones de consistencia . Oxford University Press . pág. 431. ISBN. 978-0-19-289593-6.
• Smullyan, Raymond Merrill (1995) [1968]. Lógica de primer orden . Nueva York: Dover Publications. ISBN 978-0-486-68370-6.
• Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-40687-9.

• Teoría de la demostración (cálculos secuenciales) en la Enciclopedia de filosofía de Stanford
• "Cálculo secuencial", Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
• Una breve distracción: cálculo secuencial
• Tutorial interactivo del cálculo secuencial