Cálculo secuencial

Estilo de argumentación lógica formal.

En lógica matemática , el cálculo secuente es un estilo de argumentación lógica formal en el que cada línea de una prueba es una tautología condicional (llamada secuente 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 al estilo anterior de lógica formal de David Hilbert , en el que cada La 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 secuentes significan teoremas condicionales en un lenguaje de primer orden en lugar de tautologías condicionales.

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

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

En otras palabras, los sistemas de deducción natural y de cálculo secuente son tipos distintos de sistemas de estilo Gentzen. Los sistemas de estilo Hilbert suelen tener un número muy pequeño 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 puedan manipularse 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 expresiones no cuantificadas (que normalmente contienen variables libres ) y luego se reintroducen los cuantificadores. Esto es muy paralelo a la forma en que los matemáticos llevan a cabo las demostraciones matemáticas en la práctica. Las pruebas de cálculo de predicados generalmente son mucho más fáciles de descubrir con este enfoque y, a menudo, son más cortas. 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.

Descripción general

En teoría de la prueba y lógica matemática , el cálculo sucesivo es una familia de sistemas formales que comparten un cierto estilo de inferencia y ciertas propiedades formales. Los primeros sistemas de cálculo secuente, 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" de Gentzen ( Hauptsatz ) sobre LK y LJ fue el teorema de eliminación de cortes , ^{[2] [3] un resultado con consecuencias} metateóricas de gran alcance , incluida la coherencia . 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 sorprendente respuesta a los teoremas de incompletitud de Gödel . Desde estos primeros trabajos, los cálculos secuenciales, también llamados sistemas 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. .

Sistemas de deducción estilo Hilbert

Una forma de clasificar 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 al estilo de Hilbert , donde un juicio tiene la forma

${\displaystyle 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, por ejemplo , 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 concluyente en una demostración válida. Un sistema al estilo de Hilbert no necesita distinción entre fórmulas y juicios; hacemos uno aquí únicamente para compararlo con los casos que siguen. ${\displaystyle B}$

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

Sistemas de deducción natural

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

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

donde los 's y son nuevamente fórmulas y . Las permutaciones de las 's son irrelevantes. En otras palabras, una sentencia consta de 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]} Los teoremas son aquellas fórmulas tales que (con un lado izquierdo vacío) es la conclusión de una demostración válida. (En algunas presentaciones de deducción natural, la s y el torniquete no se escriben explícitamente; en cambio, se utiliza una notación bidimensional a partir de la cual se pueden inferir). ${\displaystyle A_{i}}$ ${\displaystyle B}$ ${\displaystyle n\geq 0}$ ${\displaystyle A_{i}}$ ${\displaystyle \vdash }$ ${\displaystyle B}$ ${\displaystyle \vdash B}$ ${\displaystyle A_{i}}$

La semántica estándar de un juicio en deducción natural es que afirma que siempre que ^[11] , etc., sean todos verdaderos, también lo serán. los juicios ${\displaystyle 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.

Sistemas de cálculo secuencial

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 secuente. Las fórmulas del lado izquierdo del torniquete se denominan antecedente y las fórmulas del lado derecho se denominan sucedente o consecuente ; en conjunto se llaman cedentes o secuentes . ^[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 en los que se concluye 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 secuente es una afirmación de que siempre que cada uno sea verdadero, al menos uno también será verdadero. ^[13] Así, el secuente 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 una "y", y una coma a la derecha del torniquete debe considerarse como una "o" (inclusive). las secuencias ${\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 cualquier consecuente puede extenderse a una prueba del otro consecuente.

A primera vista, esta extensión de la forma de juicio puede parecer una extraña complicación: 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 de la coma. torniquete. Sin embargo, en un contexto clásico , la semántica del secuente también puede expresarse (mediante 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 darse el caso de 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 un lado está negado. Por tanto, intercambiar izquierda por derecha en un secuente 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 consecuentes y, de hecho, las reglas de inferencia en el cálculo de secuentes para tratar con la conjunción (∧) son imágenes especulares de aquellos que se ocupan de la disyunción (∨).

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

Distinción entre deducción natural y cálculo secuencial

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 intuicionista de deducción natural de Nueva Jersey 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 secuente LJ daba 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 fórmulas sucesivas múltiples está destinado particularmente a su teorema principal ("Hauptsatz"). ^[18]

Origen de la palabra "siguiente"

La palabra "secuente" está tomada 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 'sequent', porque ya hemos usado 'sequence' para cualquier sucesión de objetos, donde el alemán es 'Folge'. ". ^[19]

Demostrar fórmulas lógicas

Un árbol enraizado que describe un procedimiento de búsqueda de pruebas mediante cálculo secuencial.

árboles de reducción

El cálculo secuencial puede verse como una herramienta para probar fórmulas en lógica proposicional , similar al método de cuadros 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. ^[20]

Considere la siguiente fórmula:

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

Esto está escrito de la siguiente forma, donde la proposición que necesita ser probada 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 con asumir la premisa de la implicación y luego intentar probar su conclusión. ^[21] Por lo tanto se pasa al siguiente siguiente:

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

Nuevamente, el lado derecho incluye una implicación, cuya premisa se puede asumir de modo que sólo 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 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 del primer argumento de la izquierda. Así podemos dividir el secuente 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 el siguiente nuevamente 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 secuencial está hecho; el primer secuente se puede simplificar aún más en:

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

Este proceso siempre se puede continuar hasta que solo queden fórmulas atómicas en cada lado. El proceso se puede describir gráficamente mediante un gráfico de árbol con raíces , como se muestra a la derecha. La raíz del árbol es la fórmula que queremos probar; las hojas constan únicamente de 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 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 sólo si al menos uno de los símbolos de la derecha también aparece a la izquierda.

A continuación se detallan las reglas según las cuales se avanza a lo largo del árbol. Siempre que un secuente se divide en dos, el vértice del árbol tiene dos vértices secundarios y el árbol se ramifica. Además, uno puede cambiar libremente el orden de los argumentos de 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]

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 sólo 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 la regla lo elimina, el proceso finaliza cuando no quedan operadores lógicos: La fórmula se ha descompuesto .

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

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

Relación con las axiomatizaciones estándar

El cálculo secuencial está relacionado con otras axiomatizaciones del cálculo proposicional, como el cálculo proposicional de Frege o la axiomatización ^{[ ancla rota ]} de Jan Łukasiewicz (en sí misma parte del sistema estándar de Hilbert ): cada fórmula que se puede probar en estos tiene un árbol de reducción.

Esto se puede demostrar de la siguiente manera: toda prueba en cálculo proposicional utiliza sólo axiomas y reglas de inferencia. Cada uso de un esquema de axioma produce una fórmula lógica verdadera y, por tanto, puede demostrarse en cálculos posteriores; 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.

El sistema LK

Esta sección presenta las reglas del cálculo de secuentes LK (que significa Logistische Kalkül) tal como las introdujo Gentzen en 1934. ^[24] Una prueba (formal) en este cálculo es una secuencia de secuentes, donde cada uno de los secuentes es derivable de los secuentes que aparecen anteriormente en la secuencia usando una de las reglas siguientes.

Reglas de inferencia

Se utilizará la siguiente notación:

• ${\displaystyle \vdash }$conocido como torniquete , separa los supuestos de la izquierda de las proposiciones de la derecha
• ${\displaystyle A}$y denota 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 disyuntiva (al menos una de las fórmulas debe ser válida para cualquier asignación de variables), ${\displaystyle \vdash }$
• ${\displaystyle t}$denota un término arbitrario,
• ${\displaystyle x}$y denota variables. ${\displaystyle y}$
• Se dice que una variable aparece libre dentro de una fórmula si no está vinculada por cuantificadores o . ${\displaystyle \forall }$ ${\displaystyle \exists }$
• ${\displaystyle A[t/x]}$denota la fórmula que se obtiene sustituyendo el término por cada aparición 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 aparición de ninguna variable en queda ligada 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; uno para usar a la izquierda ('L') de a y el otro a su derecha ('R'). Las reglas se abrevian como '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 }$

Tenga en cuenta que, contrariamente a las reglas para proceder a lo largo del árbol de reducción presentado anteriormente, las siguientes reglas sirven para moverse en direcciones opuestas, de axiomas a teoremas. Por lo tanto, son imágenes especulares exactas de las reglas anteriores, excepto que aquí no se asume implícitamente la simetría y se agregan reglas relacionadas con la cuantificación .

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

Una explicación intuitiva

Las reglas anteriores se pueden dividir en dos grandes grupos: las lógicas y las 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 expresadas de manera 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 uno pueda demostrar 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. Asimismo, la regla establece que, si y es suficiente para concluir , entonces a partir de uno solo se puede concluir o debe ser falso, es decir, válido. 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 intuición sobre las reglas del cuantificador, considere la regla . Por supuesto, en general no es posible concluir que esto se cumple simplemente por el hecho de que es cierto. 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 eso es válido para cualquier valor de y. Las demás reglas deberían ser entonces 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 pueden considerar como instrucciones para la construcción de una prueba para un enunciado determinado. En este caso las reglas pueden leerse de abajo hacia arriba; por ejemplo, dice que, para demostrar que se sigue de los supuestos y , basta demostrar que se puede concluir de y se puede concluir de , respectivamente. Tenga en cuenta que, dado algún antecedente, no está claro cómo dividirlo en y . Sin embargo, sólo hay un número finito de posibilidades que comprobar, ya que el antecedente por suposición es finito. Esto también ilustra cómo se puede considerar que la teoría de la prueba opera sobre pruebas de manera combinatoria: dadas pruebas para ambos 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 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 puede concluirse y esta fórmula puede servir también como premisa para concluir otros enunciados, entonces la fórmula puede "cortarse" y unirse las derivaciones respectivas. Al construir una prueba de abajo hacia arriba, esto crea el problema de adivinar (ya que no aparece en absoluto a continuación). El teorema de eliminación de cortes es, por 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 prueba, lo que implica que a cualquier secuente demostrable se le puede dar una prueba sin cortes . ${\displaystyle A}$ ${\displaystyle A}$ ${\displaystyle A}$

La segunda regla que es algo especial es el axioma de identidad (I). La lectura intuitiva de esto es obvia: cada fórmula se demuestra a sí misma. Al igual que la regla de corte, el axioma de identidad es algo redundante: la integridad de las secuencias iniciales atómicas establece que la regla puede restringirse a fórmulas atómicas sin pérdida de demostrabilidad.

Observe que todas las reglas tienen compañeros 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á implicado por" que sería el dual de implicación de De Morgan. Agregar tal conectivo con sus reglas naturales haría que el cálculo fuera completamente simétrico de izquierda a derecha. ${\displaystyle \not \leftarrow }$

Derivaciones de ejemplo

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

Lo siguiente es la prueba de un hecho simple que involucra cuantificadores. Tenga en cuenta que lo contrario no es cierto y su falsedad se puede ver al intentar derivarla 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)}$

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

Estas derivaciones también enfatizan la estructura estrictamente formal del cálculo secuente. 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. Tenga en cuenta, 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 un cambio de conmutatividad de supuestos y derivaciones fuera del cálculo secuente, mientras que LK lo incorpora dentro del propio sistema.

Relación con los cuadros analíticos

Para ciertas formulaciones (es decir, variantes) del cálculo secuente, una prueba en dicho cálculo es isomorfa a un cuadro analítico cerrado e invertido . ^[25]

Reglas estructurales

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 sucesivo porque siempre podemos permitir conclusiones alternativas (si todos los automóviles tienen ruedas, entonces es seguro decir que todos los automóviles tienen ruedas o alas).

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

Sin embargo, el esfuerzo adicional de utilizar secuencias está justificado ya que se pueden omitir parte o la totalidad de las reglas estructurales. De esta manera se obtienen las llamadas lógicas subestructurales .

Propiedades del sistema LK

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 siguiente, la regla de corte es admisible . Este resultado también se conoce como Hauptsatz de Gentzen ("Teorema principal"). ^{[2] [3]}

Variantes

Las reglas anteriores se pueden modificar de varias maneras:

Alternativas estructurales menores

Existe cierta libertad de elección con respecto a 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, se puede considerar que los secuenciales consisten en conjuntos o multiconjuntos . En este caso, las reglas para permutar y (cuando se utilizan conjuntos) fórmulas de contracción son innecesarias.

La regla de debilitamiento se vuelve admisible si se cambia el axioma (I) para derivar cualquier secuente de la forma . Cualquier debilitamiento que aparezca en una derivación puede trasladarse al comienzo de la demostración. Este puede ser un cambio conveniente al construir pruebas 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.

Absurdo

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

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

O si, como se describió anteriormente, el debilitamiento debe 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 )}$

Lógicas subestructurales

Alternativamente, se puede restringir o prohibir el uso de algunas de las reglas estructurales. Esto produce una variedad de sistemas lógicos subestructurales . Generalmente son más débiles que LK ( es decir , tienen menos teoremas) y, por 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 informática teórica e inteligencia artificial .

Cálculo secuencial intuicionista: Sistema LJ

Sorprendentemente, algunos pequeños cambios en las reglas de LK son suficientes para convertirlo en un sistema de prueba para la lógica intuicionista . ^[27] Para este fin, uno tiene que restringir a los secuentes con como máximo una fórmula en el lado derecho, ^[28] y modificar las reglas para mantener esta invariante. 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 similar de eliminación de cortes. Esto se puede utilizar para demostrar propiedades de disyunción y existencia .

De hecho, las únicas reglas en LK que deben 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 intuicionistamente válidas.

Ver también

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

Notas

1. Gentzen 1934, Gentzen 1935.
2. Curry 1977, págs. 208-213, ofrece una prueba de cinco páginas del teorema de eliminación. Véanse también las páginas 188, 250.
3. Kleene 2009, págs. 453, ofrece una prueba muy breve del teorema de eliminación de cortes.
4. Curry 1977, págs. 189-244, llama sistemas LC a los sistemas Gentzen. El énfasis de Curry está más en la teoría que en las pruebas lógicas prácticas.
5. Kleene 2009, págs. 440–516. Este libro está mucho más preocupado por las implicaciones teóricas y metamatemáticas del cálculo secuencial al estilo Gentzen que por las aplicaciones a las demostraciones lógicas prácticas.
6. Kleene 2002, págs. 283–312, 331–361, define los sistemas Gentzen y demuestra varios teoremas dentro de estos sistemas, incluido el teorema de completitud de Gödel y el teorema de Gentzen.
7. Smullyan 1995, págs. 101-127, ofrece una breve presentación teórica de los sistemas Gentzen. Utiliza el estilo de diseño de prueba de cuadro.
8. Curry 1977, págs. 184-244, compara los sistemas de deducción natural, denominados LA, y los sistemas Gentzen, denominados LC. El énfasis de Curry es más teórico que práctico.
9. Suppes 1999, págs. 25-150, es una presentación introductoria de la deducción natural práctica de este tipo. Esto se convirtió en la base del Sistema L.
10. Lemmon 1965 es una introducción elemental a la deducción natural práctica basada en el conveniente estilo de diseño de prueba abreviada System L basado en Suppes 1999, págs.
11. Aquí, "siempre que" se utiliza como abreviatura informal "para cada asignación de valores a las variables libres en el juicio"
12. Shankar, Natarajan ; Oh, Sam; Rushby, John M .; Stringer-Calvert, David WJ (1 de noviembre de 2001). "Guía del probador PVS" (PDF) . Guía del usuario . SRI Internacional . Consultado el 29 de mayo de 2015 .
13. Para obtener explicaciones de la semántica disyuntiva para el lado derecho de los secuentes, consulte Curry 1977, págs. 189-190, Kleene 2002, págs. 290, 297, Kleene 2009, p. 441, Hilbert y Bernays 1970, pág. 385, Smullyan 1995, págs. 104-105 y Gentzen 1934, pág. 180.
14. Buss 1998, pag. 10
15. Caballero 1934, pag. 188. "Der Kalkül NJ hat manche formale Unschönheiten".
16. Caballero 1934, pag. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül wird estos sonderstellung aufgehoben ".
17. Caballero 1934, pag. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener".
18. Caballero 1934, pag. 191. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher No estamos bien."
19. Kleene 2002, pag. 441.
20. Lógica Aplicada, Univ. de Cornell: Conferencia 9. Última consulta: 25 de junio de 2016
21. "Recuerde, la forma de demostrar una implicación es asumiendo la hipótesis ". — Philip Wadler , el 2 de noviembre de 2015, en su discurso de apertura: "Proposiciones como tipos". Minuto 14:36/55:28 del videoclip de Code Mesh
22. Tait WW (2010). "La prueba de consistencia original de Gentzen y el teorema de la barra" (PDF) . En Kahle R, Rathjen M (eds.). El centenario de Gentzen: la búsqueda de la coherencia . Nueva York: Springer. págs. 213–228.
23. Jan von Plato, Elementos del razonamiento lógico , Cambridge University Press, 2014, pág. 32.
24. Andrzej-Indrzejczak, Introducción a la teoría y las aplicaciones de los cálculos secuenciales proposicionales (2021, capítulo "Cálculo secuencial de Gentzen LK"). Consultado el 3 de agosto de 2022.
25. Smullyan 1995, pág. 107
26. Kleene 2002, pag. 336, escribió en 1967 que "fue un descubrimiento lógico importante de Gentzen 1934-5 que, cuando hay cualquier prueba (puramente lógica) de una proposición, hay una prueba directa. Las implicaciones de este descubrimiento están en las investigaciones lógicas teóricas, en lugar de construir colecciones de fórmulas probadas".
27. Caballero 1934, pag. 194, escribió: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK . Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Su kzedensbedingung ausgedrückt extraño." Traducción al inglés: "La diferencia entre la lógica intuicionista y la clásica es, en el caso de los cálculos LJ y LK , de un tipo extremadamente, totalmente diferente al caso de NJ y NK . En el último caso, consistió en la eliminación o adición respectivamente de la regla del medio excluido, mientras que en el primer caso se expresa a través de las condiciones sucedentes."
28. M. Tiomkin, "Demostrar la imposibilidad de demostrarlo", págs. 22-26. En Actas del Tercer Simposio Anual sobre Lógica en Ciencias de la Computación, 5 al 8 de julio de 1988 (1988), IEEE. ISBN 0-8186-0853-6.

Referencias

• Buss, Samuel R. (1998). "Una 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 la 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 Internacional. ISBN 978-0-923891-57-2.
• Kleene, Stephen Cole (2002) [1967]. Lógica matemática . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Lógica inicial . Tomás Nelson. ISBN 0-17-712040-1.
• Mancosu, Paolo; Galván, Sergio; Zach, Richard (2021). Introducción a la teoría de la prueba: normalización, eliminación de cortes y pruebas de consistencia . Prensa de la Universidad de Oxford . pag. 431.ISBN​ 978-0-19-289593-6.
• Smullyan, Raymond Merrill (1995) [1968]. Lógica de primer orden . Nueva York: Publicaciones de Dover. ISBN 978-0-486-68370-6.
• Suppes, Patrick Coronel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-40687-9.

enlaces externos

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