En lógica matemática , un secuente es un tipo muy general de afirmación condicional.
Un consecuente puede tener cualquier número m de fórmulas de condición Ai (llamadas " antecedentes ") y cualquier número n de fórmulas afirmadas Bj ( llamadas "sucedentes" o " consecuentes "). Se entiende por consecuente que si todas las condiciones antecedentes son verdaderas, entonces al menos una de las fórmulas consecuentes es verdadera. Este estilo de afirmación condicional casi siempre se asocia con el marco conceptual del cálculo secuencial .
Las secuencias se entienden mejor en el contexto de los siguientes tres tipos de juicios lógicos :
Por tanto, los secuenciales son una generalización de afirmaciones condicionales simples, que a su vez son una generalización de afirmaciones incondicionales.
La palabra "OR" aquí es OR inclusivo . [1] La motivación para la semántica disyuntiva en el lado derecho de un secuente proviene de tres beneficios principales.
Estos tres beneficios fueron identificados en el documento fundacional de Gentzen (1934, p. 194).
No todos los autores se han adherido al significado original de Gentzen para la palabra "secuente". Por ejemplo, Lemmon (1965) utilizó la palabra "secuente" estrictamente para afirmaciones condicionales simples con una y sólo una fórmula consecuente. [2] La misma definición de consecuente único para un secuente la dan Huth y Ryan 2004, p. 5.
En un secuencial general de la forma
tanto Γ como Σ son secuencias de fórmulas lógicas, no conjuntos . Por lo tanto, tanto el número como el orden de aparición de las fórmulas son significativos. En particular, la misma fórmula podrá aparecer dos veces en la misma secuencia. El conjunto completo de reglas de inferencia de cálculo secuencial contiene reglas para intercambiar fórmulas adyacentes a la izquierda y a la derecha del símbolo de afirmación (y, por lo tanto, permutar arbitrariamente las secuencias izquierda y derecha), y también para insertar fórmulas arbitrarias y eliminar copias duplicadas dentro de la izquierda. y las secuencias correctas. (Sin embargo, Smullyan (1995, págs. 107-108) utiliza conjuntos de fórmulas en secuencias en lugar de secuencias de fórmulas. En consecuencia, los tres pares de reglas estructurales llamados "adelgazamiento", "contracción" e "intercambio" no son necesarios).
El símbolo ' ' a menudo se denomina " torniquete ", "viraje derecho", "te", "signo de afirmación" o "símbolo de afirmación". A menudo se lee, sugerentemente, como "cede", "prueba" o "implica".
Dado que cada fórmula en el antecedente (el lado izquierdo) debe ser verdadera para concluir la verdad de al menos una fórmula en el sucedente (el lado derecho), agregar fórmulas a cada lado da como resultado una secuencia más débil, mientras que eliminarlas de cada lado da como resultado uno más fuerte. Esta es una de las ventajas de simetría que se deriva del uso de la semántica disyuntiva en el lado derecho del símbolo de afirmación, mientras que la semántica conjuntiva se adhiere en el lado izquierdo.
En el caso extremo de que la lista de fórmulas antecedentes de un secuente esté vacía, el consecuente es incondicional. Esto difiere de la simple afirmación incondicional porque el número de consecuentes es arbitrario, no necesariamente un consecuente único. Así, por ejemplo, ' ⊢ B 1 , B 2 ' significa que B 1 , B 2 o ambos deben ser verdaderos. Una lista de fórmulas de antecedentes vacía es equivalente a la proposición "siempre verdadera", llamada " verum ", denotada "⊤". (Ver Tee (símbolo) .)
En el caso extremo en que la lista de fórmulas consecuentes de un secuente esté vacía, la regla sigue siendo que al menos un término de la derecha sea verdadero, lo cual es claramente imposible . Esto está representado por la proposición "siempre falsa", llamada " falsum ", denotada "⊥". Como la consecuencia es falsa, al menos uno de los antecedentes debe ser falso. Así, por ejemplo, ' A 1 , A 2 ⊢' significa que al menos uno de los antecedentes A 1 y A 2 debe ser falso.
Se ve aquí nuevamente una simetría debido a la semántica disyuntiva en el lado derecho. Si el lado izquierdo está vacío, entonces una o más proposiciones del lado derecho deben ser verdaderas. Si el lado derecho está vacío, entonces una o más de las proposiciones del lado izquierdo deben ser falsas.
El caso doblemente extremo ' ⊢ ', donde tanto la lista de fórmulas antecedente como consecuente están vacías, es " no satisfacible ". [3] En este caso, el significado del secuente es efectivamente ' ⊤ ⊢ ⊥ '. Esto es equivalente al secuente ' ⊢ ⊥ ', que claramente no puede ser válido.
Un consecuente de la forma ' ⊢ α, β ', para fórmulas lógicas α y β, significa que α es verdadera o β es verdadera (o ambas). Pero eso no significa que α sea una tautología o β sea una tautología. Para aclarar esto, considere el ejemplo ' ⊢ B ∨ A, C ∨ ¬A '. Este es un secuente válido porque B ∨ A es verdadero o C ∨ ¬A es verdadero. Pero ninguna de estas expresiones es una tautología aisladamente. Es la disyunción de estas dos expresiones lo que constituye una tautología.
De manera similar, un consecuente de la forma ' α, β ⊢ ', para fórmulas lógicas α y β, significa que α es falso o β es falso. Pero eso no significa que α sea una contradicción o β sea una contradicción. Para aclarar esto, considere el ejemplo 'B ∧ A, C ∧ ¬A ⊢'. Este es un secuente válido porque B ∧ A es falso o C ∧ ¬A es falso. Pero ninguna de estas expresiones es una contradicción aisladamente. Es la conjunción de estas dos expresiones lo que constituye una contradicción.
La mayoría de los sistemas de prueba proporcionan formas de deducir un secuente de otro. Estas reglas de inferencia están escritas con una lista de secuentes encima y debajo de una línea . Esta regla indica que si todo lo que está encima de la línea es verdadero, también lo es todo lo que está debajo de la línea.
Una regla típica es:
Esto indica que si podemos deducir que eso rinde , y eso rinde , entonces también podemos deducir que eso rinde . (Consulte también el conjunto completo de reglas de inferencia del cálculo secuente ).
El símbolo de afirmación en los secuentes originalmente significaba exactamente lo mismo que el operador de implicación. Pero con el tiempo, su significado ha cambiado para significar demostrabilidad dentro de una teoría en lugar de verdad semántica en todos los modelos.
En 1934, Gentzen no definió el símbolo de afirmación ' ⊢ ' en un secuente para indicar demostrabilidad. Lo definió para que significara exactamente lo mismo que el operador de implicación ' ⇒ '. Utilizando ' → ' en lugar de ' ⊢ ' y ' ⊃ ' en lugar de ' ⇒ ', escribió: "El consecuente A 1 , ..., A μ → B 1 , ..., B ν significa, en cuanto a contenido, exactamente igual que la fórmula (A 1 & ... & A μ ) ⊃ (B 1 ∨ ... ∨ B ν )". [4] (Gentzen empleó el símbolo de la flecha hacia la derecha entre los antecedentes y los consecuentes de los siguientes. Empleó el símbolo ' ⊃ ' para el operador de implicación lógica).
En 1939, Hilbert y Bernays afirmaron igualmente que un secuente tiene el mismo significado que la fórmula de implicación correspondiente. [5]
En 1944, Alonzo Church enfatizó que las siguientes afirmaciones de Gentzen no significaban demostrabilidad.
Numerosas publicaciones posteriores a esta época han afirmado que el símbolo de afirmación en los secuentes significa demostrabilidad dentro de la teoría donde se formulan los secuentes. Curry en 1963, [7] Lemmon en 1965, [2] y Huth y Ryan en 2004 [8] afirman que el símbolo de afirmación secuencial significa demostrabilidad. Sin embargo, Ben-Ari (2012, p. 69) afirma que el símbolo de afirmación en los secuenciales del sistema Gentzen, que denota como ' ⇒ ', es parte del lenguaje objeto, no del metalenguaje. [9]
Según Prawitz (1965): "Los cálculos de secuentes pueden entenderse como metacálculos para la relación de deducibilidad en los correspondientes sistemas de deducción natural". [10] Y además: "Una prueba en un cálculo de secuentes puede considerarse como una instrucción sobre cómo construir una deducción natural correspondiente". [11] En otras palabras, el símbolo de afirmación es parte del lenguaje objeto del cálculo secuente, que es una especie de metacálculo, pero al mismo tiempo significa deducibilidad en un sistema de deducción natural subyacente.
Un secuente es una declaración formalizada de demostrabilidad que se utiliza con frecuencia al especificar cálculos para la deducción . En el cálculo secuente, se utiliza el nombre de secuente para el constructo, que puede considerarse como un tipo específico de juicio , característico de este sistema de deducción.
El significado intuitivo del secuente es que bajo el supuesto de Γ la conclusión de Σ es demostrable. Clásicamente, las fórmulas de la izquierda del torniquete pueden interpretarse de forma conjuntiva mientras que las fórmulas de la derecha pueden considerarse como una disyunción . Esto significa que, cuando todas las fórmulas en Γ son válidas, entonces al menos una fórmula en Σ también tiene que ser verdadera. Si el sucesor es vacío, esto se interpreta como falsedad, es decir, significa que Γ prueba la falsedad y, por tanto, es inconsistente. Por otro lado, se supone que un antecedente vacío es verdadero, es decir, significa que Σ sigue sin ninguna suposición, es decir, siempre es verdadero (como una disyunción). Un secuente de esta forma, con Γ vacío, se conoce como aserción lógica .
Por supuesto, son posibles otras explicaciones intuitivas que son clásicamente equivalentes. Por ejemplo, puede leerse como una afirmación de que no puede darse el caso de que cada fórmula en Γ sea verdadera y cada fórmula en Σ sea falsa (esto está relacionado con las interpretaciones de doble negación de la lógica intuicionista clásica , como el teorema de Glivenko ).
En cualquier caso, estas lecturas intuitivas son sólo pedagógicas. Dado que las pruebas formales en la teoría de la prueba son puramente sintácticas , el significado de (la derivación de) un secuente sólo viene dado por las propiedades del cálculo que proporciona las reglas reales de inferencia .
Salvo contradicciones en la definición técnicamente precisa anterior, podemos describir los secuentes en su forma lógica introductoria. representa un conjunto de supuestos con los que comenzamos nuestro proceso lógico, por ejemplo "Sócrates es un hombre" y "Todos los hombres son mortales". Esto representa una conclusión lógica que se sigue bajo estas premisas. Por ejemplo, "Sócrates es mortal" se desprende de una formalización razonable de los puntos anteriores y podríamos esperar verlo en el lado del torniquete . En este sentido, significa el proceso de razonamiento, o "por lo tanto" en inglés.
La noción general de secuente presentada aquí puede especializarse de varias maneras. Se dice que un secuente es intuicionista si hay como máximo una fórmula en el sucedente (aunque también son posibles los cálculos multisucedentes para la lógica intuicionista). Más precisamente, la restricción del cálculo de secuentes generales a sucesivos de fórmula sucesiva única, con las mismas reglas de inferencia que para los secuentes generales, constituye un cálculo de secuentes intuicionista. (Este cálculo secuencial restringido se denomina LJ.)
De manera similar, se pueden obtener cálculos para la lógica intuicionista dual (un tipo de lógica paraconsistente ) exigiendo que los secuentes sean singulares en el antecedente.
En muchos casos, también se supone que las secuencias constan de conjuntos múltiples o conjuntos en lugar de secuencias. Por tanto, se ignora el orden o incluso el número de apariciones de las fórmulas. Para la lógica proposicional clásica esto no supone un problema, ya que las conclusiones que se pueden extraer de un conjunto de premisas no dependen de estos datos. Sin embargo, en lógica subestructural esto puede llegar a ser bastante importante.
Los sistemas de deducción natural utilizan afirmaciones condicionales de consecuencia única, pero normalmente no utilizan los mismos conjuntos de reglas de inferencia que Gentzen introdujo en 1934. En particular, los sistemas de deducción natural tabulares , que son muy convenientes para la demostración práctica de teoremas en cálculo proposicional y predicados. cálculo, fueron aplicados por Suppes (1999) y Lemmon (1965) para enseñar lógica introductoria en libros de texto.
Históricamente, Gerhard Gentzen introdujo los secuentes para especificar su famoso cálculo de secuentes . [12] En su publicación alemana utilizó la palabra "Sequenz". Sin embargo, en inglés, la palabra " secuencia " ya se utiliza como traducción del alemán "Folge" y aparece con bastante frecuencia en matemáticas. El término "sequent" ha sido creado en busca de una traducción alternativa de la expresión alemana.
Kleene [13] 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'. ".
