En lógica matemática , el cálculo secuencial es, en esencia, un estilo de argumentación lógica formal en el que cada línea de una prueba es una tautología condicional (llamada secuencial por Gerhard Gentzen ) en lugar de una tautología incondicional. Cada tautología condicional se infiere de otras tautologías condicionales en líneas anteriores en un argumento formal de acuerdo con reglas y procedimientos de inferencia , dando una mejor aproximación al estilo natural de deducción utilizado por los matemáticos que el estilo anterior de lógica formal de David Hilbert.donde cada línea era una tautología incondicional. Puede que haya que hacer distinciones más sutiles; por ejemplo, puede haber axiomas no lógicos de los que todas las proposiciones dependen implícitamente. Entonces, los secuentes significan teoremas condicionales en un lenguaje de primer orden en lugar de tautologías condicionales.
El cálculo secuencial es uno de los varios estilos existentes de cálculo de prueba para expresar argumentos lógicos línea por línea.
- Estilo Hilbert . Cada línea es una tautología (o teorema) incondicional.
- Estilo Gentzen. 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 secuencial son tipos particulares de sistemas de estilo Gentzen. Los sistemas de estilo Hilbert suelen tener un número muy pequeño de reglas de inferencia, que se basan más en conjuntos de axiomas. Los sistemas de estilo Gentzen suelen tener muy pocos axiomas, si los hay, que 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 el sistema de deducción natural como el 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 las expresiones no cuantificadas (que normalmente contienen variables libres), y luego se reintroducen los cuantificadores. Esto es muy similar a la forma en que los matemáticos llevan a cabo 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 breves. Los sistemas de deducción natural son más adecuados para la demostración práctica de teoremas. Los sistemas de cálculo secuencial son más adecuados para el análisis teórico.
Descripción general
En la teoría de la prueba 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 [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 consistencia . Gentzen demostró ademá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 este primer trabajo, 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 automática. .
Sistemas de deducción al estilo de Hilbert
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 usa en los sistemas de deducción al estilo de Hilbert , donde un juicio tiene la forma
dónde 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 final 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.
El precio que se paga por la sintaxis simple de un sistema al estilo de Hilbert es que las pruebas 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 la deducción como regla formal en el sistema, lo que ocurre en la deducción natural .
Sistemas de deducción natural
En la deducción natural, los juicios tienen la forma
donde el 'arena son de nuevo fórmulas y . Permutaciones de lason inmateriales. En otras palabras, un juicio consiste en una lista (posiblemente vacía) de fórmulas en el lado izquierdo de un símbolo de torniquete "", con una sola fórmula en el lado derecho. [8] [9] [10] Los teoremas son esas fórmulas tal que (con un lado izquierdo vacío) es la conclusión de una prueba válida. (En algunas presentaciones de deducción natural, lasy el torniquete no están escritos explícitamente; en su lugar, se utiliza una notación bidimensional de la que se pueden inferir).
La semántica estándar de un juicio en deducción natural es que afirma que siempre que [11] , , etc., son todas verdaderas, también será cierto. Los juicios
y
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 para
un objeto sintáctico llamado secuente. Las fórmulas del lado izquierdo del torniquete se denominan antecedentes , y las fórmulas del lado derecho se denominan sucesivas o consecuentes ; juntos se denominan cedentes o secuelas . [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 dónde 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 es cierto, al menos uno también será cierto. [13] Por lo tanto, 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 un "y", y una coma a la derecha del torniquete debe considerarse como un (inclusive) "o". Los secuentes
y
son equivalentes en el sentido fuerte de que una prueba de uno puede extenderse a una prueba del otro.
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 al principio es confuso que la coma parece significar cosas completamente diferentes en los dos lados de la deducción. torniquete. Sin embargo, en un contexto clásico, la semántica del secuente también puede (por tautología proposicional) expresarse como
(al menos una de las A es falsa, o una de las B es verdadera) o como
(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 a cada lado del torniquete es que se niega un lado. Por lo tanto, cambiar de izquierda a derecha en una secuencia 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 de secuencia de izquierda a derecha y, de hecho, las reglas de inferencia en el cálculo de secuencia para tratar la conjunción (∧) son imágenes espejo de aquellos que se ocupan de la disyunción (∨).
Muchos lógicos sienten [ cita requerida ] que esta presentación simétrica ofrece una visión más profunda de la estructura de la lógica que otros estilos de 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 NJ era algo feo. [15] Dijo que el papel especial del medio excluido en el sistema clásico de deducción natural NK se elimina en el sistema de cálculo secuencial clásico LK. [16] Dijo que el cálculo secuencial LJ dio más simetría que la deducción natural NJ en el caso de la lógica intuicionista, como también en el caso de la lógica clásica (LK versus NK). [17] Luego dijo que además de estas razones, el cálculo secuencial con múltiples fórmulas sucesivas está destinado particularmente a su teorema principal ("Hauptsatz"). [18]
Origen de la palabra "secuencia"
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 'secuencia', porque ya hemos usado 'secuencia' para cualquier sucesión de objetos, donde el alemán es 'Folge' . " [19]
Demostrar fórmulas lógicas
Á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. [20]
Considere la siguiente fórmula:
Esto está escrito en la siguiente forma, donde la proposición que necesita ser probada está a la derecha del símbolo del torniquete :
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, uno pasa al siguiente secuela:
Nuevamente, el lado derecho incluye una implicación, cuya premisa puede asumirse además de modo que solo se necesita probar su conclusión:
Dado que se supone que los argumentos en el lado izquierdo están relacionados por conjunción , esto puede ser reemplazado por lo siguiente:
Esto equivale a probar la conclusión en ambos casos de la disyunción en el primer argumento de la izquierda. Por lo tanto, podemos dividir el secuente en dos, donde ahora tenemos que probar cada uno por separado:
En el caso del primer juicio, reescribimos como y vuelve a dividir el secuente para obtener:
El segundo secuela está hecho; la primera secuencia se puede simplificar aún más en:
Este proceso siempre 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 deseamos probar; las hojas constan únicamente de fórmulas atómicas. El árbol se conoce como árbol de reducción . [20] [22]
Se entiende que los elementos de 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 secuente 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 en la izquierda.
Las siguientes son las reglas por las cuales uno 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, se puede cambiar libremente el orden de los argumentos en cada lado; Γ y Δ representan posibles argumentos adicionales. [20]
El término habitual para la línea horizontal que se utiliza en los diseños de estilo Gentzen para la deducción natural es línea de inferencia . [23]
Izquierda: | Derecha: |
regla: | regla: |
regla: | regla: |
regla: | regla: |
regla: | regla: |
Axioma: | |
|
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 cada operador lógico aparece en una de las reglas anteriores y es eliminado por la regla, el proceso termina cuando no quedan operadores lógicos: la fórmula se ha descompuesto .
Así, las secuelas en las hojas de los árboles incluyen sólo símbolos atómicos, que son demostrables por el axioma o no, según si uno de los símbolos de la derecha aparece también en 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 hay una división. También es obvio que un axioma es demostrable si y solo si es verdadero para cada 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 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 puede probarse en estos tiene un árbol de reducción.
Esto se puede mostrar 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 axiomas produce una fórmula lógica verdadera y, por lo tanto, puede probarse en el cálculo secuencial; A continuación se muestran ejemplos de estos . 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 introduce las reglas del cálculo secuencial LK tal como las introdujo Gentzen en 1934. (LK, de manera poco intuitiva, significa " k lassische Prädikaten l ogik".) [24] Una prueba (formal) en este cálculo es una secuencia de secuelas, donde cada una de las secuencias se deriva de las secuencias que aparecen anteriormente en la secuencia mediante el uso de una de las reglas siguientes.
Reglas de inferencia
Se utilizará la siguiente notación:
- conocido como el torniquete , separa los supuestos de la izquierda de las proposiciones de la derecha
- y denotar fórmulas de lógica de predicados de primer orden (también se puede restringir esto a la lógica proposicional),
- , y son secuencias finitas (posiblemente vacías) de fórmulas (de hecho, el orden de las fórmulas no importa; consulte la subsección Reglas estructurales ), llamadas contextos,
- cuando a la izquierda del, la secuencia de fórmulas se considera conjuntivamente (se supone que todas son válidas al mismo tiempo),
- mientras que a la derecha de la, la secuencia de fórmulas se considera disyuntivamente (al menos una de las fórmulas debe ser válida para cualquier asignación de variables),
- denota un término arbitrario,
- y denotar variables.
- Se dice que una variable ocurre libre dentro de una fórmula si ocurre fuera del alcance de los cuantificadores. o .
- denota la fórmula que se obtiene sustituyendo el término por cada ocurrencia libre de la variable en fórmula con la restricción de que el término debe ser libre para la variable en (es decir, no ocurre ninguna variable en se vuelve atado en ).
- , , , , , : Estos seis representan las dos versiones de cada una de las tres reglas estructurales; uno para usar a la izquierda ('L') de un, y el otro a su derecha ('R'). Las reglas se abrevian 'W' para debilitamiento (izquierda / derecha) , 'C' para contracción y 'P' para permutación .
Tenga en cuenta que, contrariamente a las reglas para avanzar a lo largo del árbol de reducción presentadas 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 relativas a la cuantificación .
Axioma: | Cortar: |
|
|
Reglas lógicas de la izquierda: | Reglas lógicas correctas: |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reglas estructurales izquierdas: | Reglas estructurales correctas: |
|
|
|
|
|
|
Restricciones: en las reglas y , La variable no debe aparecer libre en ninguna parte de las respectivas secuencias inferiores.
Una explicación intuitiva
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. . Por el contrario, las reglas estructurales operan 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 la regla de (Cortar).
Aunque expresadas de manera formal, las reglas anteriores permiten una lectura muy intuitiva en términos de lógica clásica. Considere, por ejemplo, la regla. Dice que, siempre que se pueda probar que se puede concluir a partir de una secuencia de fórmulas que contienen , entonces también se puede concluir de la suposición (más fuerte) de que sostiene. Asimismo, la regla afirma que, si y basta para concluir , luego de solo uno puede concluir o debe ser falso, es decir sostiene. Todas las reglas se pueden interpretar de esta manera.
Para tener una intuición sobre las reglas del cuantificador, considere la regla . Por supuesto concluyendo que se sostiene solo por el hecho de que es verdad no es posible en general. Sin embargo, si la variable y no se menciona en otra parte (es decir, todavía se puede elegir libremente, sin influir en las otras fórmulas), entonces se puede suponer quese mantiene para cualquier valor de y. Las otras reglas deberían ser bastante sencillas.
En lugar de ver las reglas como descripciones de derivaciones legales en la lógica de predicados, también se pueden considerar como instrucciones para la construcción de una prueba para un enunciado dado. En este caso, las reglas se pueden leer de abajo hacia arriba; por ejemplo, dice eso, para probar que se desprende de los supuestos y , basta para 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 se dividirá en y . Sin embargo, solo hay un número finito de posibilidades para verificar, ya que el antecedente por supuesto es finito. Esto también ilustra cómo se puede considerar que la teoría de la prueba opera sobre las pruebas de una manera combinatoria: pruebas dadas para ambas y , uno puede construir una prueba para .
Al buscar alguna prueba, la mayoría de las reglas ofrecen recetas más o menos directas de cómo hacer esto. La regla de corte es diferente: establece que, cuando una fórmula se puede concluir y esta fórmula también puede servir como premisa para concluir otras declaraciones, entonces la fórmula se puede "cortar" y se unen 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 lo tanto, crucial para las aplicaciones del cálculo secuencial en la deducción automática : establece que todos los usos de la regla de corte pueden eliminarse de una demostración, lo que implica que cualquier secuencia demostrable puede recibir una prueba sin cortes .
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 algo redundante: la integridad de las secuencias iniciales atómicas establece que la regla puede restringirse a fórmulas atómicas sin ninguna 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 conector "no está implícito por".ésa sería la doble 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.
Derivaciones de ejemplo
Aquí está la derivación de "", conocida como la Ley del medio excluido ( tertium non datur en latín).
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 derivarlo de abajo hacia arriba, porque una variable libre existente no se puede usar en sustitución en las reglas y .
Para algo más interesante probaremos . Es sencillo encontrar la derivación, que ejemplifica la utilidad de LK en pruebas automatizadas.
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. Sin embargo, tenga en cuenta 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, eliminando la necesidad de una regla de permutación explícita. Esto corresponde a la conmutatividad cambiante de supuestos y derivaciones fuera del cálculo secuencial, mientras que LK lo incrusta dentro del sistema mismo.
Relación con cuadros analíticos
Para ciertas formulaciones (es decir, variantes) del cálculo secuencial, una demostración en dicho cálculo es isomórfica a un cuadro analítico cerrado al revés . [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 siguiente 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 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 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
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 declaraciónsigue semánticamente de un conjunto de premisas si y solo si el secuentepuede derivarse de las reglas anteriores. [26]
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 formas:
Alternativas estructurales menores
Existe 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 se pueden llamar LK.
En primer lugar, como se mencionó anteriormente, las secuencias se pueden ver como conjuntos o conjuntos múltiples . En este caso, las reglas para la permutación y (cuando se usan conjuntos) las fórmulas de contratación son obsoletas.
La regla del debilitamiento será admisible, cuando se cambie el axioma (I), de modo que cualquier secuela de la forma se puede concluir. Esto significa que prueba en cualquier contexto. Cualquier debilitamiento que aparezca en una derivación se puede realizar desde el principio. Este puede ser un cambio conveniente al construir pruebas de abajo hacia arriba.
Independientemente de estos, también puede cambiar la forma en que los contextos se dividen dentro de las reglas: En los casos , y el contexto de la izquierda se divide de alguna manera en y al subir. Dado que la contracción permite la duplicación de estos, se puede suponer que se usa el contexto completo en ambas ramas de la derivación. Al hacer esto, se asegura que no se pierdan premisas importantes en la rama equivocada. Usando el debilitamiento, las partes irrelevantes del contexto pueden eliminarse más tarde.
Absurdo
Uno puede introducir , la constante del absurdo que representa falso , con el axioma:
O si, como se describió anteriormente, el debilitamiento debe ser una regla admisible, entonces con el axioma:
Con , la negación se puede subsumir como un caso especial de implicación, a través de la definición .
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 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 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 ello, hay que limitarse a las secuencias con como máximo una fórmula en el lado derecho y modificar las reglas para mantener este invariante. Por ejemplo, se reformula de la siguiente manera (donde C es una fórmula arbitraria):
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 probar las propiedades de existencia y disyunción .
De hecho, las únicas dos reglas en LK que deben restringirse a los consecuentes de fórmula única son y [28] (y el último puede verse como un caso especial del primero, a través decomo se describió anteriormente). Cuando los consecuentes de múltiples fórmulas se interpretan como disyunciones, todas las demás reglas de inferencia de LK son realmente derivables en LJ, mientras que la regla infractora es
Esto equivale a la fórmula proposicional , una tautología clásica que no es constructivamente válida.
Ver también
- Cálculo circulante
- Cálculo secuencial anidado
- Resolución (lógica)
Notas
- ↑ a b Gentzen 1934 , Gentzen 1935 .
- ↑ a b Curry 1977 , pp. 208-213, da una prueba de 5 páginas del teorema de eliminación. Consulte también las páginas 188, 250.
- ↑ a b Kleene 2009 , pp. 453, da una prueba muy breve del teorema de eliminación de cortes.
- ^ Curry 1977 , págs. 189–244, denomina sistemas LC de Gentzen systems. El énfasis de Curry está más en la teoría que en las pruebas lógicas prácticas.
- ^ Kleene 2009 , págs. 440–516. Este libro está mucho más interesado en las implicaciones teóricas y metamatemáticas del cálculo secuencial al estilo de Gentzen que en las aplicaciones a las pruebas lógicas prácticas.
- ↑ Kleene 2002 , pp. 283-312, 331-361, define los sistemas de Gentzen y demuestra varios teoremas dentro de estos sistemas, incluido el teorema de completitud de Gödel y el teorema de Gentzen.
- ^ 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.
- ^ Curry 1977 , págs. 184–244, compara los sistemas de deducción natural, denotados LA, y los sistemas Gentzen, denotados LC. El énfasis de Curry es más teórico que práctico.
- ↑ Suppes 1999 , pp. 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 .
- ^ Lemmon 1965 es una introducción elemental a la deducción natural práctica basada en el conveniente estilo de diseño de prueba abreviado System L basado en Suppes 1999 , págs. 25-150.
- ^ Aquí, "siempre que" se usa como una abreviatura informal "para cada asignación de valores a las variables libres en el juicio"
- ^ Shankar, Natarajan ; Owre, Sam; Rushby, John M .; Stringer-Calvert, David WJ (1 de noviembre de 2001). "PVS Prover Guide" (PDF) . Guía de usuario . SRI Internacional . Consultado el 29 de mayo de 2015 .
- ↑ Para obtener explicaciones de la semántica disyuntiva del lado derecho de las secuelas, consulte Curry 1977 , págs. 189-190, Kleene 2002 , págs. 290, 297, Kleene 2009 , pág. 441, Hilbert y Bernays 1970 , pág. 385, Smullyan 1995 , págs. 104-105 y Gentzen 1934 , pág. 180.
- ^ Buss 1998 , p. 10
- ^ Gentzen 1934 , p. 188. "Der Kalkül NJ hat manche formale Unschönheiten".
- ^ Gentzen 1934 , p. 191. "En dem Klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten Eine Sonderstellung unter den Schlußweisen ein [...], er sich der indem Einführungs- und nicht Beseitigungssystematik einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben . "
- ^ Gentzen 1934 , p. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener".
- ^ Gentzen 1934 , p. 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 kanndeergher nichor vichor.
- ^ Kleene 2002 , p. 441.
- ^ a b c Lógica aplicada, Univ. de Cornell: Conferencia 9 . Última consulta: 25/06/2016
- ^ "Recuerde, la forma en que demuestra una implicación es asumiendo la hipótesis ". - Philip Wadler , el 2 de noviembre de 2015, en su Keynote: "Propositions as Types". Minuto 14:36 / 55: 28 del videoclip Code Mesh
- ^ Tait WW (2010). "Prueba de consistencia original de Gentzen y el teorema de la barra" (PDF) . En Kahle R, Rathjen M (eds.). Centenario de Gentzen: la búsqueda de la coherencia . Nueva York: Springer. págs. 213-228.
- ^ Jan von Platón, Elementos de razonamiento lógico , Cambridge University Press, 2014, p. 32.
- ^ Gentzen 1934 , págs. 190-193.
- ^ Smullyan 1995 , p. 107
- ^ Kleene 2002 , p. 336, escribió en 1967 que "fue un descubrimiento lógico importante de Gentzen 1934-5 que, cuando hay alguna 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 ".
- ^ Gentzen 1934 , p. 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. extraño ". Traducción al inglés: "La diferencia entre la lógica intuicionista y 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 sucesivas ".
- ^ Teoría de la prueba estructural (CUP, 2001), Sara Negri y Jan van Plato
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 .
- Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II" . Mathematische Zeitschrift . 39 (3): 405–431. doi : 10.1007 / bf01201363 .
- 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 la metamatemática . Ishi Press International. 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 . Thomas Nelson. ISBN 0-17-712040-1.
- Smullyan, Raymond Merrill (1995) [1968]. Lógica de primer orden . Nueva York: Publicaciones de Dover. ISBN 978-0-486-68370-6.
- Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-40687-9.
enlaces externos
- "Cálculo secuencial" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
- Un breve desvío: cálculo secuencial
- Tutorial interactivo del cálculo secuencial