En lógica matemática, un consecuente es un tipo muy general de afirmación condicional.
Un consecuente puede tener cualquier número m de las fórmulas de condición Ai (llamadas "antecedentes") y cualquier número n de fórmulas Bj declaradas (llamadas "sucedentes" o "secuentes"). 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 aserción condicional está casi siempre asociado con el marco conceptual del cálculo de consecuentes.
Introducción Los consecuentes se comprenden mejor en el contexto de los siguientes tres tipos de juicios lógicos: <li>Afirmación incondicional. No hay fórmulas antecedentes. Ejemplo: ⊢ B Significado: B es verdadero. Cualquier número de fórmulas anteriores. <li>Aserción condicional. Simple aseveración condicional. Fórmula única consecuente. Ejemplo: A1, A2, A3 ⊢ B Significado: SI A1 Y A2 Y A3 son verdaderos, entonces B es verdadero. <li>Consecuente. Cualquier número de fórmulas consecuentes. Ejemplo: A1, A2, A3 ⊢ B1, B2, B3, B4 Significado: SI A1 Y A2 Y A3 son verdaderos, ENTONCES B1 O B2 OR B3 OR B4 es verdadero. Así, los consecuentes son una generalización de afirmaciones condicionales simples, que son una generalización de aserciones incondicionales.
La palabra "O" aquí es el OR inclusivo.La semántica disyuntiva para el lado derecho de un consecuente es declarada y explicada por ,,,,,, and . La motivación para la semántica disjuntiva en el lado derecho de un consecuente trae consigo tres ventajas principales. La simetría de las reglas de inferencia clásicas para secuencias con semántica semejante. La facilidad y sencillez de convertir tales reglas clásicas a reglas intuicionistas. La capacidad de demostrar la integridad del cálculo predicado cuando se expresa de esta manera. Estos tres beneficios fueron identificados en el documento de fundación de .
No todos los autores se adhirieron al significado original de Gentzen para la palabra "consecuente". Por ejemplo, usó la palabra "consecuente" estrictamente para afirmaciones condicionales simples con una y sólo una fórmula consecuente., escribió: "Así, un consecuente es un argumento marco que contiene un conjunto de suposiciones y una conclusión que se afirma que deriva de ellos. [...] Las proposiciones a la izquierda de '⊢' se convierten en suposiciones del argumento, y la proposición A la derecha se convierte en una conclusión válidamente extraída de esos supuestos". La misma definición consecutiva para un secuente es dada por .
Detalles de la sintaxis El consecuente tiene la forma:
donde tanto Γ como Σ son secuencias de fórmulas lógicas, no conjuntos. Por lo tanto son significativos tanto el número como el orden de apariciones de las fórmulas. En particular, la misma fórmula puede 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 aserción (y por lo tanto permutar arbitrariamente los consecuentes de la izquierda y de la derecha), y también para insertar fórmulas arbitrarias y eliminar copias duplicadas dentro de la izquierda y los consecuentes correctos. (Sin embargo, Smullyan (1995, pp. 107-108), utiliza conjuntos de fórmulas en secuencias en lugar de secuencias de fórmulas. En consecuencia, no se requieren los tres pares de reglas estructurales llamadas "adelgazamiento", "contracción" e "intercambio".)
El símbolo ' ' se refiere a veces como "torniquete", "tachuela derecha", "tee", "signo de aserción" o "símbolo de aserción". Por lo general se lee, sugestivamente, como "produce", "demuestra" o "implica".
Propiedades
Efectos de insertar y eliminar proposiciones Puesto que cada fórmula en el antecedente (el lado izquierdo) debe ser verdadera para concluir la verdad de por lo menos una fórmula en el sucediente (el lado derecho), agregando las fórmulas a cada lado da lugar a un consecuente más débil, mientras que quitando de ambos lados da 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 la aserción, mientras que la semántica conjuntiva se inserta en el lado izquierdo.
Consecuencias de listas vacías de fórmulas En el caso extremo donde la lista de fórmulas antecedentes de un consecuente 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 solo consecuente. Por ejemplo, ' ⊢ B1, B2 significa que B1, o B2, o ambos, deben ser verdaderos. Una lista de fórmulas antecedentes vacías es equivalente a la proposición "siempre verdadera", llamada "tautologia", denominada "⊤". (Véase T (símbolo).)
En el caso extremo donde la lista de fórmulas consecuentes de un consecuente esté vacía, la regla es que al menos un término a la derecha es verdadero, lo cual es claramente imposible. Esto es significado por la proposición "siempre falsa", llamada "contradiccion, o absurdo", que se denomina "⊥". Como consecuencia es falsa, al menos uno de los antecedentes debe ser falso. Por ejemplo, ' A1, A2 ⊢ ' significa que al menos uno de los antecedentes A1 A2 debe ser falso.
Se ve aquí de nuevo una simetría a causa de 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 las listas de fórmulas antecedentes y consecuentes estén vacías, es "no satifactorio, ni fiable ".. En este caso, el significado del consecuente es efectivamente '⊤ ⊢ ⊥'. Esto es equivalente al siguiente '⊢ ⊥', que claramente no puede ser válido.
Ejemplos Una secuencia de la forma 'α, β', para las fórmulas lógicas α y β, significa que α es verdadera o β es verdadera. Pero no significa que α o β sean tautologías. Para aclarar esto, considerar el ejemplo ' ⊢ B ∨ A, C ∨ ¬A'. Esta es una secuencia válida ya sea porque B ∨ A es verdadero o C ∨ ¬A es verdadero. Pero ninguna de estas expresiones es una tautología aislada. Es la disyunción de estas dos expresiones la que es una tautología.
Del mismo modo, un consecuente con la forma 'α, β ⊢', para las fórmulas lógicas α y β, significa que α es falso o β es falso. Pero esto no significa que α es una contradicción o β es 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 aislada. La conjunción de estas dos expresiones es una contradicción.
Reglas La mayoría de los sistemas de demostración proporcionan maneras de deducir una consecuente de otro. Estas reglas de inferencia se escriben con una lista de secuencias 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á bajo la línea.
Una regla típica es:
Esto indica que, si es posible deducir que lleva a y que lleva a , entonces también es posible deducir que lleva a . (Véase también el conjunto completo de reglas de inferencia de cálculo secuencial.)
Interpretación Historia del significado de las afirmaciones sucesivas El símbolo de aserción en 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 más que la verdad semántica en todos los modelos.
En 1934, Gentzen no definió el símbolo de aserción '⊢' en un consecuente para significar probabilidad. Él lo definió para significar exactamente igual que el operador de la implicación "⇒". Usando '→' en lugar de '⊢' y '⊃' en lugar de '⇒', escribió: "El consecuente A1, ..., Aμ → B1, ..., Bν significa, en cuanto al contenido, exactamente igual que la fórmula (A1 & ... & Aμ) ⊃ (B1 ∨ ... ∨ Bν)".. 2.4. La secuencia A1, ..., Aμ → B1, ..., Bν significa contenido exactamente igual que la fórmula (A1 & ... & Aμ) ⊃ (B1 ∨ ... ∨ Bν). (Gentzen empleó el símbolo de la flecha derecha entre los antecedentes y los consecuentes de los sucesivos, empleando el símbolo ' ⊃ ' para el operador de la implicación lógica).
Asimismo, en 1939, Hilbert y Bernays declararon que un consecuente tiene el mismo significado que la correspondiente fórmula de implicación.. Para la interpretación sustantiva es una secuencia A1, ..., Ar → B1, ..., Bs, en el que el número r y s son distintos de 0, lo que equivale a la implicación (A1 & ... & Ar) → (B1 ∨ ... ∨ Bs)
"Sin embargo, el uso del teorema de la deducción como regla primitiva o derivada no debe confundirse con el uso de Sequenzen de Gentzen. Para la flecha de Gentzen, →, no es comparable a nuestra notación sintáctica, ⊢, sino que pertenece a su lenguaje objeto (como se desprende del hecho de que las expresiones que lo contienen aparecen como premisas y conclusiones en las aplicaciones de sus reglas de inferencia).".
Numerosas publicaciones después de este tiempo han declarado que el símbolo de aserción en secuentes sí significa probabilidad dentro de la teoría donde se formulan los consecuentes. Curry en 1963, Lemmon en 1965, and Huth and Ryan en 2004 todos los estados que el símbolo de aserción consecuente significa probabilidad. Sin embargo, afirmó que el símbolo de aserción en las consecuencias del sistema de Gentzen, que denotó como ' ⇒ ', es parte del lenguaje de objetos, no del metalenguaje., Define consecuentes que tienen la forma U ⇒ V para conjuntos (posiblemente no vacíos) de fórmulas U y V. Luego se escribe." Intuitivamente, un consecuente representa una 'forma probable' en el sentido de que las fórmulas en U son suposiciones para el conjunto de fórmulas V que han de probarse. El símbolo ⇒ es similar al símbolo ⊢ en sistemas de Hilbert, excepto que ⇒ es parte del lenguaje de objeto del sistema deductivo que se está formalizando, mientras que ⊢ es una notación de metalenguaje usada para razonar sobre sistemas deductivos."</ref>
Según Prawitz (1965): "Los cálculos de consecuentes pueden ser entendidos como meta-cálculos para la relación de deducibilidad en los sistemas correspondientes de deducción natural.". Y además: "Una prueba en un cálculo de consecuentes puede ser vista como una instrucción sobre cómo construir una deducción natural correspondiente."Véase , para esto y más detalles de la interpretación. En otras palabras, el símbolo de aserción es parte del lenguaje de objetos para el cálculo secuencial, que es una especie de meta-cálculo, pero simultáneamente significa deducibilidad en un sistema de deducción natural subyacente.
Significado intuitivo
El significado intuitivo de un subsiguiente es tal que, bajo el supuesto de Γ, es demostrabe la conclusión de Σ. Clásicamente, las fórmulas a la izquierda del trinquete pueden ser interpretadas como una conjunción, mientras que las fórmulas de la derecha pueden considerse como una disyunción. Esto significa que si todas las fórmulas en el conjunto Γ fueran verdaderas, entonces por lo menos una fórmula Σ también tiene que ser verdadera. Si el sucedente está vacío, se interpreta esta situación como una falsedad, es decir, significa que Γ/implica falsedad y por lo tanto es inconsistente. Por otro lado, asumimos un vacío como verdadero, es decir, significa que Σ procede sin ningún supuesto, o sea, la disyunción es siempre verdadera. Una afirmación lógica se ve como un secuente en el formato .
Son posibles otras explicaciones intuitivas equivalentes. Por ejemplo, puede leerse como una afirmación de que no es probable que se produzca un caso en el que todas las fórmulas de Γ sean verdaderas y todas las fórmulas de Σ sean falsas (esto está relacionado con la regla de inferencia de la doble negación).