El sistema L es una lógica deductiva natural desarrollada por EJ Lemmon . [1] Derivado del método de Suppes , [2] representa pruebas de deducción natural como secuencias de pasos justificados. Ambos métodos se derivan del sistema de deducción natural de Gentzen de 1934/1935, [3] en el que las demostraciones se presentaron 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. [4] 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 con barras que corren a la izquierda de la tabla. para indicar dependencias. Sin embargo, la versión de Kleene tiene la ventaja de que se presenta, aunque sólo de forma muy esquemática, dentro de un marco riguroso de teoría metamatemática, mientras que los libros de Suppes [2] y Lemmon [1] son aplicaciones del diseño tabular para enseñar lógica introductoria.
Descripción del sistema deductivo
El sistema L es un cálculo de predicados con igualdad, por lo que su descripción se puede dividir 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 sostienen:
- Un conjunto de enteros positivos, posiblemente vacíos
- Un entero positivo
- Una fórmula bien formada (o wff)
- Un conjunto de números, posiblemente vacío; una regla; y posiblemente una referencia a otra prueba
Lo siguiente es un ejemplo:
p → q , ¬ q ⊢ ¬ p [Modus Tollendo Tollens (MTT)] | |||
Número de suposición | Número de línea | Fórmula ( wff ) | Líneas en uso y justificación |
---|---|---|---|
1 | (1) | p → q | A |
2 | (2) | ¬ q | A |
3 | (3) | pag | A (para RAA) |
1, 3 | (4) | q | 1, 3, MPP |
1, 2, 3 | (5) | q ∧ ¬ q | 2, 4, ∧I |
1, 2 | (6) | ¬ p | 3, 5, RAA |
QED |
La segunda columna contiene números de línea. El tercero tiene una wff, que está justificada por la regla contenida en el cuarto junto con información auxiliar sobre otras wff, posiblemente en otras pruebas. La primera columna representa los números de línea de los supuestos sobre los que se basa la wff, determinados por la aplicación de la regla citada en contexto. Cualquier línea de cualquier prueba válida se puede convertir en una secuencia enumerando las wffs en las líneas citadas como premisas y las wff en la línea como conclusión. De manera análoga, se pueden convertir en condicionales donde el antecedente es una conjunción. Estos secuentes a menudo se enumeran encima de la prueba, como Modus Tollens está arriba.
Reglas de 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 un secuente, debemos cumplir con reglas cuidadosamente especificadas. Las reglas se pueden dividir en cuatro grupos: las reglas proposicionales (1-10), las reglas del 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 predicados, luego un cálculo de predicados con igualdad, luego un cálculo de predicados con igualdad que permite la derivación de nuevas reglas. Algunas de las reglas de cálculo proposicional, como MTT, son superfluas y pueden derivarse como reglas de otras reglas.
- La regla de suposición (A): "A" justifica cualquier wff. La única suposición es su propio número de línea.
- Modus Ponendo Ponens (MPP): Si hay líneas ayb 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 ay b.
- La regla de la prueba condicional (CP): Si una línea con la proposición P tiene una línea de suposición b con la proposición Q, "b, a CP" justifica Q → P. Se mantienen todas las suposiciones de a aparte de b.
- La regla de la doble negación (DN): "un DN" justifica sumar o restar dos símbolos de negación de la wff en una línea a previamente en la prueba, lo que hace que esta regla sea bicondicional. El grupo de supuestos es el de la línea citada.
- La regla de ∧-introducción (∧I): Si las proposiciones P y Q están en las líneas ayb, "a, b ∧I" justifica P∧Q. Los supuestos son el conjunto colectivo de proposiciones conjuntas.
- La regla de ∧-eliminación (∧E): Si la línea a es una conjunción P∧Q, se puede concluir P o Q usando "a ∧E". Las suposiciones son de línea a. ∧I y ∧E permiten la monotonicidad de la implicación , ya que cuando una proposición P se une con Q con ∧I y se separa con ∧E, retiene los supuestos de Q.
- La regla de ∨-introducción (∨I): Para una línea a con proposición P se puede introducir P∨Q citando "a ∨I". Las suposiciones son a.
- La regla de ∨-eliminación (∨E): Para una disyunción P∨Q, si uno asume P y Q y por separado llega a la conclusión R de cada uno, 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 byd suponen P y Q respectivamente, y las líneas cy e son R con P y Q en sus respectivos grupos de supuestos. Los supuestos son los grupos colectivos de las dos líneas que concluyen R menos las líneas de P y Q, by d.
- Reductio Ad Absurdum (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, a RAA" y derivar ¬Q de los supuestos de la línea a aparte de b.
- Modus Tollens (MTT): Para las proposiciones P → Q y ¬Q en las líneas ayb se puede citar "a, b MTT" para derivar ¬P. Los supuestos son los de las líneas ay b. Esto se demuestra a partir de otras reglas anteriores.
- Introducción universal (UI): para un predicado en la línea a, se puede citar "una interfaz de usuario" para justificar una cuantificación universal,, siempre que ninguno de los supuestos en la línea a tenga el término en cualquier lugar. Los supuestos son los de la línea a.
- Eliminación universal (UE): para un predicado cuantificado universalmente en la línea a, se puede citar "un UE" para justificar . Los supuestos son los de la línea a. UE es una dualidad con UI en el sentido de que uno puede cambiar entre variables cuantificadas y libres usando estas reglas.
- Introducción existencial (IE): para un predicado en línea se puede citar "un IE" para justificar una cuantificación existencial, . Los supuestos son los de la línea a.
- Eliminación existencial (EE): para un predicado cuantificado existencialmente en la línea a, si asumimos para ser cierto en la línea by derivar 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, ninguno de sus supuestos aparte de la línea b, o en la línea a. Por esta razón EE y EI están en dualidad, como se puede suponer y utilice la IE para llegar a una conclusión de , ya que la IE eliminará la conclusión del término . Los supuestos son los supuestos de la línea ay los de la línea c además de b.
- Introducción a la igualdad (= I): En cualquier momento se puede introducir citando "= I" sin suposiciones.
- Eliminación de igualdad (= E): para proposiciones y P en las líneas a y b, se puede citar "a, b = E" para justificar el cambio de términos términos en P a . Los supuestos son el conjunto de ay b.
- Instancia de sustitución (SI (S)): para una secuencia probado en la prueba X y casos de sustitución de y en las líneas ayb, se puede citar "a, b SI (S) X" para justificar la introducción de una instancia de sustitución de . Los supuestos son los de las líneas ay b. Una regla derivada sin supuestos es un teorema y puede introducirse en cualquier momento sin supuestos. Algunos lo citan como "TI (S)", para "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.
Ejemplos de
Un ejemplo de la demostración de un secuente (un teorema en este caso):
⊢ p ∨ ¬ p | |||
Número de suposición | Número de línea | Fórmula ( wff ) | Líneas en uso y justificación |
---|---|---|---|
1 | (1) | ¬ ( p ∨ ¬ p ) | A (para RAA) |
2 | (2) | pag | A (para RAA) |
2 | (3) | ( p ∨ ¬ p ) | 2, ∨I |
1, 2 | (4) | ( p ∨ ¬ p ) ∧ ¬ ( p ∨ ¬ p ) | 3, 1, ∧I |
1 | (5) | ¬ p | 2, 4, RAA |
1 | (6) | ( p ∨ ¬ p ) | 5, ∨I |
1 | (7) | ( p ∨ ¬ p ) ∧ ¬ ( p ∨ ¬ p ) | 1, 6, ∧I |
(8) | ¬¬ ( p ∨ ¬ p ) | 1, 7, RAA | |
(9) | ( p ∨ ¬ p ) | 8, DN | |
QED |
Una prueba del principio de explosión utilizando la monotonicidad de la vinculación. Algunos han llamado a la siguiente técnica, demostrada en las líneas 3-6, la Regla de Aumento (Finito) de Locales: [5]
p , ¬ p ⊢ q | |||
Número de suposición | Número de línea | Fórmula ( wff ) | Líneas en uso y justificación |
---|---|---|---|
1 | (1) | pag | A (para RAA) |
2 | (2) | ¬ p | A (para RAA) |
1, 2 | (3) | p ∧ ¬ p | 1, 2, ∧I |
4 | (4) | ¬ q | A (para DN) |
1, 2, 4 | (5) | ( p ∧ ¬ p ) ∧ ¬ q | 3, 4, ∧I |
1, 2, 4 | (6) | p ∧ ¬ p | 5, ∨E |
1, 2 | (7) | ¬¬ q | 4, 6, RAA |
1, 2 | (8) | q | 7, DN |
QED |
Un ejemplo de sustitución y ∨E:
( p ∧ ¬ p ) ∨ ( q ∧ ¬ q ) ⊢ r | |||
Número de suposición | Número de línea | Fórmula ( wff ) | Líneas en uso y justificación |
---|---|---|---|
1 | (1) | ( p ∧ ¬ p ) ∨ ( q ∧ ¬ q ) | A |
2 | (2) | p ∧ ¬ p | A (para ∨E) |
2 | (3) | pag | 2 ∧E |
2 | (4) | ¬ p | 2 ∧E |
2 | (5) | r | 3, 4 SI (S) ver prueba anterior |
6 | (6) | q ∧ ¬ q | A (para ∨E) |
6 | (7) | q | 6 ∧E |
6 | (8) | ¬ q | 2 ∧E |
6 | (9) | r | 7, 8 SI (S) ver prueba anterior |
1 | (10) | r | 1, 2, 5, 6, 9, ∨E |
QED |
Historia de los sistemas tabulares de deducción natural
El desarrollo histórico de los sistemas de deducción natural de diseño tabular, 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 [6] indicó las dependencias precedentes mediante números de línea entre corchetes, anticipando la notación de número de línea de 1957 de Suppes.
- 1950: En un libro de texto, Quine (1982 , págs. 241-255) demostró un método para usar 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á del todo 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 al teorema de la lógica práctica demostrada en un libro de texto por Suppes (1999 , págs. 25-150). Esto indica las dependencias (es decir, las proposiciones precedentes) por los números de línea a la izquierda de cada línea.
- 1963: Stoll (1979 , págs. 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 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 demostraciones lógicas prácticas, un sistema usando citas explícitas de proposiciones antecedentes a la izquierda de cada línea, el otro sistema usando barras verticales -líneas a la izquierda para indicar dependencias. [7]
Ver también
Notas
- ^ a b Véase Lemmon 1965 para una presentación introductoria del sistema de deducción natural de Lemmon.
- ^ a b Véase Suppes 1999 , págs. 25-150, para una presentación introductoria del sistema de deducción natural de Suppes.
- ^ Gentzen 1934 , Gentzen 1935 .
- ^ Kleene 2002 , págs. 50–56, 128–130.
- ^ Coburn, Barry; Miller, David (octubre de 1977). "Dos comentarios sobre la lógica del comienzo de Lemmon" . Diario de Notre Dame de lógica formal . 18 (4): 607–610. doi : 10.1305 / ndjfl / 1093888128 . ISSN 0029-4527 .
- ^ Quine (1981) . Vea particularmente las páginas 91–93 para la notación de números de línea de Quine para las dependencias de antecedentes.
- ↑ Una ventaja particular de los sistemas tabulares de deducción natural 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 , págs. 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 .(Traducciones al inglés 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: Publicaciones de Dover. 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 (Ed. 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]. Establecer teoría y lógica . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-63829-4.
- Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-40687-9.
- Szabo, ME (1969). Los artículos recopilados de Gerhard Gentzen . Amsterdam: Holanda Septentrional.
enlaces externos
- Pelletier, Jeff, " Una historia de la deducción natural y los libros de texto de lógica elemental " .