En lógica matemática , un secuencial es un tipo muy general de afirmación condicional.
Un consecuente puede tener cualquier número m de fórmulas condicionales A i (llamadas " antecedentes ") y cualquier número n de fórmulas afirmadas B j (llamadas "sucedentes" o " consecuentes "). Se entiende que un consecuente significa 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 consecuente .
Las secuencias se entienden mejor en el contexto de los siguientes tres tipos de juicios lógicos :
Por lo tanto, los consecuentes son una generalización de aserciones condicionales simples, que son una generalización de aserciones incondicionales.
La palabra "OR" aquí es el OR inclusivo . [1] La motivación para la semántica disyuntiva en el lado derecho de un secuencial proviene de tres beneficios principales.
Los tres beneficios fueron identificados en el documento fundacional de Gentzen (1934, pág. 194).
No todos los autores se han adherido al significado original de Gentzen para la palabra "consecuente". Por ejemplo, Lemmon (1965) utilizó la palabra "consecuente" estrictamente para afirmaciones condicionales simples con una y sólo una fórmula consecuente. [2] La misma definición de consecuente único para un consecuente es dada por Huth y Ryan 2004, p. 5.
En una secuencia 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 puede aparecer dos veces en la misma secuencia. El conjunto completo de reglas de inferencia del cálculo de secuencias contiene reglas para intercambiar fórmulas adyacentes a la izquierda y a la derecha del símbolo de aserció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 las secuencias izquierda y derecha. (Sin embargo, Smullyan (1995, pp. 107-108), utiliza conjuntos de fórmulas en secuencias en lugar de secuencias de fórmulas. En consecuencia, los tres pares de reglas estructurales llamadas "adelgazamiento", "contracción" e "intercambio" no son necesarios).
El símbolo " " se suele denominar " torniquete ", "viraje a la derecha", "tee", "señal de afirmación" o "símbolo de afirmación". A menudo se lee, de manera sugerente, 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 cualquiera de los lados da como resultado un consecuente más débil, mientras que eliminarlas de cualquiera de los lados da como resultado uno más fuerte. Esta es una de las ventajas de simetría que se desprende del uso de semántica disyuntiva en el lado derecho del símbolo de aserción, mientras que se respeta la semántica conjuntiva en el lado izquierdo.
En el caso extremo en que la lista de fórmulas antecedentes de un consecuente está vacía, el consecuente es incondicional. Esto difiere de la afirmación incondicional simple porque el número de consecuentes es arbitrario, no necesariamente un único consecuente. Así, por ejemplo, ' ⊢ B 1 , B 2 ' significa que B 1 , o B 2 , o ambos deben ser verdaderos. Una lista de fórmulas antecedentes vacía es equivalente a la proposición "siempre verdadera", llamada " verum ", denotada "⊤". (Véase Tee (símbolo) .)
En el caso extremo en que la lista de fórmulas consecuentes de un consecuente esté vacía, la regla sigue siendo que al menos un término de la derecha sea verdadero, lo que es claramente imposible . Esto se indica mediante 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.
Aquí se observa 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 la consecuente están vacías, " no es satisfacible ". [3] En este caso, el significado del consecuente es efectivamente ' ⊤ ⊢ ⊥ '. Esto es equivalente al consecuente ' ⊢ ⊥ ', que claramente no puede ser válido.
Un consecuente de la forma ' ⊢ α, β ', para las fórmulas lógicas α y β, significa que α es verdadera o β es verdadera (o ambas). Pero 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 consecuente 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 es una tautología.
De manera similar, un consecuente de la forma ' α, β ⊢ ', para las fórmulas lógicas α y β, significa que α es falsa o β es falsa. Pero 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 consecuente válido porque B ∧ A es falso o C ∧ ¬A es falso. Pero ninguna de estas expresiones es una contradicción en forma aislada. Es la conjunción de estas dos expresiones lo que es una contradicción.
La mayoría de los sistemas de demostración proporcionan formas de deducir un consecuente de otro. Estas reglas de inferencia se escriben con una lista de consecuentes por encima y por debajo de una línea . Esta regla indica que si todo lo que está por encima de la línea es verdadero, también lo es todo lo que está por debajo de ella.
Una regla típica es:
Esto indica que si podemos deducir que se obtiene , y que se obtiene , entonces también podemos deducir que se obtiene . (Véase también el conjunto completo de reglas de inferencia del cálculo secuencial ).
El símbolo de aserción en los consecuentes 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 aserción ' ⊢ ' en un consecuente para significar demostrabilidad. Lo definió para significar exactamente lo mismo que el operador de implicación ' ⇒ '. Usando ' → ' en lugar de ' ⊢ ' y ' ⊃ ' en lugar de ' ⇒ ', escribió: "El consecuente A 1 , ..., A μ → B 1 , ..., B ν significa, en cuanto a contenido, exactamente lo mismo que la fórmula (A 1 & ... & A μ ) ⊃ (B 1 ∨ ... ∨ B ν )". [4] (Gentzen empleó el símbolo de flecha a la derecha entre los antecedentes y consecuentes de los consecuentes. Empleó el símbolo ' ⊃ ' para el operador de implicación lógica.)
En 1939, Hilbert y Bernays afirmaron también que un consecuente tiene el mismo significado que la fórmula de implicación correspondiente. [5]
En 1944, Alonzo Church enfatizó que las afirmaciones subsiguientes de Gentzen no significaban demostrabilidad.
Numerosas publicaciones posteriores han afirmado que el símbolo de aserción en los secuentes sí significa demostrabilidad dentro de la teoría en la que 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 aserción en los secuentes significa demostrabilidad. Sin embargo, Ben-Ari (2012, p. 69) afirma que el símbolo de aserción en los secuentes del sistema Gentzen, que él 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 sistemas correspondientes de deducción natural". [10] Y además: "Una prueba en un cálculo de secuentes puede verse 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 para el cálculo de secuentes, que es una especie de metacálculo, pero que simultáneamente significa deducibilidad en un sistema de deducción natural subyacente.
Un consecuente es una declaración formalizada de demostrabilidad que se utiliza con frecuencia al especificar cálculos para la deducción . En el cálculo consecuente, el nombre consecuente se utiliza 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 consecuente es que bajo el supuesto de Γ la conclusión de Σ es demostrable. Clásicamente, las fórmulas a la izquierda del torniquete se pueden interpretar de forma conjuntiva mientras que las fórmulas a la derecha se pueden considerar 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 sucedente está vacío, esto se interpreta como falsedad, es decir, significa que Γ prueba falsedad y, por lo tanto, es inconsistente. Por otro lado, se supone que un antecedente vacío es verdadero, es decir, significa que Σ sigue sin ningún supuesto, es decir, siempre es verdadero (como una disyunción). Un consecuente de esta forma, con Γ vacío, se conoce como una 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 toda fórmula en Γ sea verdadera y toda 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 demostración son puramente sintácticas , el significado de (la derivación de) un consecuente sólo viene dado por las propiedades del cálculo que proporciona las reglas reales de inferencia .
Salvo que exista alguna contradicción en la definición técnicamente precisa anterior, podemos describir los consecuentes en su forma lógica introductoria. representa un conjunto de suposiciones con las que comenzamos nuestro proceso lógico, por ejemplo, "Sócrates es un hombre" y "Todos los hombres son mortales". El representa una conclusión lógica que se sigue de estas premisas. Por ejemplo, "Sócrates es mortal" se sigue 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 español.
La noción general de consecuente introducida aquí puede especializarse de varias maneras. Se dice que un consecuente es un consecuente intuicionista si hay como máximo una fórmula en el sucedente (aunque también son posibles los cálculos de múltiples sucedentes para la lógica intuicionista). Más precisamente, la restricción del cálculo consecuente general a los consecuentes de fórmula única sucedente, con las mismas reglas de inferencia que para los consecuentes generales, constituye un cálculo consecuente intuicionista. (Este cálculo consecuente restringido se denota LJ.)
De manera similar, se pueden obtener cálculos para la lógica intuicionista dual (un tipo de lógica paraconsistente ) al requerir que los consecuentes sean singulares en el antecedente.
En muchos casos, también se supone que los consecuentes consisten en conjuntos múltiples o conjuntos en lugar de secuencias. Por lo tanto, no se tiene en cuenta el orden o incluso el número de ocurrencias de las fórmulas. Para la lógica proposicional clásica esto no plantea ningún problema, ya que las conclusiones que se pueden extraer de una colección de premisas no dependen de estos datos. Sin embargo, en la 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 tabular , que son muy convenientes para la demostración práctica de teoremas en cálculo proposicional y cálculo de predicados, fueron aplicados por Suppes (1999) y Lemmon (1965) para enseñar lógica introductoria en los libros de texto.
Históricamente, Gerhard Gentzen introdujo el término sequentz para especificar su famoso cálculo sequentz . [12] En su publicación alemana utilizó la palabra "sequenz". Sin embargo, en inglés, la palabra " sequenz " ya se utiliza como traducción de la expresión alemana "folge" y aparece con bastante frecuencia en matemáticas. El término "sequent" se creó entonces 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'".
