Cálculo de secuencias

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 la 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

${\displaystyle B}$

dónde${\displaystyle B}$es cualquier fórmula de lógica de primer orden (o cualquier lógica a la que se aplique el sistema deductivo, por ejemplo , cálculo proposicional, lógica de orden superior o lógica modal ). Los teoremas son aquellas fórmulas que aparecen como juicio final en una demostración válida. Un sistema de estilo Hilbert no necesita distinguir entre fórmulas y juicios; aquí hacemos esta distinción únicamente para compararla con los casos que siguen.

El precio que se paga por la sintaxis simple de un sistema de 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 recurren 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 cual ocurre 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 el${\displaystyle A_{i}}$'arena${\displaystyle B}$son nuevamente fórmulas y${\displaystyle n\geq 0}$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 .${\displaystyle \vdash }$", con una sola fórmula en el lado derecho, ^{[ 8 ] [ 9 ] [ 10 ]} (aunque permutaciones de la${\displaystyle A_{i}}$(los son a menudo inmateriales). Los teoremas son esas fórmulas${\displaystyle B}$de tal manera que${\displaystyle \vdash B}$(con un lado izquierdo vacío) es la conclusión de una prueba válida. (En algunas presentaciones de la deducción natural, la${\displaystyle A_{i}}$La letra s y el torniquete no se describen explícitamente; en su lugar, se utiliza una notación bidimensional a partir de la cual se pueden inferir.

La semántica estándar de un juicio en la deducción natural es que afirma que siempre que ^{[ 11 ]}${\displaystyle A_{1}}$,${\displaystyle A_{2}}$, etc., son todas ciertas,${\displaystyle B}$También será cierto. Los juicios

${\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 estricto de que una demostración de cualquiera de ellas puede extenderse a una demostración de la otra.

Finalmente, el cálculo de secuencias 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 secuente. Las fórmulas del lado izquierdo del torniquete se llaman antecedente , y las fórmulas del lado derecho se llaman consecuente ; juntas se llaman fórmulas cedentes o secuentes . ^{[ 12 ]} Nuevamente,${\displaystyle A_{i}}$y${\displaystyle B_{i}}$son fórmulas y${\displaystyle n}$y${\displaystyle k}$son 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${\displaystyle B}$dónde${\displaystyle \vdash B}$es la conclusión de una prueba válida.

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

${\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 estricto de que una demostración de cualquiera de los secuentes puede extenderse a una demostración del otro secuente.

A primera vista, esta extensión de la forma de juicio puede parecer una complicación extraña; no está motivada por una deficiencia obvia de la deducción natural, y resulta inicialmente confuso que la coma parezca significar cosas completamente diferentes a ambos lados del torniquete. Sin embargo, en un contexto clásico , la semántica del secuente también puede (por tautología proposicional) expresarse 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 que todas las A sean verdaderas y todas las B sean falsas).

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

Muchos lógicos consideran que esta presentación simétrica ofrece una comprensió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. ^{[ 15 ] [ 16 ]}

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 de secuentes de salida múltiple (LK y LJ). Escribió que el sistema de deducción natural intuicionista NJ era algo feo. ^{[ 17 ]} Dijo que el papel especial del tercero excluido en el sistema de deducción natural clásico NK se elimina en el sistema de cálculo de secuentes clásico LK. ^{[ 18 ]} Dijo que el cálculo de secuentes LJ proporcionaba 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 frente a NK). ^{[ 19 ]} Luego dijo que, además de estas razones, el cálculo de secuentes con fórmulas de múltiples sucesores está destinado particularmente a su teorema principal ("Hauptsatz"). ^{[ 20 ]}

La palabra «secuente» se toma de la palabra «Sequenz» 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 traducimos como "secuente", porque ya hemos usado "secuencia" para cualquier sucesión de objetos, donde el alemán es "Folge"». ^{[ 21 ]}

Gentzen utilizó mayúsculas de dos letras para representar diversos sistemas de demostración. En su artículo de 1935, afirmó que en LK , la L significaba "logische" (lógico) y la K significaba "klassische Pradikatenlogik" ("lógica predicativa clásica"). La J en LJ significaba "intuitionistische Pradikatenlogik" ("lógica predicativa intuicionista"). ^{[ 1 ] : 177} De manera similar, la N en NK y NJ significaba "natürlichen Schließens" ("deducción natural"). No está claro cómo llegó a usar la J para representar "intuitionistische", pero presumiblemente para distinguirla tipográficamente del numeral 1 y del número romano I. En otros lugares, Gentzen usó LI y NI en lugar de LJ y NJ . ^{[ 22 ] : 83}

El cálculo de secuencias puede considerarse una herramienta para demostrar fórmulas en lógica proposicional , similar al método de los tableaux analíticos . 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. ^{[ 23 ]}

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 se debe probar 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, en lugar de probar esto a partir de los axiomas, basta con asumir la premisa de la implicación y luego intentar probar su conclusión. ^{[ 24 ]} Por lo tanto, se pasa al siguiente secuente:

${\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 de manera que solo sea necesario demostrar 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 conjunción , esto se puede reemplazar por lo siguiente:

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

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

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

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

En el caso de la primera sentencia, reescribimos${\displaystyle p\rightarrow r}$como${\displaystyle \lnot p\lor r}$y divide la secuencia nuevamente para obtener:

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

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

La segunda secuencia está hecha; la primera secuencia se puede simplificar aún más en:

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

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

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

A continuación se describen las reglas para recorrer el árbol. Cuando una secuencia se divide en dos, el vértice del árbol tiene dos vértices hijos y el árbol se ramifica. Además, se puede cambiar libremente el orden de los argumentos en cada lado; Γ y Δ representan posibles argumentos adicionales. ^{[ 23 ]}

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 . ^{[ 26 ]}

Partiendo de cualquier fórmula en lógica proposicional, mediante una serie de pasos, se puede procesar el lado derecho del torniquete hasta que solo contenga símbolos atómicos. A continuación, se repite el mismo procedimiento para el lado izquierdo. Dado que cada operador lógico aparece en una de las reglas anteriores y es eliminado por dicha regla, el proceso finaliza cuando no quedan operadores lógicos: la fórmula ha sido descompuesta .

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

Es fácil observar que los pasos del árbol conservan el valor de verdad semántico de las fórmulas que implican, entendiendo la conjunción entre las distintas ramas del árbol siempre que haya una bifurcación. También es evidente que un axioma es demostrable si y solo si es verdadero para cualquier 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 de secuencias 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 forma parte del sistema de Hilbert estándar ): Cada fórmula que puede demostrarse en estos tiene un árbol de reducción. Esto puede mostrarse de la siguiente manera: Cada demostración en cálculo proposicional utiliza solo axiomas y las reglas de inferencia. Cada uso de un esquema axiomático produce una fórmula lógica verdadera y, por lo tanto, puede demostrarse en cálculo de secuencias; ejemplos de estos se muestran a continuación . La única regla de inferencia en los sistemas mencionados anteriormente es el modus ponens , que se implementa mediante la regla de corte .

Se utilizará la siguiente notación:

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

Cabe señalar que, a diferencia de las reglas para avanzar a lo largo del árbol de reducción presentado anteriormente, las siguientes reglas se aplican en sentido contrario, desde los axiomas hasta los teoremas. Por lo tanto, son imágenes especulares exactas de las reglas anteriores, con la salvedad de que aquí no se asume implícitamente la simetría y se añaden reglas relativas a la cuantificación .

En la tabla siguiente,${\displaystyle A\setminus B}$denota el complemento relativo de${\displaystyle B}$en${\displaystyle A}$.

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

Las reglas anteriores se pueden dividir en dos grupos principales: lógicas y 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.${\displaystyle \vdash }$En cambio, las reglas estructurales operan sobre la estructura de las secuencias, 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).

Aunque se enuncian de forma formal, las reglas anteriores permiten una lectura muy intuitiva en términos de lógica clásica. Consideremos, por ejemplo, la regla${\displaystyle ({\land }L_{1})}$. Dice que, siempre que uno pueda demostrar que${\displaystyle \Delta }$se puede concluir a partir de alguna secuencia de fórmulas que contienen${\displaystyle A}$, entonces también se puede concluir${\displaystyle \Delta }$a partir del supuesto (más fuerte) de que${\displaystyle A\land B}$Se mantiene. Asimismo, la regla${\displaystyle ({\neg }R)}$establece que, si${\displaystyle \Gamma }$y${\displaystyle A}$basta con concluir${\displaystyle \Delta }$, luego de${\displaystyle \Gamma }$solo uno puede aún concluir${\displaystyle \Delta }$o que${\displaystyle A}$debe ser falso, es decir${\displaystyle {\neg }A}$Se sostiene. Todas las reglas pueden interpretarse de esta manera.

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

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

Al buscar alguna 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 una fórmula${\displaystyle A}$Se puede concluir que esta fórmula también puede servir como premisa para concluir otras afirmaciones, entonces la fórmula${\displaystyle A}$se pueden "recortar" y se unen las derivaciones respectivas. Al construir una demostración de abajo hacia arriba, esto crea el problema de adivinar.${\displaystyle A}$(ya que no aparece en absoluto más abajo). El teorema de eliminación de cortes es, por lo tanto, crucial para las aplicaciones del cálculo de secuentes en la deducción automatizada : establece que todos los usos de la regla de corte pueden eliminarse de una demostración, lo que implica que cualquier secuente demostrable puede tener una demostración sin cortes .

La segunda regla, que resulta algo especial, es el axioma de identidad (I). Su interpretación intuitiva es obvia: toda fórmula se demuestra a sí misma. Al igual que la regla de corte, el axioma de identidad es algo redundante: la completitud de las secuencias iniciales atómicas establece que la regla puede restringirse a fórmulas atómicas sin que ello afecte a su demostrabilidad.

Obsérvese que, si ignoramos el conector no estándar \, todas las reglas tienen contrapartes simétricas, excepto las de implicación. Esto refleja el hecho de que el lenguaje habitual de la lógica de primer orden no incluye el conector "no está implicado por"${\displaystyle \not \leftarrow }$Ese sería el dual de De Morgan de la implicación. Añadir dicho conector con sus reglas naturales hace que el cálculo sea completamente simétrico izquierda-derecha.

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

A continuación se presenta la demostración de un hecho simple que involucra cuantificadores. Nótese que lo contrario no es cierto, y su falsedad se puede observar al intentar derivarlo de abajo hacia arriba, ya que una variable libre existente no puede usarse en sustitución en las reglas.${\displaystyle (\forall R)}$y${\displaystyle (\exists L)}$.

Para algo más interesante lo demostraremos${\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)}}$Resulta sencillo encontrar la derivación, lo que ejemplifica la utilidad de LK en la demostración automatizada.

Estas derivaciones también enfatizan la estructura estrictamente formal del cálculo de secuentes. 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. Cabe señalar, 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 multiconjuntos de fórmulas en la interpretación del secuente, en lugar de secuencias, eliminando la necesidad de una regla de permutación explícita. Esto corresponde a trasladar la conmutatividad de supuestos y derivaciones fuera del cálculo de secuentes, mientras que LK la integra dentro del propio sistema.

Para ciertas formulaciones (es decir, variantes) del cálculo de secuencias, una demostración en dicho cálculo es isomorfa a un tableau analítico cerrado invertido . ^{[ 28 ]}

Las reglas estructurales merecen un análisis más detallado.

El debilitamiento (W) permite añadir elementos arbitrarios a una secuencia. Intuitivamente, esto se permite en el antecedente porque siempre podemos restringir el alcance de nuestra demostración (si todos los coches tienen ruedas, entonces podemos afirmar con seguridad que todos los coches negros tienen ruedas); y en el concesionario porque siempre podemos contemplar conclusiones alternativas (si todos los coches tienen ruedas, entonces podemos afirmar con seguridad que todos los coches tienen ruedas o alas).

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

Sin embargo, el esfuerzo adicional que supone el uso de secuencias se justifica, ya que se pueden omitir parte o la totalidad de las reglas estructurales. Al hacerlo, se obtienen 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, una afirmación${\displaystyle A}$Se deduce semánticamente de un conjunto de premisas.${\displaystyle \Gamma }$${\displaystyle (\Gamma \vDash A)}$si y solo si el secuencial${\displaystyle \Gamma \vdash A}$puede derivarse de las reglas anteriores. ^{[ 29 ]}

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

Existe cierta libertad de elección en cuanto a los detalles técnicos de cómo se formalizan las secuencias y las reglas estructurales, sin que ello implique cambiar las secuencias que deriva el sistema.

En primer lugar, como se mencionó anteriormente, las secuencias 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 el axioma (I) se cambia para derivar cualquier secuencial de la forma${\displaystyle \Gamma ,A\vdash A,\Delta }$Cualquier debilitamiento que aparezca en una derivación puede trasladarse al principio de la demostración. Esto puede resultar conveniente al construir demostraciones de abajo hacia arriba.

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,${\displaystyle ({\lor }L)}$en cambio puede formularse como

${\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 conectores diferentes.

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

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

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

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

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

Alternativamente, se puede restringir o prohibir el uso de algunas de las reglas estructurales. Esto da lugar a diversos sistemas de lógica subestructural . Generalmente son más débiles que la lógica de Kalman ( 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, poseen otras propiedades interesantes que han propiciado aplicaciones en la informática teórica y la inteligencia artificial .

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

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

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

De hecho, las únicas reglas en LK que necesitan ser restringidas a consecuentes de fórmula única son${\displaystyle ({\to }R)}$,${\displaystyle (\neg R)}$(que puede considerarse un caso especial de${\displaystyle {\to }R}$, como se describió anteriormente) y${\displaystyle ({\forall }R)}$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${\displaystyle ({\to }R)}$y${\displaystyle ({\forall }R)}$convertirse

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

y (cuando${\displaystyle y}$no aparece libre en la secuencia inferior)

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

Estas dos reglas no son válidas desde un punto de vista intuicionista.