Notación de Suppes-Lemmon

La notación de Suppes-Lemmon ^{[ 1 ]} es un sistema de notación lógica deductiva natural desarrollado por E. J. Lemmon ^{[ 2 ]} . Derivada del método de Suppes ^{[ 3 ]} , representa las pruebas de deducción natural como secuencias de pasos justificados. Ambos métodos utilizan reglas de inferencia derivadas del sistema de deducción natural de Gentzen de 1934/1935 ^{[ 4 ]} , en el que las pruebas se presentaban en forma de diagrama de árbol en lugar de en la forma tabular de Suppes y Lemmon. Si bien la disposición en diagrama de árbol tiene ventajas para fines filosóficos y educativos, la disposición tabular es mucho más conveniente para aplicaciones prácticas.

Kleene presenta una disposición tabular similar. ^{[ 5 ]} La principal diferencia radica en que Kleene no abrevia los lados izquierdos de las afirmaciones a números de línea, prefiriendo en cambio proporcionar listas completas de proposiciones precedentes o bien indicar los lados izquierdos mediante barras que recorren la parte izquierda de la tabla para señalar las dependencias. Sin embargo, la versión de Kleene tiene la ventaja de que se presenta, aunque de forma muy esquemática, dentro de un marco riguroso de teoría metamatemática, mientras que los libros de Suppes ^{[ 3 ]} y Lemmon ^{[ 2 ]} son ​​aplicaciones de la disposición tabular para la enseñanza de la lógica introductoria.

La notación de Suppes-Lemmon es una notación para el cálculo de predicados con igualdad, por lo que su descripción se puede separar en dos partes: la sintaxis general de la prueba y las reglas específicas del contexto .

Un ejemplo de la demostración de una sucesión (un teorema en este caso):

Una prueba del principio de explosión usando la monotonicidad de la implicación . Algunos han llamado a la siguiente técnica, demostrada en las líneas 3-6, la Regla de Aumento (Finito) de Premisas: ^{[ 6 ]}

Un ejemplo de sustitución y ∨E:

El desarrollo histórico de los sistemas de deducción natural con formato tabular, que se basan en reglas y que indican las proposiciones antecedentes mediante números de línea (y métodos relacionados como barras verticales o asteriscos) incluye las siguientes publicaciones.

• 1940: En un libro de texto, Quine ^{[ 7 ]} indicó las dependencias antecedentes mediante números de línea entre corchetes, anticipándose a la notación de números de línea de Suppes de 1957.
• 1950: En un libro de texto, Quine (1982 , págs. 241-255) demostró un método que utiliza uno o más asteriscos a la izquierda de cada línea de demostración para indicar dependencias. Esto equivale a las barras verticales de Kleene. (No está del todo claro si la notación con asteriscos de Quine apareció en la edición original de 1950 o se añadió en una edición posterior). 
• 1957: Introducción a la demostración práctica de teoremas lógicos en un libro de texto de Suppes (1999 , págs. 25-150) . Esto indicaba las dependencias (es decir, las proposiciones antecedentes) mediante números de línea a la izquierda de cada línea. 
• 1963: Stoll (1979 , pp. 183–190, 215–219) utiliza conjuntos de números de línea para indicar dependencias antecedentes de las líneas de argumentos lógicos secuenciales basados ​​en reglas de inferencia de deducción natural. 
• 1965: El libro de texto completo de Lemmon (1965) es una introducción a las demostraciones lógicas utilizando un método basado en el de Suppes.
• 1967: En un libro de texto, Kleene (2002 , pp. 50–58, 128–130) demostró brevemente dos tipos de pruebas lógicas prácticas: un sistema que utiliza citas explícitas de proposiciones antecedentes a la izquierda de cada línea, y otro sistema que utiliza barras verticales a la izquierda para indicar dependencias. ^{[ 8 ]} 

• Deducción natural
• Cálculo de secuencias
• Sistemas deductivos

• Coburn, Barry; Miller, David (octubre de 1977). "Dos comentarios sobre la lógica inicial de Lemmon" . Notre Dame Journal of Formal Logic . 18 (4): 607– 610. doi : 10.1305/ndjfl/1093888128 . ISSN 0029-4527 . 
• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. Yo" . Mathematische Zeitschrift . 39 (2): 176– 210. doi : 10.1007/BF01201353 . (Traducción al inglés de Investigaciones sobre la deducción lógica en Szabo.)
• Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II" . Mathematische Zeitschrift . 39 (3): 405– 431. doi : 10.1007/bf01201363 .
• Kleene, Stephen Cole (2002) [1967]. Lógica matemática . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Lógica básica . Thomas Nelson. ISBN 0-17-712040-1.
• Pelletier, Francis Jeffry; Hazen, Allen (2024). «Sistemas de deducción natural en lógica» . En Zalta, Edward N.; Nodelman, Uri (eds.). La enciclopedia de filosofía de Stanford (  edición de primavera de 2024). Laboratorio de Investigación en Metafísica, Universidad de Stanford . Recuperado el 25 de mayo de 2025 .
• Quine, Willard Van Orman (1981) [1940]. Lógica matemática (  Edición revisada). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-55451-1.
• Quine, Willard Van Orman (1982) [1950]. Métodos de lógica (Cuarta  ed.). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-57176-1.
• Stoll, Robert Roth (1979) [1963]. Teoría de conjuntos y lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-63829-4.
• Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-40687-9.
• Szabo, ME (1969). Obras completas de Gerhard Gentzen . Ámsterdam: North-Holland.

• Pelletier, Jeff, " Historia de los libros de texto de deducción natural y lógica elemental " .