Consecuente

En lógica matemática, un consecuente es un tipo muy general de afirmación condicional.

${\displaystyle A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}.}$

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 B_j 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:

1. Afirmación incondicional. No hay fórmulas antecedentes.
   • Ejemplo: ⊢ B
   • Significado: B es verdadero. Cualquier número de fórmulas anteriores.
2. Aserción condicional.
   Simple aseveración condicional. Fórmula única consecuente.
   • Ejemplo: A₁, A₂, A₃ ⊢ B

   Significado: SI A₁ Y A₂ Y A₃ son verdaderos, entonces B es verdadero.

   1. Consecuente. Cualquier número de fórmulas consecuentes.
      • Ejemplo: A₁, A₂, A₃ ⊢ B₁, B₂, B₃, B₄
      • Significado: SI A₁ Y A₂ Y A₃ son verdaderos, ENTONCES B₁ O B₂ OR B₃ OR B₄ 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.^[1] La motivación para la semántica disjuntiva en el lado derecho de un consecuente trae consigo tres ventajas principales.

1. La simetría de las reglas de inferencia clásicas para secuencias con semántica semejante.
2. La facilidad y sencillez de convertir tales reglas clásicas a reglas intuicionistas.
3. 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 Gentzen (1934, p. 194).

No todos los autores se adhirieron al significado original de Gentzen para la palabra "consecuente". Por ejemplo,Lemmon (1965) usó la palabra "consecuente" estrictamente para afirmaciones condicionales simples con una y sólo una fórmula consecuente.^[2] La misma definición consecutiva para un secuente es dada por Huth y Ryan, 2004, p. 5.

Detalles de la sintaxis

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".

Propiedades

Este artículo o sección necesita referencias que aparezcan en una publicación acreditada.

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, ' ⊢ 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.

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:

${\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.)

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 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.

Significado intuitivo

Este artículo o sección necesita referencias que aparezcan en una publicación acreditada.

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.

Variaciones

Este artículo o sección necesita referencias que aparezcan en una publicación acreditada.

La noción general de un consecuente, introducida en este artículo, puede ser especializada en diversas formas. Un consecuente se llama intuitivo si existe a lo sumo una fórmula en el sucedente. Este forma es requisito para obtener métodos de cálculo para la lógica intuicionista.

Del mismo modo, se pueden obtener los métodos de cálculo para la lógica intuicionista dual, que es una tipo de lógica paraconsistente, exigiendo que los consecuentes tengan una fórmula en el antecedente.

En muchos casos, también se asume que los consecuentes consisten en multiconjuntos o conjuntos en lugar de secuencias matemáticas. Por lo tanto, es posible no tener en cuenta el orden e incluso el número de ocurrencias de las fórmulas. Para la lógica proposicional, esto no es un problema, ya que las conclusiones que se pueden extraer de la colección de premisas no dependen de estos datos. En la lógica subestrutural, sin embargo, estos datos pueden tener cierta importancia.

Los sistemas de deducción natural usan afirmaciones condicionales de una sola consecuencia, pero no son típicamente usados 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 probar teoremas prácticos en cálculo proposicional y de predicado, fueron aplicados por Suppes (1957) y Lemmon (1965) para enseñar introducción a la lógica en los libros de texto.

Etimología

Históricamente, los consecuentes fueron introducidos por Gerhard Gentzen, con el objetivo de especificar el famoso cálculo de consecuentes.^[12] La palabra usada originalmente fue la palabra alemana Sequenz. En inglés, sin embargo, la palabra Sequence es ahora considerada como una traducción de la palabra alemana Folge, y que, muchas veces, es utilizada en matemáticas. El término Sequent, por lo tanto, se creó como 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 se traduce como 'secuent' (consecuente), porque se ha usado 'secuencia' para cualquier sucesión de objetos, donde el alemán es 'Folge'."

Véase también

• Lógica intuicionista
• Gerhard Gentzen
• Deducción natural

Referencias

1. La semántica disyuntiva para el lado derecho de un consecuente es declarada y explicada por Curry, 1977, pp. 189–190,Kleene, 2002, pp. 290, 297,Kleene, 2009, p. 441,Hilbert y Bernays, 1970, p. 385,Smullyan, 1995, pp. 104–105,Takeuti, 2013, p. 9, and Gentzen, 1934, p. 180.
2. Lemmon, 1965, p. 12, 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".
3. Smullyan, 1995, p. 105.
4. Gentzen, 1934, p. 180.

   2.4. La Secuuencia A₁, ..., A_μ → B₁, ..., B_ν significa contenido exactamente igual que la fórmula

   (A₁ & ... & A_μ) ⊃ (B₁ ∨ ... ∨ B_ν).

5. Hilbert y Bernays, 1970, p. 385.

   Para la interpretación sustantiva es una secuencia

   A₁, ..., A_r → B₁, ..., B_s,

   en el que el número r y s son distintos de 0, lo que equivale a la implicación

   (A₁ & ... & A_r) → (B₁ ∨ ... ∨ B_s)

6. Church, 1996, p. 165.
7. Curry, 1977, p. 184
8. Huth y Ryan (2004, p. 5)
9. Ben-Ari, 2012, p. 69, Define consecuentes que tienen la forma U ⇒ V para conjuntos (posiblemente no vacíos) de fórmulas U y V. Luego se escribe."
10. Prawitz, 2006, p. 90.
11. Véase Prawitz, 2006, p. 91, para esto y más detalles de la interpretación.
12. Gentzen, 1934,Gentzen, 1935.
13. Kleene, 2002, p. 441

Bibliografía

• Ben-Ari, Mordechai (1993). Mathematical logic for computer science. Londres: Springer. ISBN 978-1-4471-4128-0.
• Church, Alonzo (1944). Introduction to mathematical logic. Princeton, Nueva Jersey: Princeton University Press. ISBN 978-0-691-02906-1.
• Curry, Haskell Brooks (1963). Foundations of mathematical logic. Nueva York: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Gentzen, Gerhard (1934). «Untersuchungen über das logische Schließen. I». Mathematische Zeitschrift. 39 (2): 176-210. doi:10.1007/bf01201353.
• Gentzen, Gerhard (1935). «Untersuchungen über das logische Schließen. II». Mathematische Zeitschrift. 39 (3): 405-431. doi:10.1007/bf01201363.
• Hilbert, David; Bernays, Paul (1939). Grundlagen der Mathematik II (Segunda edición). Berlin, Nueva York: Springer-Verlag. ISBN 978-3-642-86897-9.
• Huth, Michael; Ryan, Mark (2004). Logic in Computer Science (Segunda edición). Cambridge, United Kingdom: Cambridge University Press. ISBN 978-0-521-54310-1.
• Kleene, Stephen Cole (1952). Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2.
• Kleene, Stephen Cole (1967). Mathematical logic. Mineola, Nueva York: Dover Publications. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Beginning logic. Thomas Nelson. ISBN 0-17-712040-1.
• Prawitz, Dag (1965). Natural deduction: A proof-theoretical study. Mineola, Nueva York: Dover Publications. ISBN 978-0-486-44655-4.
• Smullyan, Raymond Merrill (1968). First-order logic. Nueva York: Dover Publications. ISBN 978-0-486-68370-6.
• Suppes, Patrick Colonel (1957). Introduction to logic. Mineola, Nueva York: Dover Publications. ISBN 978-0-486-40687-9.
• Takeuti, Gaisi (1975). Proof theory (Segunda edición). Mineola, Nueva York: Dover Publications. ISBN 978-0-486-49073-1.

• Hazewinkel, Michiel, ed. (2001), «Consecuente», Encyclopaedia of Mathematics (en inglés), Springer, ISBN 978-1556080104.

Enlaces externos

• Esta obra contiene una traducción total derivada de «Sequent» de Wikipedia en inglés, concretamente de esta versión, publicada por sus editores bajo la Licencia de documentación libre de GNU y la Licencia Creative Commons Atribución-CompartirIgual 4.0 Internacional.

• Datos: Q843632