Cálculo secuencial

En lógica matemática, el cálculo de secuencias es un estilo de argumentación lógica formal en el que cada línea de una prueba es una tautología condicional (llamada secuencia 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 las 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 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 incondicional (o teorema).
• Estilo Gentzen. Cada línea es una tautología condicional (o teorema) con cero o más condiciones a la izquierda.
  • Deducción natural. Cada línea (condicional) tiene exactamente una propuesta afirmada sobre la derecha.
  • Cálculo secuencial. Cada línea (condicional) tiene cero o más proposiciones afirmadas a la derecha.

En otras palabras, la deducción natural y los sistemas de cálculo secuencial son tipos particulares 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 teóricas y prácticas en comparación con los sistemas de estilo Hilbert. Por ejemplo, tanto la deducción natural como los sistemas de cálculo secuencial facilitan la eliminación y la introducción de cuantificadores universales y existenciales para 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 vuelven a introducir los cuantificadores. Esto es muy similar a la forma en que los matemáticos llevan a cabo en la práctica las demostraciones matemáticas. Las pruebas de cálculo de predicados son generalmente 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.

Resumen

En la teoría de la demostración y la 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 como una herramienta para estudiar la deducción natural en lógica de primer orden (en lógica clásica e intuicionista). versiones, respectivamente). El llamado "Teorema principal" de Gentzen (Hauptsatz) sobre LK y LJ fue el teorema de eliminación de cortes, un resultado con consecuencias metateóricas de gran 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 corte para dar una prueba (transfinita) de la consistencia de la aritmética de Peano, en una sorprendente respuesta a los teoremas de incompletitud de Gödel. Desde este trabajo inicial, los cálculos secuenciales, también llamados sistemas Gentzen, 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 automática.

Sistemas de deducción estilo Hilbert

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

B{displaystyle B}

Donde B{displaystyle B} es cualquier fórmula de la lógica de primer orden (o cualquier lógica que el sistema de deducción aplica a, 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 la sentencia final en una prueba válida. Un sistema de estilo Hilbert no necesita distinción entre fórmulas y juicios; hacemos uno aquí solamente para comparación con los casos que siguen.

El precio que se paga por la sintaxis simple de un sistema estilo Hilbert es que las pruebas formales completas tienden a ser extremadamente largas. Los argumentos concretos sobre las pruebas 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

A1,A2,...... ,An⊢ ⊢ B{displaystyle A_{1},A_{2},ldotsA_{n}vdash B}

Donde Ai{displaystyle A_{i}'s y B{displaystyle B} son de nuevo fórmulas y n≥ ≥ 0{displaystyle ngeq 0}. Permutaciones de las Ai{displaystyle A_{i}Es inmaterial. En otras palabras, un juicio consiste en una lista (posiblemente vacía) de fórmulas en el lado izquierdo de un símbolo voltible "⊢ ⊢ {displaystyle vdash }", con una sola fórmula en el lado derecho. Los teoremas son esas fórmulas B{displaystyle B} tales que ⊢ ⊢ B{displaystyle vdash B} (con un lado izquierdo vacío) es la conclusión de una prueba válida. (En algunas presentaciones de deducción natural, la Ai{displaystyle A_{i}s y el torntil no están escritos explícitamente; en cambio una notación bidimensional de la que pueden ser inferidos se utiliza.)

La semántica estándar de un juicio en deducción natural es que afirma que cada vez que A1{displaystyle A_{1}, A2{displaystyle A_{2}, etc., son todos verdaderos, B{displaystyle B} también será verdad. Los juicios

A1,...... ,An⊢ ⊢ B{displaystyle A_{1},ldotsA_{n}vdash B}

y

⊢ ⊢ ()A1∧ ∧ ⋯ ⋯ ∧ ∧ An)→ → B{displaystyle vdash (A_{1}land cdots land A_{n})rightarrow B.

son equivalentes en el sentido fuerte de que una prueba de uno 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

A1,...... ,An⊢ ⊢ B1,...... ,Bk,{displaystyle A_{1},ldotsA_{n}vdash B_{1},ldots B_{k},}

un objeto sintáctico llamado secuencial. Las fórmulas en el lado izquierdo del torntil se llaman el antecedentes, y las fórmulas de la mano derecha se llaman la succedent o consiguiente; juntos se llaman cedents o secuelas. Otra vez, Ai{displaystyle A_{i} y Bi{displaystyle B_{i} son fórmulas, y n{displaystyle n} y k{displaystyle k} son enteros no negativos, es decir, el lado izquierdo o el lado derecho (o ninguno o ambos) puede estar vacío. Como en deducción natural, los teoremas son aquellos B{displaystyle B} Donde ⊢ ⊢ B{displaystyle vdash B} es la conclusión de una prueba válida.

La semántica estándar de un secuenciado es una afirmación de que cada vez que cada uno Ai{displaystyle A_{i} es verdad, al menos uno Bi{displaystyle B_{i} también será verdad. Así el secuente vacío, teniendo ambos cedents vacíos, es falso. Una manera de expresar esto es que un coma a la izquierda del torntil debe ser pensado como un "y", y una coma a la derecha del torntil debe ser pensado como un "o" (inclusivo). Las secuelas

A1,...... ,An⊢ ⊢ B1,...... ,Bk{displaystyle A_{1},ldotsA_{n}vdash B_{1},ldots B_{k}

y

⊢ ⊢ ()A1∧ ∧ ⋯ ⋯ ∧ ∧ An)→ → ()B1Alternativa Alternativa ⋯ ⋯ Alternativa Alternativa Bk){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 secuentes puede extenderse a una prueba 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, e inicialmente es 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 secuente también puede (por tautología proposicional) expresarse como

⊢ ⊢ ¬ ¬ A1Alternativa Alternativa ¬ ¬ A2Alternativa Alternativa ⋯ ⋯ Alternativa Alternativa ¬ ¬ AnAlternativa Alternativa B1Alternativa Alternativa B2Alternativa Alternativa ⋯ ⋯ Alternativa Alternativa Bk{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

⊢ ⊢ ¬ ¬ ()A1∧ ∧ A2∧ ∧ ⋯ ⋯ ∧ ∧ An∧ ∧ ¬ ¬ B1∧ ∧ ¬ ¬ B2∧ ∧ ⋯ ⋯ ∧ ∧ ¬ ¬ Bk){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 As sean verdaderas y todas las B sean falsas).

En estas formulaciones, la única diferencia entre las fórmulas a cada lado del torniquete es que un lado está negado. Por lo 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 los secuentes y, de hecho, las reglas de inferencia en el cálculo de secuentes para tratar con conjunciones. (∧) son imágenes especulares de aquellos que se ocupan de la disyunción (∨).

Muchos lógicos sienten 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 de deducción natural intuicionista NJ era algo feo. 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 secuencial clásico LK. 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). 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").

Origen de la palabra "secuente"

La palabra "secuente" se toma de la palabra "Sequenz" en el artículo de 1934 de Gentzen. Kleene hace el siguiente comentario sobre la traducción al inglés: "Gentzen dice 'Sequenz', que traducimos como 'sequent', porque ya hemos usado 'sequence' 39; para cualquier sucesión de objetos, donde el alemán es 'Folge'."

Demostración de fórmulas lógicas

Un árbol enraizado que describe un procedimiento de búsqueda de pruebas por cálculo secuenciado

Á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 los cuadros analíticos. Da una serie de pasos que permiten reducir el problema de probar una fórmula lógica a fórmulas cada vez más simples hasta llegar a las triviales.

Considere la siguiente fórmula:

()()p→ → r)Alternativa Alternativa ()q→ → r))→ → ()()p∧ ∧ q)→ → r){displaystyle (prightarrow r)lor (qrightarrow r)rightarrow (pland q)rightarrow r)}

Esto está escrito en la siguiente forma, donde la proposición que necesita ser probada es a la derecha del símbolo de voltaje ⊢ ⊢ {displaystyle vdash }:

⊢ ⊢ ()()p→ → r)Alternativa Alternativa ()q→ → r))→ → ()()p∧ ∧ q)→ → r){displaystyle vdash (prightarrow r)lor (qrightarrow r)rightarrow (pland 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 tratar de probar su conclusión. Por lo tanto, se pasa al siguiente secuente:

()p→ → r)Alternativa Alternativa ()q→ → r)⊢ ⊢ ()p∧ ∧ q)→ → r{displaystyle (prightarrow r)lor (qrightarrow r)vdash (pland q)rightarrow r}

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

()p→ → r)Alternativa Alternativa ()q→ → r),()p∧ ∧ q)⊢ ⊢ r{displaystyle (prightarrow r)lor (qrightarrow r),(pland q)vdash r}

Dado que se supone que los argumentos en el lado izquierdo están relacionados por conjunción, esto puede ser reemplazado por lo siguiente:

()p→ → r)Alternativa Alternativa ()q→ → r),p,q⊢ ⊢ r{displaystyle (prightarrow r)lor (qrightarrow r),p,qvdash r}

Esto es equivalente 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:

p→ → r,p,q⊢ ⊢ r{displaystyle prightarrow r,p,qvdash r}

q→ → r,p,q⊢ ⊢ r{displaystyle qrightarrow r,p,qvdash r}

En el caso del primer juicio, reescribimos p→ → r{displaystyle prightarrow r} como ¬ ¬ pAlternativa Alternativa r{displaystyle lnot plor r} y dividir el secuenciado de nuevo para conseguir:

¬ ¬ p,p,q⊢ ⊢ r{displaystyle lnot p,p,qvdash r}

r,p,q⊢ ⊢ r{displaystyle r,p,qvdash r}

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

p,q⊢ ⊢ p,r{displaystyle p,qvdash p,r}

Este proceso siempre se puede continuar hasta que solo haya 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 consisten únicamente en fórmulas atómicas. El árbol se conoce como árbol de reducción.

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 consisten solo en símbolos atómicos, el consecuente se acepta axiomáticamente (y siempre es cierto) si y solo si al menos uno de los símbolos de la derecha también aparece a la izquierda.

Las siguientes son las reglas por las cuales uno procede a lo largo del árbol. Cada vez 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 en cada lado; Γ y Δ representan posibles argumentos adicionales.

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.

Comenzando con cualquier fórmula en lógica proposicional, mediante una serie de pasos, el lado derecho del torniquete se puede procesar hasta que solo incluya símbolos atómicos. Luego, se hace lo mismo para el lado izquierdo. Dado que todos los operadores lógicos aparecen en una de las reglas anteriores y la regla los elimina, el proceso termina cuando no quedan operadores lógicos: la fórmula se ha descompuesto.

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

Es fácil ver que los pasos en el árbol conservan el valor de verdad semántico de las fórmulas implícitas en ellos, entendiendo la conjunción entre las diferentes ramas del árbol siempre que haya 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. Así, 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 de Jan Łukasiewicz (en sí misma una parte del sistema estándar de Hilbert): Cada fórmula que se puede demostrar en estos tiene un árbol de reducción.

Esto se puede demostrar de la siguiente manera: cada prueba en el cálculo proposicional usa solo axiomas y las reglas de inferencia. Cada uso de un esquema de axioma produce una fórmula lógica verdadera y, por lo tanto, puede probarse en cálculo secuencial; ejemplos de estos se muestran a continuación. La única regla de inferencia en los sistemas mencionados anteriormente es modus ponens, que se implementa mediante la regla de corte.

El sistema LK

Esta sección presenta las reglas del cálculo secuencial LK (que significa Logistische Kalkül) tal como lo introdujo Gentzen en 1934. Una prueba (formal) en este cálculo es una secuencia de secuencias, donde cada una de las secuencias se puede derivar de las secuencias que aparecen antes en la secuencia mediante el uso de una de las siguientes reglas.

Reglas de inferencia

Se utilizará la siguiente notación:

• ⊢ ⊢ {displaystyle vdash } conocido como el torntil, separa el suposiciones a la izquierda proposiciones a la derecha
• A{displaystyle A} y B{displaystyle B} denota fórmulas de la lógica predicada de primer orden (también se puede restringir esto a la lógica proposiciónl),
• .. ,Δ Δ ,.. {displaystyle GammaDeltaSigma }, y ▪ ▪ {displaystyle Pi } son secuencias finitas (posiblemente vacías) de fórmulas (de hecho, el orden de fórmulas no importa; ver § Reglas estructurales), llamadas contextos,
  • cuando en izquierda de la ⊢ ⊢ {displaystyle vdash }, se considera la secuencia de fórmulas conjuntivamente (todos supuestos que se mantienen al mismo tiempo)
  • mientras que en derecho de la ⊢ ⊢ {displaystyle vdash }, se considera la secuencia de fórmulas disjuntivamente (al menos una de las fórmulas debe tener para cualquier asignación de variables),
• t{displaystyle t} denota un término arbitrario,
• x{displaystyle x} y Sí.{displaystyle y} denota variables.
• una variable se dice que ocurre libre dentro de una fórmula si no está ligada por cuantificadores О О {displaystyle forall } o ∃ ∃ {displaystyle exists }.
• A[t/x]{displaystyle A[t/x]} denota la fórmula que se obtiene sustituyendo el término t{displaystyle t} para cada ocurrencia libre de la variable x{displaystyle x} en fórmula A{displaystyle A} con la restricción de que el término t{displaystyle t} debe ser libre para la variable x{displaystyle x} dentro A{displaystyle A} (es decir, no ocurre ninguna variable en t{displaystyle t} se atan A[t/x]{displaystyle A[t/x]}).
• WL{displaystyle WL., WR{displaystyle WR., CL{displaystyle CL}, CR{displaystyle CR}, PL{displaystyle ¡Vamos!, PR{displaystyle PR.: Estos seis soporten para las dos versiones de cada una de las tres reglas estructurales; una para uso en la izquierda ('L') de una ⊢ ⊢ {displaystyle vdash }, y el otro a su derecha ('R'). Las reglas son abreviadas 'W' para Debilitamiento (izquierda/derecha), 'C' para Contracciones, y 'P' para Permutación.

Tenga en cuenta que, contrariamente a las reglas para proceder a lo largo del árbol de reducción presentado anteriormente, las siguientes reglas son 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 ()О О R){displaystyle ({forall }R)} y ()∃ ∃ L){displaystyle ({exists }L)}, la variable Sí.{displaystyle y} no debe ocurrir libre en ningún lugar en los respectivos secunts inferiores.

Una explicación intuitiva

Las reglas anteriores pueden dividirse en dos grupos principales: lógica y estructural Unos. Cada una de las reglas lógicas introduce una nueva fórmula lógica ya sea a la izquierda o a la derecha del torntil ⊢ ⊢ {displaystyle vdash }. En cambio, las reglas estructurales funcionan sobre la estructura de los secuentes, ignorando la forma exacta de las fórmulas. Las dos excepciones a este esquema general son el axioma de identidad (I) y el estado de (Cut).

Aunque se afirma de manera formal, las reglas anteriores permiten una lectura muy intuitiva en términos de lógica clásica. Considerar, por ejemplo, la regla ()∧ ∧ L1){displaystyle ({land }L_{1})}. Dice que, cuando uno puede probar que Δ Δ {displaystyle Delta } se puede concluir de alguna secuencia de fórmulas que contienen A{displaystyle A}, entonces uno también puede concluir Δ Δ {displaystyle Delta } de la suposición (más fuerte) de que A∧ ∧ B{displaystyle Aland B} sostiene. Asimismo, la regla ()¬ ¬ R){displaystyle ({neg }R)} dice que, si .. {displaystyle "Gamma" y A{displaystyle A} suficiente para concluir Δ Δ {displaystyle Delta }, entonces de .. {displaystyle "Gamma" solo uno puede concluir Δ Δ {displaystyle Delta } o A{displaystyle A} Debe ser falso, es decir. ¬ ¬ A{displaystyle {neg }A} sostiene. Todas las reglas pueden ser interpretadas de esta manera.

Para una intuición sobre las reglas del cuantificador, considere la regla ()О О R){displaystyle ({forall }R)}. Por supuesto, concluyendo que О О xA{displaystyle forall {x}A} es sólo por el hecho de que A[Sí./x]{displaystyle A[y/x]} es verdad no es posible en general. Si, sin embargo, la variable y no se menciona en otros lugares (es decir, todavía puede ser elegido libremente, sin influenciar la otra fórmula), entonces uno puede asumir, que A[Sí./x]{displaystyle A[y/x]} sostiene por cualquier valor de y. Las otras reglas deben ser bastante directas.

En lugar de ver las reglas como descripciones de derivaciones legales en lógica predicada, también se pueden considerar como instrucciones para la construcción de una prueba para una declaración dada. En este caso las reglas pueden leerse en el fondo; por ejemplo, ()∧ ∧ R){displaystyle ({land }R)} dice que, para probar eso A∧ ∧ B{displaystyle Aland B} de las hipótesis .. {displaystyle "Gamma" y .. {displaystyle Sigma }, basta probar que A{displaystyle A} puede concluirse .. {displaystyle "Gamma" y B{displaystyle B} puede concluirse .. {displaystyle Sigma }, respectivamente. Tenga en cuenta que, dado algún antecedente, no está claro cómo se va a dividir en .. {displaystyle "Gamma" y .. {displaystyle Sigma }. Sin embargo, sólo hay muchas posibilidades de ser verificadas ya que el antecedente por suposición es finito. Esto también ilustra cómo la teoría de la prueba puede verse como operando en pruebas de forma combinatoria: dadas pruebas para ambos A{displaystyle A} y B{displaystyle B}, uno puede construir una prueba para A∧ ∧ B{displaystyle Aland B}.

Al buscar alguna prueba, la mayoría de las reglas ofrecen recetas más o menos directas de cómo hacerlo. La regla del corte es diferente: afirma que, cuando una fórmula A{displaystyle A} se puede concluir y esta fórmula también puede servir de premisa para concluir otras declaraciones, luego la fórmula A{displaystyle A} puede ser "cortado" y se unen las respectivas derivaciones. Al construir una prueba de fondo, esto crea el problema de adivinar A{displaystyle A} (ya que no aparece en absoluto abajo). El teorema de la cut-elimination es, por tanto, crucial para las aplicaciones de cálculo secuencial en deducción automatizada: establece que todos los usos de la regla de corte pueden ser eliminados de una prueba, lo que implica que cualquier secuencia provable se puede dar a un libre de corte Prueba.

La segunda regla que es algo especial es el axioma de identidad (I). La lectura intuitiva de esto es obvia: cada fórmula se prueba a sí misma. Al igual que la regla de corte, el axioma de identidad es un tanto redundante: la integridad de los secuentes iniciales atómicos 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 los que tienen implicación. Esto refleja el hecho de que el lenguaje habitual de la lógica de primer orden no incluye el "no está implícito por" conectividad ↚{displaystyle not leftarrow } Ese sería el doble de implicación de De Morgan. Agregar tal conectividad con sus reglas naturales haría el cálculo completamente simétrico izquierda derecha.

Ejemplos de derivaciones

Aquí está la derivación de "⊢ ⊢ AAlternativa Alternativa ¬ ¬ A{displaystyle vdash Alor lnot A}", conocido como el Derecho del medio excluido ()tercio no datur en latín).

		()I){displaystyle (I)}
A⊢ ⊢ A{displaystyle Avdash A}
		()¬ ¬ R){displaystyle (lnot R)}
⊢ ⊢ ¬ ¬ A,A{displaystyle vdash lnot A,A}
		()Alternativa Alternativa R2){displaystyle (lor R_{2})}
⊢ ⊢ AAlternativa Alternativa ¬ ¬ A,A{displaystyle vdash Alor lnot A,A}
		()PR){displaystyle (PR)}
⊢ ⊢ A,AAlternativa Alternativa ¬ ¬ A{displaystyle vdash A,Alor lnot A}
		()Alternativa Alternativa R1){displaystyle (lor R_{1})}
⊢ ⊢ AAlternativa Alternativa ¬ ¬ A,AAlternativa Alternativa ¬ ¬ A{displaystyle vdash Alor lnot A,Alor lnot A}
		()CR){displaystyle (CR)}
⊢ ⊢ AAlternativa Alternativa ¬ ¬ A{displaystyle vdash Alor lnot A}

La siguiente es la prueba de un simple hecho que implica cuantificadores. Tenga en cuenta que el converso no es verdadero, y su falsedad se puede ver cuando se trata de derivarlo abajo-up, porque una variable libre existente no se puede utilizar en sustitución de las reglas ()О О R){displaystyle (forall R)} y ()∃ ∃ L){displaystyle (exists L)}.

		()I){displaystyle (I)}
p()x,Sí.)⊢ ⊢ p()x,Sí.){displaystyle p(x,y)vdash p(x,y)}
		()О О L){displaystyle (forall L)}
О О x()p()x,Sí.))⊢ ⊢ p()x,Sí.){displaystyle forall xleft(p(x,y)right)vdash p(x,y)}
		()∃ ∃ R){displaystyle (exists R)}
О О x()p()x,Sí.))⊢ ⊢ ∃ ∃ Sí.()p()x,Sí.)){displaystyle forall xleft(p(x,y)right)vdash exists yleft(p(x,y)right)}
		()∃ ∃ L){displaystyle (exists L)}
∃ ∃ Sí.()О О x()p()x,Sí.)))⊢ ⊢ ∃ ∃ Sí.()p()x,Sí.)){displaystyle exists yleft(forall xleft(p(x,y)right)vdash exists yleft(p(x,y)right)}
		()О О R){displaystyle (forall R)}
∃ ∃ Sí.()О О x()p()x,Sí.)))⊢ ⊢ О О x()∃ ∃ Sí.()p()x,Sí.))){displaystyle exists yleft(forall xleft(p(x,y)right)vdash forall xleft(exists yleft(p(x,y)right)right)}

Para algo más interesante probaremos ()()A→ → ()BAlternativa Alternativa C))→ → ()()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)→ → ¬ ¬ A)){displaystyle {left(left(Arightarrow left(Blor Cright)rightarrow left(left(left(Brightarrow lnot Aright)land lnot Cright)rightarrow lnot Aright)}}}}. Es sencillo encontrar la derivación, que ejemplifica la utilidad de LK en la prueba automatizada.

()I){displaystyle (I)} A⊢ ⊢ A{displaystyle Avdash A} ()¬ ¬ R){displaystyle (lnot R)} ⊢ ⊢ ¬ ¬ A,A{displaystyle vdash lnot A,A} ()PR){displaystyle (PR)} ⊢ ⊢ A,¬ ¬ A{displaystyle vdash A,lnot A} ()I){displaystyle (I)} B⊢ ⊢ B{displaystyle Bvdash B} ()I){displaystyle (I)} C⊢ ⊢ C{displaystyle Cvdash C} ()Alternativa Alternativa L){displaystyle (lor L)} BAlternativa Alternativa C⊢ ⊢ B,C{displaystyle Blor Cvdash B,C} ()PR){displaystyle (PR)} BAlternativa Alternativa C⊢ ⊢ C,B{displaystyle Blor Cvdash C,B} ()¬ ¬ L){displaystyle (lnot L)} BAlternativa Alternativa C,¬ ¬ C⊢ ⊢ B{displaystyle Blor C,lnot Cvdash B} ()I){displaystyle (I)} ¬ ¬ A⊢ ⊢ ¬ ¬ A{displaystyle lnot Avdash lnot A} ()→ → L){displaystyle (rightarrow L)} ()BAlternativa Alternativa C),¬ ¬ C,()B→ → ¬ ¬ A)⊢ ⊢ ¬ ¬ A{displaystyle left(Blor Cright),lnot C,left(Brightarrow lnot Aright)vdash lnot A} ()∧ ∧ L1){displaystyle (land L_{1})} ()BAlternativa Alternativa C),¬ ¬ C,()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)⊢ ⊢ ¬ ¬ A{displaystyle left(Blor Cright),lnot C,left(left(Brightarrow lnot Aright)land lnot Cright)vdash lnot A} ()PL){displaystyle (PL)} ()BAlternativa Alternativa C),()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C),¬ ¬ C⊢ ⊢ ¬ ¬ A{displaystyle left(Blor Cright),left(left(Brightarrow lnot Aright)land lnot Cright),lnot Cvdash lnot A} ()∧ ∧ L2){displaystyle (land L_{2})} ()BAlternativa Alternativa C),()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C),()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)⊢ ⊢ ¬ ¬ A{displaystyle left(Blor Cright),left(left(Brightarrow lnot Aright)land lnot Cright),left(left(Brightarrow lnot Aright)land lnot Cright)vdash lnot A} ()CL){displaystyle (CL)} ()BAlternativa Alternativa C),()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)⊢ ⊢ ¬ ¬ A{displaystyle left(Blor Cright),left(left(Brightarrow lnot Aright)land lnot Cright)vdash lnot A} ()PL){displaystyle (PL)} ()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C),()BAlternativa Alternativa C)⊢ ⊢ ¬ ¬ A{displaystyle left(left(Brightarrow lnot Aright)land lnot Cright),left(Blor Cright)vdash lnot A}		()→ → L){displaystyle (rightarrow L)}
()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C),()A→ → ()BAlternativa Alternativa C))⊢ ⊢ ¬ ¬ A,¬ ¬ A{displaystyle left(left(Brightarrow lnot Aright)land lnot Cright),left(Arightarrow left(Blor Cright)vdash lnot A,lnot A}
		()CR){displaystyle (CR)}
()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C),()A→ → ()BAlternativa Alternativa C))⊢ ⊢ ¬ ¬ A{displaystyle left(left(Brightarrow lnot Aright)land lnot Cright),left(Arightarrow left(Blor Cright)vdash lnot A}
		()PL){displaystyle (PL)}
()A→ → ()BAlternativa Alternativa C)),()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)⊢ ⊢ ¬ ¬ A{displaystyle left(Arightarrow left(Blor Cright)left(left(Brightarrow lnot Aright)land lnot Cright)vdash lnot A}
		()→ → R){displaystyle (rightarrow R)}
()A→ → ()BAlternativa Alternativa C))⊢ ⊢ ()()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)→ → ¬ ¬ A){displaystyle left(Arightarrow left(Blor Cright)vdash left(left(left(left(Brightarrow lnot Aright)land lnot Cright)rightarrow lnot Aright)}
		()→ → R){displaystyle (rightarrow R)}
⊢ ⊢ ()()A→ → ()BAlternativa Alternativa C))→ → ()()()B→ → ¬ ¬ A)∧ ∧ ¬ ¬ C)→ → ¬ ¬ A)){displaystyle vdash left(left(Arightarrow left(Blor Cright)rightarrow left(left(left(Brightarrow lnot Aright)land lnot Cright)rightarrow lnot Aright)right

Estas derivaciones también enfatizan la estructura estrictamente formal del cálculo secuencial. 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 secuente, en lugar de secuencias, lo que elimina la necesidad de una regla de permutación explícita. Esto corresponde a desplazar la conmutatividad de suposiciones y derivaciones fuera del cálculo de secuencias, mientras que LK lo integra dentro del propio sistema.

Relación con cuadros analíticos

Para ciertas formulaciones (es decir, variantes) del cálculo secuencial, una prueba en dicho cálculo es isomorfa a un cuadro analítico cerrado al revés.

Reglas estructurales

Las reglas estructurales merecen una discusión adicional.

El debilitamiento (W) permite agregar 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 importa ni el orden (P) ni la multiplicidad de ocurrencias (C) de los elementos de las secuencias. Por lo tanto, uno podría en lugar de secuencias también considerar conjuntos.

Sin embargo, el esfuerzo extra de usar secuencias está justificado ya que se pueden omitir parte o todas las reglas estructurales. Al hacerlo, se obtienen las llamadas lógicas subestructurales.

Propiedades del sistema LK

Este sistema de reglas puede demostrarse ser a la vez sólido y completo con respecto a la lógica de primer orden, es decir, una declaración A{displaystyle A} sigue semánticamente de un conjunto de locales .. {displaystyle "Gamma" ().. ⊨ ⊨ A){displaystyle (Gamma vDash A)} si y sólo si la secuencia .. ⊢ ⊢ A{displaystyle #Gamma vdash A} puede derivarse de las reglas anteriores.

En el cálculo secuente, la regla de corte es admisible. Este resultado también se denomina Hauptsatz de Gentzen ("Teorema principal").

Variantes

Las reglas anteriores se pueden modificar de varias formas:

Alternativas estructurales menores

Hay cierta libertad de elección con respecto a los detalles técnicos de cómo se formalizan las secuencias y las reglas estructurales. Siempre que cada derivación en LK pueda transformarse efectivamente en una derivación utilizando las nuevas reglas y viceversa, las reglas modificadas aún pueden llamarse LK.

En primer lugar, como se mencionó anteriormente, se puede ver que las secuencias consisten en conjuntos o conjuntos múltiples. En este caso, las reglas para permutar y (cuando se usan conjuntos) las fórmulas de contratación están obsoletas.

La regla del debilitamiento será admisible, cuando el axioma (I) sea cambiado, de tal manera que cualquier secuencia de la forma .. ,A⊢ ⊢ A,Δ Δ {displaystyle GammaAvdash A,Delta } se puede concluir. Esto significa que A{displaystyle A} prueba A{displaystyle A} en cualquier contexto. Cualquier debilitamiento que aparece en una derivación puede ser realizado justo al principio. Esto puede ser un cambio conveniente al construir pruebas de abajo hacia arriba.

Independiente de éstos también puede cambiar la forma en que los contextos se dividen dentro de las reglas: En los casos ()∧ ∧ R),()Alternativa Alternativa L){displaystyle ({land }R),({lor }L)}, y ()→ → L){displaystyle ({rightarrow }L)} el contexto izquierdo se divide de alguna manera .. {displaystyle "Gamma" y .. {displaystyle Sigma } cuando va hacia arriba. Dado que la contracción permite la duplicación de estos, se puede suponer que el contexto completo se utiliza en ambas ramas de la derivación. Al hacer esto, se asegura que no se pierden locales importantes en la rama equivocada. Utilizando el debilitamiento, las partes irrelevantes del contexto se pueden eliminar más adelante.

Absurdo

Uno puede presentar ⊥ ⊥ {displaystyle bot }, la constante absurda representando falso, con el axioma:

⊥ ⊥ ⊢ ⊢ {displaystyle {cfrac {}{bot vdash quad}}}

O si, como se describe arriba, el debilitamiento debe ser una regla admisible, entonces con el axioma:

.. ,⊥ ⊥ ⊢ ⊢ Δ Δ {displaystyle {cfrac {fnh}{fnh} {fnMicrosoft} {fnh} {fn}} {fnK}}} {fnK}} {fnK}}}}}} {fnf}}fnf}fnKfnKf}}}}}}}\\fnKfnKfnKfnKfnKfnKfnKfnKfnKfnKf}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}\\\\\\fnKfnKfnK\fnKfnKfnKfnKfnKfnKfnKfnKfnKf}}}}}}}}}}}}}}} Gammabot vdash Delta }}

Con ⊥ ⊥ {displaystyle bot }, la negación puede subsumirse como un caso especial de implicación, a través de la definición ()¬ ¬ A)⟺ ⟺ ()A→ → ⊥ ⊥ ){displaystyle (neg A)iff (Ato 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. Por lo general, son más débiles que LK (es decir, tienen menos teoremas) y, por lo tanto, no están 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 secuente intuitivo: Sistema LJ

Sorprendentemente, algunos pequeños cambios en las reglas de LK bastan para convertirlo en un sistema de prueba de lógica intuitiva. Para ello, hay que restringir a los secuestrantes con la mayor parte de una fórmula de la mano derecha, y modificar las reglas para mantener este invariante. Por ejemplo, ()Alternativa Alternativa L){displaystyle ({lor }L)} se reformula como sigue (donde C es una fórmula arbitraria):

.. ,A⊢ ⊢ C.. ,B⊢ ⊢ C.. ,.. ,AAlternativa Alternativa B⊢ ⊢ C()Alternativa Alternativa L){displaystyle {cfrac {GammaAvdash CqquadSigmaBvdash C}{GammaSigmaAlor Bvdash 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 corte similar. Esto se puede usar para probar las propiedades de disyunción y existencia.

De hecho, las únicas reglas en LK que necesitan ser restringidas a consejeras de una sola forma son ()→ → R){displaystyle ({to }R)}, ()¬ ¬ R){displaystyle (neg R)} (que se puede ver como un caso especial → → R{displaystyle {to }R}, como se describe anteriormente) y ()О О R){displaystyle ({forall }R)}. Cuando los consequentes multiformula se interpretan como disyunciones, todas las otras reglas de inferencia de LK son derivadas en LJ, mientras que las reglas ()→ → R){displaystyle ({to }R)} y ()О О R){displaystyle ({forall }R)} se convirtió en

.. ,A⊢ ⊢ BAlternativa Alternativa C.. ⊢ ⊢ ()A→ → B)Alternativa Alternativa C{displaystyle {cfrac {GamaAvdash Blor C}{ Gamma vdash (Ato B)lor C}}

y cuando Sí.{displaystyle y} no se produce libre en el fondo secuenciado)

.. ⊢ ⊢ A[Sí./x]Alternativa Alternativa C.. ⊢ ⊢ ()О О xA)Alternativa Alternativa C.{displaystyle {cfrac {Gammavdash A[y/x]lor C}{ Gamma vdash (forall xA)lor C}}

Estas reglas no son intuitivamente válidas.