Notación Suppes-Lemmon

La notación de Suppes-Lemmon ^[1] es un sistema de notación de lógica deductiva natural desarrollado por E. J. Lemmon . ^[2] Derivado 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 forma tabular de Suppes y Lemmon. Aunque el diseño de diagrama de árbol tiene ventajas para fines filosóficos y educativos, el diseño tabular es mucho más conveniente para aplicaciones prácticas.

Kleene presenta un diseño tabular similar. ^[5] La principal diferencia es que Kleene no abrevia los lados izquierdos de las afirmaciones a números de línea, prefiriendo en cambio dar listas completas de proposiciones precedentes o alternativamente indicar los lados izquierdos mediante barras que recorren el lado izquierdo de la tabla para indicar dependencias. Sin embargo, la versión de Kleene tiene la ventaja de que se presenta, aunque de manera 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 del diseño tabular para enseñar lógica introductoria.

Descripción del sistema deductivo

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

Sintaxis de prueba general

Una prueba es una tabla con 4 columnas y filas ordenadas ilimitadas. De izquierda a derecha, las columnas contienen:

1. Un conjunto de números enteros positivos, posiblemente vacíos.
2. Un entero positivo
3. Una fórmula bien formada (o fbf)
4. Un conjunto de números, posiblemente vacíos; una regla; y posiblemente una referencia a otra prueba

El siguiente es un ejemplo:

La segunda columna contiene los números de línea. La tercera contiene una función de fórmula formal, que está justificada por la regla que se cumple en la cuarta junto con información auxiliar sobre otras funciones de fórmula formal, posiblemente en otras pruebas. La primera columna representa los números de línea de los supuestos en los que se basa la función de fórmula formal, determinados por la aplicación de la regla citada en el contexto. Cualquier línea de cualquier prueba válida puede convertirse en un consecuente enumerando las funciones de fórmula formal en las líneas citadas como premisas y la función de fórmula formal en la línea como conclusión. Análogamente, pueden convertirse en condicionales donde el antecedente es una conjunción. Estos consecuentes a menudo se enumeran encima de la prueba, como lo hace Modus Tollens .

Reglas del cálculo de predicados con igualdad

La prueba anterior es válida, pero no es necesario que las pruebas se ajusten a la sintaxis general del sistema de pruebas. Sin embargo, para garantizar la validez de una secuencia, debemos ajustarnos a reglas cuidadosamente especificadas. Las reglas se pueden dividir en cuatro grupos: las reglas proposicionales (1-10), las reglas de predicado (11-14), las reglas de igualdad (15-16) y la regla de sustitución (17). Agregar estos grupos en orden permite construir un cálculo proposicional, luego un cálculo de predicado, luego un cálculo de predicado con igualdad, luego un cálculo de predicado con igualdad que permite la derivación de nuevas reglas. Algunas de las reglas del cálculo proposicional, como la TMT, son superfluas y se pueden derivar como reglas de otras reglas.

1. Regla de suposición (A): "A" justifica cualquier wff. La única suposición es su propio número de línea.
2. Modus Ponendo Ponens (MPP): Si hay líneas a y b previamente en la prueba que contienen P → Q y P respectivamente, " a , b MPP" justifica Q. Los supuestos son el conjunto colectivo de líneas a y b .
3. Regla de la prueba condicional (PC): si una línea a con la proposición P tiene como supuesto la línea b con la proposición Q, " b , a PC" justifica Q→P. Se mantienen todos los supuestos de a , excepto b .
4. Regla de la doble negación (DN): " una DN" justifica la adición o sustracción de dos símbolos de negación de la fbf en una línea a previamente en la prueba, lo que hace que esta regla sea bicondicional. El conjunto de supuestos es el de la línea citada.
5. Regla de introducción ∧ (∧I): Si las proposiciones P y Q están en las líneas a y b , " a , b ∧I" justifica P∧Q. Los supuestos son el conjunto de proposiciones conjuntas.
6. Regla de eliminación de ∧ (∧E): si la línea a es una conjunción P∧Q, se puede concluir que P o Q son iguales usando " a ∧E". Los supuestos son los de la línea a . ∧I y ∧E permiten la monotonía de la implicación , ya que cuando una proposición P se une con Q con ∧I y se separa con ∧E, conserva los supuestos de Q.
7. Regla de introducción de ∨ (∨I): Para una recta a con proposición P se puede introducir P∨Q citando " a ∨I". Los supuestos son a 's.
8. Regla de eliminación de ∨ (∨E): Para una disyunción P∨Q, si se supone P y Q y se llega por separado a la conclusión R a partir de cada una, entonces se puede concluir R. La regla se cita como " a , b , c , d , e ∨E", donde la línea a tiene la disyunción inicial P∨Q, las líneas b y d suponen P y Q respectivamente, y las líneas c y e concluyen R con P y Q en sus respectivos conjuntos de supuestos. Los supuestos son los conjuntos colectivos de las dos líneas que concluyen R, c y e , menos las líneas que suponen P y Q, b y d .
9. Reducción al absurdo (RAA): Para una proposición P∧¬P en la línea a que cita un supuesto Q en la línea b , se puede citar " b , una RAA" y derivar ¬Q de los supuestos de la línea a además de b .
10. Modus Tollens (MTT): Para las proposiciones P→Q y ¬Q en las líneas a y b se puede citar " a , b MTT" para derivar ¬P. Las suposiciones son las de las líneas a y b . Esto se demuestra a partir de otras reglas anteriores.
11. Introducción universal (IU): para un predicado en la línea a , se puede citar " una IU" para justificar una cuantificación universal, , siempre que ninguna de las suposiciones en la línea a tenga el término en ninguna parte. Las suposiciones son las de la línea a . ${\displaystyle Ra}$ ${\displaystyle (\forall x)Rx}$ ${\displaystyle a}$
12. Eliminación universal (UE): para un predicado cuantificado universalmente en la línea a , se puede citar " una UE" para justificar . Las suposiciones son las de la línea a . La UE es una dualidad con UI en el sentido de que se puede cambiar entre variables cuantificadas y libres utilizando estas reglas. ${\displaystyle (\forall x)Rx}$ ${\displaystyle Ra}$
13. Introducción existencial (IE): Para un predicado de la línea a se puede citar " una IE" para justificar una cuantificación existencial, . Los supuestos son los de la línea a . ${\displaystyle Ra}$ ${\displaystyle (\exists x)Rx}$
14. Eliminación existencial (EE): Para un predicado cuantificado existencialmente en la línea a , si asumimos que es verdadero en la línea b y derivamos P con él en la línea c , podemos citar " a , b , c EE" para justificar P. El término no puede aparecer en la conclusión P, ninguna de sus suposiciones aparte de la línea b , o en la línea a . Por esta razón EE y EI están en dualidad, ya que uno puede asumir y usar EI para llegar a una conclusión de , ya que EI eliminará la conclusión del término . Las suposiciones son las suposiciones en la línea a y cualquier suposición en la línea c aparte de b . ${\displaystyle (\exists x)Rx}$ ${\displaystyle Ra}$ ${\displaystyle a}$ ${\displaystyle Ra}$ ${\displaystyle (\exists x)Rx}$ ${\displaystyle a}$
15. Introducción de igualdad (=I): En cualquier punto se puede introducir la cita "=I" sin hacer suposiciones. ${\displaystyle a=a}$
16. Eliminación de igualdad (=E): Para las proposiciones y P en las líneas a y b , se puede citar " a , b =E" para justificar el cambio de cualquier término en P a . Los supuestos son el conjunto de líneas a y b . ${\displaystyle a=b}$ ${\displaystyle a}$ ${\displaystyle b}$
17. Instancia de sustitución (SI(S)): Para una secuencia demostrada en la prueba X e instancias de sustitución de y en las líneas a y b , se puede citar " a , b SI(S) X" para justificar la introducción de una instancia de sustitución de . Las suposiciones son las de las líneas a y b . Una regla derivada sin suposiciones es un teorema, y ​​se puede introducir en cualquier momento sin suposiciones. Algunos lo citan como "TI(S)", por "teorema" en lugar de "secuencia". Además, algunos citan solo "SI" o "TI" en cualquier caso cuando no se necesita una instancia de sustitución, ya que sus proposiciones coinciden exactamente con las de la prueba a la que se hace referencia. ${\displaystyle P,Q\vdash R}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle R}$

Ejemplos

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

Una prueba del principio de explosión utilizando la monotonía de 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:

Historia de los sistemas de deducción natural tabular

El desarrollo histórico de los sistemas de deducción natural basados ​​en tablas, que se basan en reglas y que indican 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, pp. 241–255) demostró un método para utilizar uno o más asteriscos a la izquierda de cada línea de prueba para indicar dependencias. Esto es equivalente a las barras verticales de Kleene. (No está totalmente claro si la notación de asterisco de Quine apareció en la edición original de 1950 o se agregó en una edición posterior).
• 1957: Introducción a la demostración de teoremas de lógica práctica en un libro de texto de Suppes (1999, pp. 25-150). En él se indicaban 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: Todo el libro de texto de Lemmon (1965) es una introducción a las pruebas 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 el otro sistema que utiliza barras verticales a la izquierda para indicar dependencias. ^[8]

Véase también

• Deducción natural
• Cálculo secuencial
• Sistemas deductivos

Notas

1. Pelletier, Francis Jeffry; Hazen, Allen (2024), Zalta, Edward N.; Nodelman, Uri (eds.), "Sistemas de deducción natural en lógica", The Stanford Encyclopedia of Philosophy (edición de primavera de 2024), Metaphysics Research Lab, Stanford University , consultado el 1 de mayo de 2024
2. Véase Lemmon 1965 para una presentación introductoria del sistema de deducción natural de Lemmon.
3. Véase Suppes 1999, págs. 25-150, para una presentación introductoria del sistema de deducción natural de Suppes.
4. Gentzen 1934, Gentzen 1935.
5. Kleene 2002, págs. 50–56, 128–130.
6. 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.
7. Quine (1981). Véanse en particular las páginas 91-93 para la notación de número de línea de Quine para dependencias antecedentes.
8. Una ventaja particular de los sistemas de deducción natural tabular de Kleene es que demuestra la validez de las reglas de inferencia tanto para el cálculo proposicional como para el cálculo de predicados. Véase Kleene 2002, pp. 44-45, 118-119.

Referencias

• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift . 39 (2): 176–210. doi :10.1007/BF01201353. (Traducción al español 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 inicial . Thomas Nelson. ISBN 0-17-712040-1.
• 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 edición). 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). Los documentos recopilados de Gerhard Gentzen . Ámsterdam: Holanda Septentrional.

Enlaces externos

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