Consecuente

El consecuente tiene la forma:

${\displaystyle \Gamma \vdash \Sigma }$

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 ' ${\displaystyle \vdash }$ ' 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".

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.

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, ' ⊢ B₁, B₂ significa que B₁, o B₂, 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, ' A₁, A₂ ⊢ ' significa que al menos uno de los antecedentes A₁ A₂ 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 ".[3] En este caso, el significado del consecuente es efectivamente '⊤ ⊢ ⊥'. Esto es equivalente al siguiente '⊢ ⊥', que claramente no puede ser válido.

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.

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:

${\displaystyle {\frac {\Gamma ,\alpha \vdash \Sigma \qquad \Gamma \vdash \Sigma ,\alpha }{\Gamma \vdash \Sigma }}}$

Esto indica que, si es posible deducir que ${\displaystyle \Gamma ,\alpha }$ lleva a ${\displaystyle \Sigma }$ y que ${\displaystyle \Gamma }$ lleva a ${\displaystyle \Sigma ,\alpha }$, entonces también es posible deducir que ${\displaystyle \Gamma }$ lleva a ${\displaystyle \Sigma }$. (Véase también el conjunto completo de reglas de inferencia de cálculo secuencial.)

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 A₁, ..., A_μ → B₁, ..., B_ν significa, en cuanto al contenido, exactamente igual que la fórmula (A₁ & ... & A_μ) ⊃ (B₁ ∨ ... ∨ B_ν)".[4] (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.[5]

"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)."[6]

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,[7] Lemmon en 1965,[2] and Huth and Ryan en 2004[8] todos los estados que el símbolo de aserción consecuente significa probabilidad. Sin embargo,Ben-Ari (2012, p. 69) afirmó que el símbolo de aserción en los consecuencias del sistema de Gentzen, que denotó como ' ⇒ ', es parte del lenguaje de objetos, no del metalenguaje.[9]

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."[10] 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."[11] 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.

El significado intuitivo de un subsiguiente ${\displaystyle \Gamma \vdash \Sigma }$ 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, ${\displaystyle \Gamma \vdash }$ significa que Γ/implica falsedad y por lo tanto es inconsistente. Por otro lado, asumimos un vacío como verdadero, es decir, ${\displaystyle \vdash \Sigma }$ 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 ${\displaystyle \vdash \Sigma }$.

Son posibles otras explicaciones intuitivas equivalentes. Por ejemplo, ${\displaystyle \Gamma \vdash \Sigma }$ 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).

En cualquier caso, estas lecturas intuitivas son de propósito meramente pedagógico. Cómo las pruebas formales en teoría de la prueba son puramente sintáctica, la semántica de (o derivación de) un subsiguiente se da solo por las propiedades del cálculo que determina las reglas de inferencia.

Salvo cualquier contradicción en la definición técnica dada anteriormente, podemos describir consecuentes en la misma forma lógica. La expresión ${\displaystyle \Gamma }$ representa un conjunto de suposiciones con las cuales comenzamos nuestro proceso lógico. Por ejemplo: "Sócrates es humano" y "Todos los humanos son mortales". El símbolo ${\displaystyle \Sigma }$ representa una conclusión lógica es fruto del resultado de esas premisas. Por ejemplo, la conclusión "Sócrates es mortal" es fruto del resultado de una formalización razonable de los supuestos mencionados anteriormente, y por lo tanto se puede insertar en el lado derecho, ${\displaystyle \Sigma }$, del trinquete. Por lo tanto, el símbolo ${\displaystyle \vdash }$ puede ser interpretado como el proceso de razonamiento, o "por lo tanto" en español.