En lógica matemática , un secuente es un tipo muy general de afirmación condicional.
Un secuente puede tener cualquier número m de fórmulas de condición A i (llamadas " antecedentes ") y cualquier número n de fórmulas afirmadas B j (llamadas "sucesores" o " consecuentes "). Se entiende que un secuente 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 secuencial .
Introducción
La forma y semántica de las secuelas.
Las secuencias se entienden mejor en el contexto de los siguientes tres tipos de juicios lógicos :
- Afirmación incondicional . Sin fórmulas antecedentes.
- Ejemplo: ⊢ B
- Significado: B es verdadero.
- Afirmación condicional . Cualquier número de fórmulas antecedentes.
- Aserción condicional simple . Fórmula consecuente única.
- Ejemplo: A 1 , A 2 , A 3 ⊢ B
- Significado: SI A 1 Y A 2 Y A 3 son verdaderas, ENTONCES B es verdadera.
- Sequent . Cualquier número de fórmulas consecuentes.
- Ejemplo: A 1 , A 2 , A 3 ⊢ B 1 , B 2 , B 3 , B 4
- Significado: SI A 1 Y A 2 Y A 3 son verdaderas, ENTONCES B 1 O B 2 O B 3 O B 4 es cierto.
- Aserción condicional simple . Fórmula consecuente única.
Por tanto, las secuencias son una generalización de aserciones condicionales simples, que son una generalización de aserciones incondicionales.
La palabra "OR" aquí es la OR inclusiva . [1] La motivación de la semántica disyuntiva en el lado derecho de una secuencia proviene de tres beneficios principales.
- La simetría de las reglas de inferencia clásicas para secuencias con tal semántica.
- La facilidad y simplicidad de convertir tales reglas clásicas en reglas intuicionistas.
- La capacidad de demostrar la completitud del cálculo de predicados cuando se expresa de esta manera.
Los tres de estos beneficios fueron identificados en el artículo de fundación de Gentzen (1934 , p. 194).
No todos los autores se han adherido al significado original de Gentzen para la palabra "secuente". Por ejemplo, Lemmon (1965) usó la palabra "secuencia" estrictamente para aseveraciones condicionales simples con una y sólo una fórmula consecuente. [2] La misma definición de consecuente simple para un secuente es dada por Huth & Ryan 2004 , p. 5.
Detalles de sintaxis
En una secuencia general de la forma
tanto Γ como Σ son secuencias de fórmulas lógicas, no conjuntos . Por 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 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 las secuencias izquierda y derecha), y también para insertar fórmulas arbitrarias y eliminar copias duplicadas dentro de la izquierda. y las secuencias correctas. (Sin embargo, Smullyan (1995 , págs. 107-108), usa conjuntos de fórmulas en secuencias en lugar de secuencias de fórmulas. En consecuencia, los tres pares de reglas estructurales llamados "adelgazamiento", "contracción" e "intercambio" no son necesarios).
El símbolo ' 'a menudo se denomina " torniquete ", "virada a la derecha", "tee", "signo de afirmación" o "símbolo de afirmación". A menudo se lee, sugestivamente, como "cede", "prueba" o "implica".
Propiedades
Efectos de insertar y eliminar proposiciones
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 siguiente (el lado derecho), agregar fórmulas a cada lado da como resultado un secuente más débil, mientras que eliminarlas de cualquier lado da uno más fuerte. Ésta es una de las ventajas de la simetría que se deriva del uso de semántica disyuntiva en el lado derecho del símbolo de aserción, mientras que la semántica conjuntiva se adhiere al lado izquierdo.
Consecuencias de listas vacías de fórmulas
En el caso extremo en el que la lista de fórmulas antecedentes de un secuente está vacía, el consecuente es incondicional. Esto difiere de la simple aserción incondicional porque el número de consecuentes es arbitrario, no necesariamente un consecuente único. Así, por ejemplo, '⊢ B 1 , B 2 ' significa que B 1 o B 2 , o ambos, deben ser verdaderos. Una lista de fórmulas antecedente vacía es equivalente a la proposición "siempre verdadera", llamada " verum ", denotada "⊤". (Ver Tee (símbolo)) .
En el caso extremo en el que la lista de fórmulas consecuentes de un secuente está vacía, la regla sigue siendo que al menos un término de la derecha sea verdadero, lo cual es claramente imposible . Esto se significa por la proposición 'siempre falsa', llamada " falsum ", denotada "⊥". Dado que 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 ve 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 es " no satisfactorio ". [3] En este caso, el significado del secuente es efectivamente '⊤ ⊢ ⊥'. Esto es equivalente al secuente 'seque ⊥', que claramente no puede ser válido.
Ejemplos de
Una secuencia 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 que β sea una tautología. Para aclarar esto, considere el ejemplo '⊢ B ∨ A, C ∨ ¬A'. Esta es una secuencia válida porque B ∨ A es verdadera o C ∨ ¬A es verdadera. Pero ninguna de estas expresiones es una tautología aislada. Es la disyunción de estas dos expresiones lo que constituye una tautología.
De manera similar, una secuencia de la forma 'α, β ⊢', para las fórmulas lógicas α y β, significa que α es falso o β es falso. Pero no significa que α sea una contradicción o que β sea una contradicción. Para aclarar esto, considere el ejemplo 'B ∧ A, C ∧ ¬A ⊢'. Este es un secuente válido porque B ∧ A es falso o C ∧ ¬A es falso. Pero ninguna de estas expresiones es una contradicción aislada. Es la conjunción de estas dos expresiones lo que es una contradicción.
Reglas
La mayoría de los sistemas de prueba proporcionan formas de deducir un secuente de otro. Estas reglas de inferencia están escritas con una lista de secuencias por encima y por debajo de una línea . Esta regla indica que si todo lo que está arriba de la línea es verdadero, también lo es todo lo que está debajo de la línea.
Una regla típica es:
Esto indica que si podemos deducir que rendimientos , y eso rendimientos , entonces también podemos deducir que rendimientos . (Consulte también el conjunto completo de reglas de inferencia de cálculo secuencial ).
Interpretación
Historia del significado de las afirmaciones posteriores
El símbolo de aserción en las secuencias 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 afirmación '⊢' en una secuencia 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 secuente A 1 , ..., A μ → B 1 , ..., B ν significa, en cuanto al contenido, exactamente igual que la fórmula (A 1 & ... & A μ ) ⊃ (B 1 ∨ ... ∨ B ν ) ". [4] (Gentzen empleó el símbolo de la flecha derecha entre los antecedentes y los consecuentes de los secuentes. Empleó el símbolo '⊃' para el operador de implicación lógica).
En 1939, Hilbert y Bernays afirmaron igualmente que un secuente tiene el mismo significado que la correspondiente fórmula de implicación. [5]
En 1944, Alonzo Church enfatizó que las afirmaciones posteriores de Gentzen no significaban demostrabilidad.
- "El empleo del teorema de deducción como regla primitiva o derivada no debe, sin embargo, confundirse con el uso de Sequenzen por Gentzen. Porque la flecha de Gentzen, →, no es comparable a nuestra notación sintáctica, ⊢, pero 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 posteriores a este tiempo han afirmado que el símbolo de afirmación en las secuencias significa demostrabilidad dentro de la teoría donde se formulan las secuencias. Curry en 1963, [7] Lemmon en 1965, [2] y Huth y Ryan en 2004 [8] todos afirman que el símbolo de afirmación posterior significa demostrabilidad. Sin embargo, Ben-Ari (2012 , p. 69) afirma que el símbolo de aserción en las secuencias del sistema Gentzen, que él denota como '⇒', es parte del lenguaje del 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 correspondientes sistemas de deducción natural". [10] Y además: "Una demostración en un cálculo de secuencias se puede considerar 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 objeto para el cálculo secuencial, que es una especie de metacálculo, pero simultáneamente significa deducibilidad en un sistema de deducción natural subyacente.
Significado intuitivo
Un secuente es una declaración formalizada de probabilidad que se usa con frecuencia al especificar cálculos para la deducción . En el cálculo secuencial, se utiliza el nombre secuenciante 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 secuente es que bajo el supuesto de Γ la conclusión de Σ es demostrable. Clásicamente, las fórmulas de la izquierda del torniquete se pueden interpretar de forma conjunta, mientras que las fórmulas de la derecha se pueden considerar como una disyunción . Esto significa que, cuando todas las fórmulas en Γ se cumplen, entonces al menos una fórmula en Σ también tiene que ser verdadera. Si el sucesor está vacío, esto se interpreta como falsedad, es decirsignifica que Γ prueba falsedad y, por 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 cierto (como una disyunción). Una secuencia de esta forma, con Γ vacío, se conoce como afirmación lógica .
Por supuesto, son posibles otras explicaciones intuitivas, que son clásicamente equivalentes. Por ejemplo,se puede leer como una afirmación de que no puede ser el caso de que todas las fórmulas en Γ sean verdaderas y todas las fórmulas en Σ sean falsas (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 solo pedagógicas. Dado que las demostraciones formales en la teoría de la prueba son puramente sintácticas , el significado de (la derivación de) un secuente solo está dado por las propiedades del cálculo que proporciona las reglas reales de inferencia .
Salvo cualquier contradicción en la definición técnicamente precisa anterior, podemos describir las secuelas 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". Larepresenta una conclusión lógica que se sigue bajo estas premisas. Por ejemplo, "Sócrates es mortal" se deriva de una formalización razonable de los puntos anteriores y podríamos esperar verlo en ellado del torniquete . En este sentido, significa el proceso de razonamiento, o "por lo tanto" en inglés.
Variaciones
La noción general de secuencia que se introduce aquí puede especializarse de diversas formas. Se dice que un secuente es un secuente intuicionista si hay como máximo una fórmula en el sucesivo (aunque también son posibles los cálculos de sucesivos múltiples para la lógica intuicionista). Más precisamente, la restricción del cálculo secuencial general a secuencias secuenciales de una sola fórmula sucesiva, con las mismas reglas de inferencia que para las secuencias generales, constituye un cálculo secuencial intuicionista. (Este cálculo secuencial restringido se denomina LJ).
De manera similar, se pueden obtener cálculos para la lógica intuicionista dual (un tipo de lógica paraconsistente ) al requerir que las secuencias sean singulares en el antecedente.
En muchos casos, también se supone que los secuentes consisten en conjuntos múltiples o conjuntos en lugar de secuencias. Por lo tanto, uno ignora el orden o incluso el número de ocurrencias de las fórmulas. Para la lógica proposicional clásica , esto no presenta ningún problema, ya que las conclusiones que se pueden extraer de una colección de premisas no dependen de estos datos. En lógica subestructural , sin embargo, esto puede llegar a ser bastante importante.
Los sistemas de deducción natural usan aserciones condicionales de consecuencia única, pero normalmente no usan los mismos conjuntos de reglas de inferencia que Gentzen introdujo en 1934. En particular, los sistemas tabulares de deducción natural , que son muy convenientes para la demostración práctica de teoremas en cálculo proposicional y predicado. cálculo, fueron aplicados por Suppes (1957)
y Lemmon (1965) por enseñar lógica introductoria en libros de texto.Etimología
Históricamente, Gerhard Gentzen ha introducido las secuencias para especificar su famoso cálculo de secuencias . [12] En su publicación alemana utilizó la palabra "Sequenz". Sin embargo, en inglés, la palabra " secuencia " ya se utiliza como traducción del alemán "Folge" y aparece con bastante frecuencia en matemáticas. El término "secuente" se ha creado 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 'secuencia', porque ya hemos usado 'secuencia' para cualquier sucesión de objetos, donde el alemán es 'Folge' . "
Ver también
- Gerhard Gentzen
- Lógica intuicionista
- Deducción natural
- Cálculo secuencial
Notas
- ↑ La semántica disyuntiva para el lado derecho de una secuencia se establece y explica en Curry 1977 , pp. 189-190, Kleene 2002 , pp. 290, 297, Kleene 2009 , p. 441, Hilbert y Bernays 1970 , pág. 385, Smullyan 1995 , págs. 104-105, Takeuti 2013 , pág. 9 y Gentzen 1934 , pág. 180.
- ↑ a b Lemmon , 1965 , p. 12, escribió: "Por lo tanto, un secuente es un marco de argumento que contiene un conjunto de supuestos y una conclusión que se afirma que se sigue de ellos. [...] Las proposiciones a la izquierda de '⊢' se convierten en supuestos del argumento, y la proposición de la derecha se convierte en una conclusión válidamente extraída de esos supuestos ".
- ^ Smullyan 1995 , p. 105.
- ^ Gentzen 1934 , p. 180.
- 2.4. Die Sequenz A 1 , ..., A μ → B 1 , ..., B ν bedeutet inhaltlich genau dasselbe wie die Formel
- (A 1 & ... & A μ ) ⊃ (B 1 ∨ ... ∨ B ν ).
- 2.4. Die Sequenz A 1 , ..., A μ → B 1 , ..., B ν bedeutet inhaltlich genau dasselbe wie die Formel
- ^ Hilbert y Bernays 1970 , p. 385.
- Für die inhaltliche Deutung ist eine Sequenz
- A 1 , ..., A r → B 1 , ..., B s ,
- worin die Anzahlen r und s von 0 verschieden sind, gleichbedeutend mit der Implikation
- (A 1 & ... & A r ) → (B 1 ∨ ... ∨ B s )
- Für die inhaltliche Deutung ist eine Sequenz
- ^ Iglesia 1996 , p. 165.
- ^ Curry 1977 , p. 184
- ^ Huth y Ryan (2004 , p. 5)
- ↑ Ben-Ari , 2012 , p. 69, define secuentes a tienen la forma U ⇒ V para los conjuntos (posiblemente no vacíos) de fórmulas U y V . Luego escribe:
- "Intuitivamente, un secuente representa 'demostrable a partir de' en el sentido de que las fórmulas en U son suposiciones para el conjunto de fórmulas V que deben probarse. El símbolo ⇒ es similar al símbolo ⊢ en los sistemas de Hilbert, excepto que ⇒ es parte del lenguaje objeto del sistema deductivo que se está formalizando, mientras que ⊢ es una notación de metalenguaje utilizada para razonar sobre sistemas deductivos ".
- ^ Prawitz , 2006 , p. 90.
- ^ Véase Prawitz , 2006 , p. 91, para este y otros detalles de interpretación.
- ^ Gentzen 1934 , Gentzen 1935 .
- ^ Kleene 2002 , p. 441
Referencias
- Ben-Ari, Mordejai (2012) [1993]. Lógica matemática para informática . Londres: Springer. ISBN 978-1-4471-4128-0.
- Church, Alonzo (1996) [1944]. Introducción a la lógica matemática . Princeton, Nueva Jersey: Princeton University Press. ISBN 978-0-691-02906-1.
- Curry, Haskell Brooks (1977) [1963]. Fundamentos de la lógica matemática . 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 (1970) [1939]. Grundlagen der Mathematik II (Segunda ed.). Berlín, Nueva York: Springer-Verlag. ISBN 978-3-642-86897-9.
- Huth, Michael; Ryan, Mark (2004). Lógica en Ciencias de la Computación (Segunda ed.). Cambridge, Reino Unido: Cambridge University Press. ISBN 978-0-521-54310-1.
- Kleene, Stephen Cole (2009) [1952]. Introducción a la metamatemática . Ishi Press International. ISBN 978-0-923891-57-2.
- Kleene, Stephen Cole (2002) [1967]. Lógica matemática . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-42533-7.
- Lemmon, Edward John (1965). Lógica inicial . Thomas Nelson. ISBN 0-17-712040-1.
- Prawitz, Dag (2006) [1965]. Deducción natural: un estudio teórico-demostrativo . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-44655-4.
- Smullyan, Raymond Merrill (1995) [1968]. Lógica de primer orden . Nueva York: Publicaciones de Dover. ISBN 978-0-486-68370-6.
- Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-40687-9.
- Takeuti, Gaisi (2013) [1975]. Teoría de la prueba (Segunda ed.). Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-49073-1.
enlaces externos
- "Sequent (en lógica)" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]