Ver el código de «Consecuente»

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

: <math>A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n.</math>

Un consecuente puede tener cualquier número ''m'' de las [[Fórmula bien formada|fórmulas]] de condición ''Ai'' (llamadas "[[antecedente (lógica)|antecedentes]]") y cualquier número ''n'' de fórmulas ''B<sub>j</sub>'' declaradas (llamadas "sucedentes" o "secuentes"). Se entiende que un [[Apódosis|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 secuentes|cálculo de consecuentes]].

== Introducción ==
Los consecuentes se comprenden mejor en el contexto de los siguientes tres tipos de [[Juicio (pensamiento)|juicios lógicos]]:
<ol>
<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.''
<ol type="a"> Simple aseveración condicional. Fórmula única consecuente.
* Ejemplo: ''A<sub>1</sub>'', ''A<sub>2</sub>'', ''A<sub>3</sub>'' ⊢ ''B''
Significado: SI ''A<sub>1</sub>'' Y ''A<sub>2</sub>'' Y ''A<sub>3</sub>'' son verdaderos, entonces ''B'' es verdadero.
<li>'''Consecuente'''. Cualquier número de fórmulas consecuentes.
* Ejemplo: ''A<sub>1</sub>'', ''A<sub>2</sub>'', ''A<sub>3</sub>'' ⊢ ''B<sub>1</sub>'', ''B<sub>2</sub>'', ''B<sub>3</sub>'', ''B<sub>4</sub>''
* Significado: SI ''A<sub>1</sub>'' Y ''A<sub>2</sub>'' Y ''A<sub>3</sub>''  son verdaderos, ENTONCES ''B<sub>1</sub>'' O ''B<sub>2</sub>'' OR ''B<sub>3</sub>'' OR ''B<sub>4</sub>'' es verdadero.
</ol>
</ol>
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 [[Disyunción lógica|OR inclusivo]].<ref>La semántica disyuntiva para el lado derecho de un consecuente es declarada y explicada por {{harvnb|Curry|1977|pp=189–190}}, {{harvnb|Kleene|2002|pp=290, 297}}, {{harvnb|Kleene|2009|p=441}}, {{harvnb|Hilbert|Bernays|1970|p=385}}, {{harvnb|Smullyan|1995|pp=104–105}}, {{harvnb|Takeuti|2013|p=9}}, and {{harvnb|Gentzen|1934|p=180}}.</ref> 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 {{harvtxt|Gentzen|1934|p=194}}.

No todos los autores se adhirieron al significado original de Gentzen para la palabra "consecuente". Por ejemplo, {{harvtxt|Lemmon|1965}} usó la palabra "consecuente" estrictamente para afirmaciones condicionales simples con una y sólo una fórmula consecuente.<ref name=Lemmon1965p12>{{harvnb|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".</ref> La misma definición consecutiva para un secuente es dada por {{harvnb|Huth|Ryan|2004|p=5}}.

=== Detalles de la sintaxis ===
El consecuente tiene la forma:
:<math>\Gamma\vdash\Sigma</math>
donde tanto Γ como Σ son secuencias de fórmulas lógicas, no [[conjunto]]s. 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 [[Cálculo de secuentes|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 [[permutación|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 ' <math>\vdash</math> ' se refiere a veces como  "[[Trinquete (símbolo)|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 ===
{{referencias|t=20161214211058|filosofía}}
==== 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<sub>1</sub>'', ''B<sub>2</sub>'' significa que ''B<sub>1</sub>'', o  ''B<sub>2</sub>'', o ambos, deben ser verdaderos. Una lista de fórmulas antecedentes vacías es equivalente a la proposición "siempre verdadera", llamada "[[Tautología|verum]]", 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 "[[Falso (lógica)|falsum]]", que se denomina "⊥". Como consecuencia es falsa, al menos uno de los antecedentes debe ser falso. Por ejemplo, ' ''A<sub>1</sub>'', ''A<sub>2</sub>'' ⊢ ' significa que al menos uno de los antecedentes ''A<sub>1</sub>''  ''A<sub>2</sub>'' 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 "[[Interpretación (lógica)|no satisfiable]]".<ref>{{harvnb|Smullyan|1995|p=105}}.</ref> 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 [[Coplanaridad|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:
:<math> \frac{\Gamma,\alpha\vdash\Sigma\qquad \Gamma\vdash\Sigma,\alpha}{\Gamma\vdash\Sigma}</math>

Esto indica que, si es posible deducir que <math>\Gamma,\alpha</math> lleva a <math>\Sigma</math> y que <math>\Gamma</math> lleva a <math>\Sigma,\alpha</math>, entonces también es posible deducir que <math>\Gamma</math> lleva a <math>\Sigma</math>. (Véase también el conjunto completo de [[cálculo secuencial#Reglas de inferencia|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<sub>1</sub>, ..., A<sub>μ</sub> → B<sub>1</sub>, ..., B<sub>ν</sub> significa, en cuanto al contenido, exactamente igual que la fórmula (A<sub>1</sub> &amp; ... &amp; A<sub>μ</sub>) ⊃ (B<sub>1</sub> ∨ ... ∨ B<sub>ν</sub>)".<ref>{{harvnb|Gentzen|1934|p=180}}.
: 2.4. La Secuuencia A<sub>1</sub>, ..., A<sub>μ</sub> → B<sub>1</sub>, ..., B<sub>ν</sub> significa contenido exactamente igual que la fórmula
::: (A<sub>1</sub> &amp; ... &amp; A<sub>μ</sub>) ⊃ (B<sub>1</sub> ∨ ... ∨ B<sub>ν</sub>).</ref> (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, [[David Hilbert|Hilbert]] y [[Paul Bernays|Bernays]] declararon que un consecuente tiene el mismo significado que la correspondiente fórmula de implicación.<ref>{{harvnb|Hilbert|Bernays|1970|p=385}}.
: Para la interpretación sustantiva es una secuencia
::: A<sub>1</sub>, ..., A<sub>r</sub> → B<sub>1</sub>, ..., B<sub>s</sub>,
: en el que el número r y s son distintos de 0, lo que equivale a la implicación
::: (A<sub>1</sub> &amp; ... &amp; A<sub>r</sub>) → (B<sub>1</sub> ∨ ... ∨ B<sub>s</sub>)
</ref>

: "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)."<ref>{{harvnb|Church|1996|p=165}}.</ref>

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. [[Haskell Curry|Curry]] en 1963,<ref>{{harvnb|Curry|1977|p=184}}</ref> [[John Lemmon|Lemmon]] en 1965,<ref name=Lemmon1965p12 /> and Huth and Ryan en 2004<ref>{{harvtxt|Huth|Ryan|2004|p=5}}</ref> todos los estados que el símbolo de aserción consecuente significa probabilidad. Sin embargo, {{harvtxt|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.<ref>{{harvnb|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."</ref>
: 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."<ref>{{harvnb|Prawitz|2006|p=90}}.</ref> 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."<ref>Véase {{harvnb|Prawitz|2006|p=91}}, para esto y más detalles de la interpretación.</ref> 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 ===
{{referencias|t=20161214210951|filosofía}}
El significado intuitivo de un subsiguiente <math>\Gamma\vdash\Sigma</math> 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 lógica|conjunción]], mientras que las fórmulas de la derecha pueden considerse como una [[Disyunción lógica|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, <math>\Gamma\vdash</math> significa que Γ/implica falsedad y por lo tanto es [[inconsistencia|inconsistente]]. Por otro lado, asumimos un vacío como verdadero, es decir, <math>\vdash\Sigma</math> 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 <math>\vdash\Sigma</math>.

Son posibles otras explicaciones intuitivas equivalentes. Por ejemplo, <math>\Gamma\vdash\Sigma</math> 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 [[Sintaxis|sintáctica]], la [[semántica]] de (o derivación de) un subsiguiente se da solo por las propiedades del cálculo que determina las [[regla de inferencia|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 <math>\Gamma</math> 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 <math>\Sigma</math> 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, <math>\Sigma</math>, del ''trinquete''. Por lo tanto, el símbolo <math>\vdash</math> puede ser interpretado como el proceso de razonamiento, o "por lo tanto" en español.

== Variaciones ==
{{referencias|t=20161214210920|filosofía}}
La noción general de un consecuente, introducida en este artículo, puede ser especializada en diversas formas. Un consecuente se llama ''intuicionístico'' 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 [[multiconjunto]]s o [[conjunto]]s en lugar de [[Secuencia (matemáticas)|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 tabular]]es, que son muy convenientes para probar teoremas prácticos en cálculo proposicional y de predicado, fueron aplicados por {{harvtxt|Suppes|1957}} y {{harvtxt|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]].<ref>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> 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<ref>{{harvnb|Kleene|2002|p=441}}</ref> 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 ==
{{listaref}}
== Bibliografía ==
* {{cita libro|ref=harv|apellido1=Ben-Ari|nombre1=Mordechai|enlace-autor1=Mordechai Ben-Ari|título=Mathematical logic for computer science|editorial=Springer|ubicación=Londres|año=2012|fecha=1993|isbn=978-1-4471-4128-0}}
* {{cita libro|ref=harv|apellido1=Church|nombre1=Alonzo|enlace-autor1=Alonzo Church|título=Introduction to mathematical logic|editorial=[[Princeton University Press]]|ubicación=Princeton, Nueva Jersey|fecha=1944|año=1996|isbn=978-0-691-02906-1}}
* {{cita libro|ref=harv|apellido1=Curry|nombre1=Haskell Brooks|enlace-autor1=Haskell Curry|título=Foundations of mathematical logic|fecha=1963|año=1977|editorial=Dover Publications Inc.|ubicación=Nueva York|isbn=978-0-486-63462-3}}
* {{cita publicación|ref=harv|apellido1=Gentzen|nombre1=Gerhard|enlace-autor1=Gerhard Gentzen|título=Untersuchungen über das logische Schließen. I|publicación=Mathematische Zeitschrift|volumen=39 (2)|año=1934|editorial=|páginas=176–210|doi=10.1007/bf01201353|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508}}
* {{cita publicación|ref=harv|apellido1=Gentzen|nombre1=Gerhard|enlace-autor1=Gerhard Gentzen|título=Untersuchungen über das logische Schließen. II|publicación=Mathematische Zeitschrift|volumen=39 (3)|año=1935|editorial=|páginas=405–431|doi=10.1007/bf01201363|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375605}}
* {{cita libro|ref=harv|apellido1=Hilbert|nombre1=David| enlace-autor1=David Hilbert | apellido2=Bernays | nombre2=Paul |author2-link=Paul Bernays|título=Grundlagen der Mathematik II|fecha=1939|año=1970|editorial=Springer-Verlag|ubicación=Berlin, Nueva York|isbn=978-3-642-86897-9|edición=Segunda}}
* {{cita libro|ref=harv|apellido1=Huth|nombre1=Michael|apellido2=Ryan|nombre2=Mark|título=Logic in Computer Science| año=2004|editorial=[[Cambridge University Press]]|ubicación=Cambridge, United Kingdom|edición=Segunda|isbn=978-0-521-54310-1}}
* {{cita libro|ref=harv|apellido1=Kleene|nombre1=Stephen Cole|enlace-autor1=Stephen Cole Kleene|título=Introduction to metamathematics|fecha=1952|año=2009|editorial=Ishi Press International|isbn=978-0-923891-57-2}}
* {{cita libro|ref=harv|apellido1=Kleene|nombre1=Stephen Cole|enlace-autor1=Stephen Cole Kleene|título=Mathematical logic|fecha=1967|año=2002|editorial=Dover Publications|ubicación=Mineola, Nueva York|isbn=978-0-486-42533-7}}
* {{cita libro|ref=harv|apellido1=Lemmon|nombre1=Edward John|enlace-autor1=John Lemmon|título=Beginning logic|año=1965|editorial=Thomas Nelson|isbn=0-17-712040-1}}
* {{cita libro|ref=harv|apellido1=Prawitz|nombre1=Dag|enlace-autor1=Dag Prawitz|año=2006|fecha=1965|título=Natural deduction: A proof-theoretical study|editorial=Dover Publications|ubicación=Mineola, Nueva York|isbn=978-0-486-44655-4}}
* {{cita libro|ref=harv|apellido1=Smullyan|nombre1=Raymond Merrill|enlace-autor1=Raymond Smullyan|año=1995|fecha=1968|título=First-order logic|editorial=Dover Publications|ubicación=Nueva York|isbn=978-0-486-68370-6}}
* {{cita libro|ref=harv|apellido1=Suppes|nombre1=Patrick Colonel|enlace-autor1=Patrick Suppes|año=1999|fecha=1957|título=Introduction to logic|editorial=Dover Publications|ubicación=Mineola, Nueva York|isbn=978-0-486-40687-9}}
* {{cita libro|ref=harv|apellido1=Takeuti|nombre1=Gaisi|enlace-autor1=Gaisi Takeuti|título=Proof theory|edición=Segunda|editorial=Dover Publications|ubicación=Mineola, Nueva York|año=2013|fecha=1975|isbn=978-0-486-49073-1}}

* {{springer|título=Sequent (in logic)|id=p/s084590}}

== Enlaces externos ==
{{traducido ref|en|Sequent|oldid=754125174|trad=total}}

{{Control de autoridades}}
[[Categoría:Lógica]]
[[Categoría:Teoría de la demostración]]