Deducción natural

La deducción natural ha tenido una gran variedad de estilos de notación, ^{[ 7 ]} lo que puede dificultar el reconocimiento de una demostración para un lector no familiarizado con alguno de ellos. Para ayudar con esta situación, este artículo incluye una sección de Notación que  explica cómo leer toda la notación que se utilizará. Esta sección simplemente explica la evolución histórica de los estilos de notación, la mayoría de los cuales no se pueden mostrar porque no hay ilustraciones disponibles bajo una licencia de derechos de autor pública ; se remite al lector a la SEP y la IEP para obtener imágenes.

• Gentzen inventó la deducción natural utilizando demostraciones en forma de árbol; consulte la sección «  Notación de árbol de Gentzen» para obtener más detalles.
• Jaśkowski cambió esto a una notación que utilizaba varias cajas anidadas. ^{[ 7 ]}
• Fitch cambió el método de Jaśkowski para dibujar las cajas, creando la notación de Fitch . ^{[ 7 ]}
• 1940: En un libro de texto, Quine ^{[ 8 ]} 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: Una 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 (1978) es una introducción a las demostraciones lógicas utilizando un método basado en el de Suppes , lo que ahora se conoce como notación Suppes-Lemmon .
• 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. ^{[ 9 ]} 

Gentzen , inventor de la deducción natural, tenía su propio estilo de notación para los argumentos. Esto se ejemplificará con un argumento sencillo a continuación. Supongamos que tenemos un ejemplo sencillo de argumento en lógica proposicional , como por ejemplo: "Si llueve, entonces está nublado; está lloviendo; por lo tanto, está nublado". (Esto se presenta en modus ponens ). Si lo representamos como una lista de proposiciones, como es habitual, tendríamos:

${\displaystyle 1)~P\to Q}$

${\displaystyle 2)~P}$

${\displaystyle \therefore ~Q}$

En la notación de Gentzen, ^{[ 7 ]} esto se escribiría así:

${\displaystyle {\frac {P\to Q,P}{Q}}}$

Las premisas se muestran encima de una línea, llamada línea de inferencia , ^{[ 12 ] [ 13 ]} separadas por una coma , que indica combinación de premisas. ^{[ 14 ]} La conclusión se escribe debajo de la línea de inferencia. ^{[ 12 ]} La línea de inferencia representa la consecuencia sintáctica , ^{[ 12 ]} a veces llamada consecuencia deductiva , ^{[ 15 ] [ 16 ]} que también se simboliza con ⊢. ^{[ 16 ]} Por lo tanto, lo anterior también se puede escribir en una sola línea como${\displaystyle P\to Q,P\vdash Q}$. (El torniquete, por su consecuencia sintáctica, tiene menor precedencia que la coma, que representa la combinación de premisas, la cual a su vez tiene menor precedencia que la flecha, utilizada para la implicación material; por lo tanto, no se necesitan paréntesis para interpretar esta fórmula.) ^{[ 14 ]}

La consecuencia sintáctica se contrasta con la consecuencia semántica , ^{[ 17 ]} que se simboliza con ⊧. ^{[ 18 ] [ 16 ]} En este caso, la conclusión se deduce sintácticamente porque la deducción natural es un sistema de prueba sintáctico , que asume las reglas de inferencia como primitivas .

El estilo de Gentzen se utilizará en gran parte de este artículo. Las anotaciones de descarga de Gentzen, utilizadas para internalizar juicios hipotéticos, pueden evitarse representando las pruebas como un árbol de secuencias Γ  ⊢ A en lugar de un árbol de juicios que afirman que A (es verdadero). 

Muchos libros de texto utilizan la notación de Suppes-Lemmon , ^{[ 7 ]} por lo que este artículo también la incluirá, aunque por ahora solo se aplica a la lógica proposicional y el resto del contenido se presenta únicamente en el estilo Gentzen. Una demostración , presentada de acuerdo con la notación de Suppes-Lemmon , es una secuencia de líneas que contienen oraciones, ^{[ 19 ]} donde cada oración es una suposición o el resultado de aplicar una regla de demostración a oraciones anteriores de la secuencia. ^{[ 19 ]} Cada línea de demostración se compone de una oración de demostración , junto con su anotación , su conjunto de suposiciones y el número de línea actual . ^{[ 19 ]} El conjunto de suposiciones enumera las suposiciones de las que depende la oración de demostración dada, a las que se hace referencia mediante los números de línea. ^{[ 19 ]} La anotación especifica qué regla de demostración se aplicó y a qué líneas anteriores para obtener la oración actual. ^{[ 19 ]} Aquí hay un ejemplo de demostración:

Esta demostración se aclarará cuando se especifiquen las reglas de inferencia y sus anotaciones apropiadas; véase §  Reglas de inferencia proposicional (estilo Suppes-Lemmon) .

En el cálculo proposicional clásico, el lenguaje formal${\displaystyle {\mathcal {L}}}$se define habitualmente (aquí: por recursión ) de la siguiente manera: ^{[ 20 ]}

1. Cada variable proposicional es una fórmula .
2. "${\displaystyle \bot }$" es una fórmula.
3. Si${\displaystyle \varphi }$y${\displaystyle \psi }$son fórmulas, también lo son${\displaystyle (\varphi \land \psi )}$,${\displaystyle (\varphi \lor \psi )}$,${\displaystyle (\varphi \to \psi )}$,${\displaystyle (\varphi \leftrightarrow \psi )}$.
4. Nada más es una fórmula.

Negación (${\displaystyle \neg }$) se define como implicación a la falsedad

${\displaystyle \neg \phi \;{\overset {\text{def}}{=}}\;\phi \to \bot }$,

dónde${\displaystyle \bot }$(falsum) representa una contradicción o falsedad absoluta. ^{[ 21 ] [ 22 ] [ 23 ] [ 24 ] [ 25 ]}

Las publicaciones más antiguas, y las que no se centran en sistemas lógicos como los sistemas mínimos , intuicionistas o de Hilbert , toman la negación como un conector lógico primitivo , lo que significa que se asume como una operación básica y no se define en términos de otros conectores. ^{[ 26 ] [ 27 ]} Algunos autores, como Bostock , utilizan${\displaystyle \bot }$y${\displaystyle \top }$y también definir${\displaystyle \neg }$como primitivos. ^{[ 28 ] [ 29 ]}

También se puede dar una definición de sintaxis utilizando la  notación de árbol de Gentzen , escribiendo fórmulas bien formadas debajo de la línea de inferencia y cualquier variable esquemática utilizada por esas fórmulas encima de ella. ^{[ 26 ]} Por ejemplo, el equivalente de las reglas 3 y 4, de la definición de Bostock anterior, se escribe de la siguiente manera:

${\displaystyle {\frac {\varphi }{(\neg \varphi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \lor \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \land \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \rightarrow \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \leftrightarrow \psi )}}}$.

Una convención de notación diferente considera la sintaxis del lenguaje como una gramática categorial con la única categoría "fórmula", denotada por el símbolo${\displaystyle {\mathcal {F}}}$. Así pues, cualquier elemento de la sintaxis se introduce mediante categorizaciones, para las cuales la notación es${\displaystyle \varphi$ :{\mathcal {F}}} , que significa "${\displaystyle \varphi }$es una expresión para un objeto en la categoría${\displaystyle {\mathcal {F}}}$." ^{[ 30 ]} Las letras de las oraciones, entonces, se introducen mediante categorizaciones como${\displaystyle P:{\mathcal {F}}}$, ${\displaystyle Q:{\mathcal {F}}}$, ${\displaystyle R:{\mathcal {F}}}$y así sucesivamente; ^{[ 30 ]} los conectores, a su vez, se definen mediante enunciados similares a los anteriores, pero utilizando la notación de categorización, como se ve a continuación:

En el resto de este artículo, el${\displaystyle \varphi$ La notación de categorización :{\mathcal {F}}} se utilizará para cualquier declaración en notación Gentzen que defina la gramática del lenguaje; cualquier otra declaración en notación Gentzen serán inferencias, que afirman que sigue un secuente en lugar de que una expresión sea una fórmula bien formada.

Dejemos que el lenguaje proposicional${\displaystyle {\mathcal {L}}}$ser definido inductivamente como${\displaystyle \Phi$ ::=p_{1},p_{2},\dots \mid \bot \mid (\Phi \to \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )} .

Defina la negación como${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,(\Phi \to \bot )}$.

La siguiente es una lista de reglas de inferencia primitivas para la deducción natural en lógica proposicional: ^{[ 31 ] [ 26 ]}

En esta tabla las letras griegas${\displaystyle \varphi ,\psi ,\chi }$son esquemas , que abarcan fórmulas en lugar de solo proposiciones atómicas. El nombre de una regla se da a la derecha de su árbol de fórmulas. Por ejemplo, la primera regla de introducción se llama${\displaystyle \land _{I}}$, que es la abreviatura de "introducción de la conjunción".

• Lógica mínima : las reglas de deducción natural son${\displaystyle ND_{MPC}=\{\land _{I},\land _{E},\lor _{I},\lor _{E},\to _{I},\to _{E}\}}$.

Sin las reglas${\displaystyle \bot _{E}}$y${\displaystyle \neg \neg _{E}}$El sistema define una lógica mínima (como lo discute Johansson ). ^{[ 33 ]}

• Lógica intuicionista : las reglas de deducción natural son${\displaystyle ND_{IPC}=ND_{MPC}\cup \{\bot _{E}\}}$.

Cuando la regla${\displaystyle \bot _{E}}$( El principio de explosión ) se agrega a las reglas de la lógica mínima, el sistema define la lógica intuicionista.

La declaración${\displaystyle P\to \neg \neg P}$es válido (ya en lógica mínima, ver ejemplo 1 a continuación), a diferencia de la implicación inversa que implicaría la ley del tercero excluido .

• Lógica clásica : las reglas de deducción natural son${\displaystyle ND_{CPC}=ND_{IPC}\cup \{\neg \neg _{E}\}}$. ^{[ 32 ]}

Cuando se admiten todas las reglas de deducción natural enumeradas, el sistema define la lógica clásica. ^{[ 34 ] [ 35 ] [ 36 ]}

Ejemplo 1 : ^{[ 24 ]} Prueba, dentro de la lógica mínima, de${\displaystyle P\to \neg \neg P}$.

Meta:${\displaystyle P\to ((P\to \bot )\to \bot )}$ Prueba:

${\displaystyle {\cfrac {{\cfrac {[P]^{v}\qquad [P\to \bot ]^{u}}{\bot }}\to _{E}}{{\cfrac {((P\to \bot )\to \bot )}{P\to ((P\to \bot )\to \bot )}}\to _{I^{v}}}}\to _{I^{u}}}$

Ejemplo 2 : Prueba, dentro de la lógica mínima, de${\displaystyle A\to \left(B\to \left(A\land B\right)\right)}$:

${\displaystyle {\cfrac {{\cfrac {[A]^{u}\quad [B]^{w}}{A\land B}}\ \land _{I}}{{\cfrac {B\to \left(A\land B\right)}{A\to \left(B\to \left(A\land B\right)\right)}}\ \to _{I^{u}}}}\ \to _{I^{w}}}$

La presentación lineal empleada en las demostraciones al estilo de Fitch y Suppes-Lemmon —con números de línea y alineación vertical/conjuntos de supuestos— permite visualizar claramente las subdemostraciones. Fitch utilizó reglas derivadas con moderación y cautela . Suppes-Lemmon fue más allá y añadió reglas derivadas al conjunto de reglas de deducción natural.

Suppes introdujo la deducción natural utilizando reglas al estilo de Gentzen. ^{[ 37 ]}

• Definió la negación en términos de contradicción:${\displaystyle \neg P\equiv (P\to \bot )}$.
• Explicó explícitamente las reglas derivadas, aunque no siempre las distinguió claramente de las primitivas en cuanto a la disposición.
• Su sistema es casi minimalista, pero permite pasos derivados para mayor brevedad.

Lemmon formalizó reglas más derivadas. ^{[ 38 ]} También definió la negación como implicación de falsedad:${\displaystyle \neg P\equiv P\to \bot }$Esto no se enuncia como una definición formal en Lógica Inicial , pero se asume implícitamente en todo el sistema, como lo demuestra lo siguiente:

• Uso de RAA (Reductio ad Absurdum): Lemmon utiliza regularmente RAA en la forma: Supongamos${\displaystyle P}$derivar${\displaystyle \bot }$, luego concluir${\displaystyle \neg P}$.
  • Esto solo funciona si${\displaystyle \neg P}$se entiende como${\displaystyle P\to \bot }$.
• Pruebas que implican contradicción: Lemmon utilizó el hecho de que de${\displaystyle \neg P\land P}$uno puede derivar${\displaystyle \bot }$.
  • Esto requiere tratamiento${\displaystyle \neg P}$como${\displaystyle P\to \bot }$, de modo que el modus ponens produce contradicción.
• Ausencia de una regla primitiva para el símbolo “¬”: Lemmon no incluyó una regla independiente para introducir o eliminar el símbolo ¬. En cambio, derivó la negación mediante implicación y contradicción.

En la tabla siguiente, basada en Lemmon (1978) ^{[ 39 ]} y Allen & Hand (2022), ^{[ 19 ]} se resaltan las reglas derivadas de Lemmon . Estas pueden derivarse de las reglas de Gentzen (no resaltadas) .

Hay nueve reglas primitivas de prueba, que son la regla de suposición , más cuatro pares de reglas de introducción y eliminación para los conectivos binarios, y las reglas de doble negación y reducción al absurdo , de las cuales solo se necesita una. ^{[ 32 ] [ 19 ]} El silogismo disyuntivo puede usarse como una alternativa más sencilla a la eliminación ∨ propia, ^{[ 19 ]} y MTT es una regla comúnmente dada, ^{[ 39 ]} aunque no es primitiva. ^{[ 19 ]}

Recordemos que ya se dio un ejemplo de demostración al introducir la notación de  Suppes-Lemmon . Este es un segundo ejemplo.

Si Γ ⊢ π ₁  : A y Γ, u : A ⊢ π ₂  : B , entonces Γ ⊢ [π ₁ / u ] π ₂  : B.

Hasta ahora, la proposición "Γ ⊢ π  : A " ha tenido una interpretación puramente lógica. En la teoría de tipos , la visión lógica se reemplaza por una visión más computacional de los objetos. Las proposiciones en la interpretación lógica se consideran ahora tipos , y las pruebas, programas en el cálculo lambda . Así, la interpretación de "π  : A " es " el programa π es de tipo A ". Los conectores lógicos también reciben una lectura diferente: la conjunción se considera producto (×), la implicación, flecha de función (→), etc. Sin embargo, las diferencias son meramente estéticas. La teoría de tipos tiene una presentación deductiva natural en términos de reglas de formación, introducción y eliminación; de hecho, el lector puede reconstruir fácilmente lo que se conoce como teoría de tipos simple a partir de las secciones anteriores.

La diferencia entre lógica y teoría de tipos es principalmente un cambio de enfoque de los tipos (proposiciones) a los programas (pruebas). La teoría de tipos está interesada principalmente en la convertibilidad o reducibilidad de los programas. Para cada tipo, hay programas canónicos de ese tipo que son irreducibles; estos se conocen como formas o valores canónicos . Si cada programa puede reducirse a una forma canónica, entonces se dice que la teoría de tipos es normalizadora (o débilmente normalizadora ). Si la forma canónica es única, entonces se dice que la teoría es fuertemente normalizadora . La normalizabilidad es una característica rara de la mayoría de las teorías de tipos no triviales, lo que es una gran desviación del mundo lógico. (Recordemos que casi toda derivación lógica tiene una derivación normal equivalente). Para esbozar la razón: en las teorías de tipos que admiten definiciones recursivas, es posible escribir programas que nunca se reducen a un valor; a tales programas de bucle generalmente se les puede dar cualquier tipo. En particular, el programa de bucle tiene el tipo ⊥, aunque no hay prueba lógica de "⊥". Por esta razón, las proposiciones como tipos; El paradigma de las demostraciones como programas solo funciona en una dirección, si es que funciona: interpretar una teoría de tipos como una lógica generalmente da como resultado una lógica inconsistente.

Al igual que la lógica, la teoría de tipos tiene muchas extensiones y variantes, incluyendo versiones de primer orden y de orden superior. Una rama, conocida como teoría de tipos dependientes , se utiliza en varios sistemas de demostración asistida por computadora . La teoría de tipos dependientes permite que los cuantificadores abarquen los propios programas. Estos tipos cuantificados se escriben como Π y Σ en lugar de ∀ y ∃, y tienen las siguientes reglas de formación:

Estos tipos son generalizaciones de los tipos flecha y producto, respectivamente, como lo demuestran sus reglas de introducción y eliminación.

La teoría de tipos dependientes, en su máxima generalidad, es muy potente: permite expresar prácticamente cualquier propiedad imaginable de los programas directamente en sus tipos. Esta generalidad tiene un alto precio : o bien la verificación de tipos es indecidible ( teoría de tipos extensional ), o bien el razonamiento extensional es más difícil ( teoría de tipos intensional ). Por este motivo, algunas teorías de tipos dependientes no permiten la cuantificación sobre programas arbitrarios, sino que se restringen a programas de un dominio de índice decidible dado , por ejemplo, enteros, cadenas o programas lineales.

Dado que las teorías de tipos dependientes permiten que los tipos dependan de los programas, surge la pregunta natural de si es posible que los programas dependan de los tipos, o de cualquier otra combinación. Existen diversas respuestas a estas preguntas. Un enfoque popular en la teoría de tipos consiste en permitir que los programas se cuantifiquen sobre los tipos, también conocido como polimorfismo paramétrico ; de este hay dos tipos principales: si los tipos y los programas se mantienen separados, se obtiene un sistema algo más ordenado llamado polimorfismo predicativo ; si la distinción entre programa y tipo se difumina, se obtiene el análogo en teoría de tipos de la lógica de orden superior, también conocido como polimorfismo impredicativo . En la literatura se han considerado diversas combinaciones de dependencia y polimorfismo, siendo la más famosa el cubo lambda de Henk Barendregt .

La intersección entre la lógica y la teoría de tipos constituye un área de investigación vasta y activa. Las nuevas lógicas suelen formalizarse en un marco teórico de tipos general, conocido como marco lógico . Marcos lógicos modernos populares, como el cálculo de construcciones y la lógica de Fourier, se basan en la teoría de tipos dependientes de orden superior, con diversas ventajas y desventajas en términos de decidibilidad y poder expresivo. Estos marcos lógicos se especifican siempre como sistemas de deducción natural, lo que demuestra la versatilidad del enfoque de la deducción natural.

Si Ω;⋅ ⊢ π ₁  : A y Ω, u : ( A válida )  ; Γ ⊢ π ₂  : C , entonces Ω;Γ ⊢ [π ₁ / u ] π ₂  : C .

Este marco de separación de juicios en conjuntos distintos de hipótesis, también conocido como contextos multizonales o poliádicos , es muy potente y extensible; se ha aplicado a muchas lógicas modales diferentes, y también a lógicas lineales y otras lógicas subestructurales , por mencionar algunos ejemplos. Sin embargo, relativamente pocos sistemas de lógica modal pueden formalizarse directamente en la deducción natural. Para dar caracterizaciones teóricas de la demostración de estos sistemas, se necesitan extensiones como el etiquetado o sistemas de inferencia profunda.

La adición de etiquetas a las fórmulas permite un control mucho más preciso de las condiciones bajo las cuales se aplican las reglas, lo que permite aplicar las técnicas más flexibles de los tableaux analíticos , como se ha hecho en el caso de la deducción etiquetada . Las etiquetas también permiten nombrar mundos en la semántica de Kripke; Simpson (1994) presenta una técnica influyente para convertir las condiciones de marco de las lógicas modales en la semántica de Kripke en reglas de inferencia en una formalización de deducción natural de la lógica híbrida . Stouppa (2004) examina la aplicación de muchas teorías de la prueba, como los hipersecuentes de Avron y Pottinger y la lógica de visualización de Belnap a lógicas modales como S5 y B.

Si Γ ⇒ π ₁  : A y Γ, u : A ⇒ π ₂  : C , entonces Γ ⇒ [π ₁ /u] π ₂  : C .

En la mayoría de las lógicas bien comportadas, la regla de corte es innecesaria como regla de inferencia, aunque sigue siendo demostrable como metateorema ; la superfluidad de la regla de corte se suele presentar como un proceso computacional, conocido como eliminación de corte . Esto tiene una aplicación interesante para la deducción natural; por lo general, es extremadamente tedioso demostrar ciertas propiedades directamente en la deducción natural debido a un número ilimitado de casos. Por ejemplo, consideremos demostrar que una proposición dada no es demostrable en la deducción natural. Un argumento inductivo simple falla debido a reglas como ∨E o E, que pueden introducir proposiciones arbitrarias. Sin embargo, sabemos que el cálculo de secuentes es completo con respecto a la deducción natural, por lo que basta con demostrar esta indemostrabilidad en el cálculo de secuentes. Ahora bien, si la regla de corte no está disponible como regla de inferencia, entonces todas las reglas de secuentes introducen un conector a la derecha o a la izquierda, por lo que la profundidad de una derivación de secuentes está completamente limitada por los conectores en la conclusión final. Por lo tanto, demostrar la imposibilidad de demostración es mucho más sencillo, ya que solo hay un número finito de casos a considerar, y cada caso se compone enteramente de subproposiciones de la conclusión. Un ejemplo sencillo de esto es el teorema de consistencia global : "⋅ ⊢ ⊥" no es demostrable. En la versión del cálculo de secuentes, esto es manifiestamente cierto, ¡porque no existe ninguna regla que pueda tener "⋅ ⇒ ⊥" como conclusión! Los teóricos de la demostración suelen preferir trabajar con formulaciones del cálculo de secuentes sin cortes debido a estas propiedades.

• Allen, Colin; Hand, Michael (2022). Introducción a la lógica (3.ª  ed.). Cambridge, Massachusetts: The MIT Press. ISBN 978-0-262-54364-4.
• Arthur, Richard TW (2017). Introducción a la lógica: uso de la deducción natural, argumentos reales, un poco de historia y algo de humor (2.ª  ed.). Peterborough, Ontario: Broadview Press. ISBN 978-1-55481-332-2OCLC 962129086​​ 
• Ayala Rincón, Mauricio; de Moura, Flávio LC (2017). Lógica Aplicada para Informáticos . Temas de Pregrado en Ciencias de la Computación. Saltador. doi : 10.1007/978-3-319-51653-0 . ISBN 978-3-319-51651-6.
• Barker-Plummer, Dave; Barwise, Jon ; Etchemendy, John (2011). Language Proof and Logic (2.ª  ed.). CSLI Publications. ISBN 978-1575866321.
• Bostock, David (1997). Lógica intermedia . Oxford; Nueva York: Clarendon Press; Oxford University Press. ISBN 978-0-19-875141-0.
• Gallier, Jean (2005). "Lógicas constructivas. Parte I: Un tutorial sobre sistemas de prueba y λ-cálculos tipados" . Archivado del original el 5 de julio de 2017. Recuperado el 12 de junio de 2014 .
• Gentzen, Gerhard Karl Erich (1935a). "Untersuchungen über das logische Schließen. Yo" . Mathematische Zeitschrift . 39 (2): 176– 210. doi : 10.1007/bf01201353 . S2CID 121546341 . Archivado desde el original el 24 de diciembre de 2015. 

— (1964) [1935]. "Investigaciones sobre la deducción lógica". American Philosophical Quarterly . 1 (4): 249– 287.

• Gentzen, Gerhard Karl Erich (1935b). "Untersuchungen über das logische Schließen. II" . Mathematische Zeitschrift . 39 (3): 405– 431. doi : 10.1007/bf01201363 . S2CID 186239837 . {{cite journal}}: CS1 maint: servicio de archivado obsoleto ( enlace )

— (1965) [1935]. "Investigaciones sobre la deducción lógica". American Philosophical Quarterly . 2 (3): 204– 218.

• Girard, Jean-Yves (1990). Pruebas y tipos . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, Inglaterra. Archivado del original el 4 de julio de 2016. Recuperado el 20 de abril de 2006 .Traducido y con apéndices por Paul Taylor e Yves Lafont.
• Hansson, Sven Ove; Hendricks, Vincent F. (2018). Introducción a la filosofía formal . Textos de pregrado en filosofía de Springer. Cham: Springer. ISBN 978-3-030-08454-7.
• Jaśkowski, Stanisław (1934). Sobre las reglas de las suposiciones en lógica formal .Reimpreso en Lógica polaca 1920-39 , ed. Storrs McCall.
• Johansson, Ingebrigt (1937). "Der Minimalkalkül, un reduzierter intuitionistischer Formalismus" . Compositio Mathematica (en alemán). 4 : 119-136 .
• Kleene, Stephen Cole (1980) [1952]. Introducción a la metamatemática (Undécima  ed.). North-Holland. ISBN 978-0-7204-2103-3.
• 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: Dover Publications. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1978) [1965]. Lógica básica (Quinta reimpresión,  edición de 1985). Boca Raton, FL: Hackett Publishing Company . ISBN 0915144-50-6.
• Magnus, PD; Button, Tim; Trueman, Robert; Zach, Richard (2023). forall x: Una introducción a la lógica formal (  edición de otoño de 2023). Open Logic Project . Recuperado el 4 de mayo de 2025 .
• Martin-Löf, Per (1996). «Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas» (PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11– 60. Archivado del original (PDF) el 8 de diciembre de 2023. Recuperado el 2 de julio de 2010 .Apuntes de conferencias de un curso breve en la Università degli Studi di Siena, abril de 1983.
• Paseau, AC; Leek, Robert. "El teorema de la compacidad" . Enciclopedia de filosofía en Internet . Consultado el 22 de marzo de 2024 .
• Paseau, Alexander; Pregel, Fabian (2023), "Deductivismo en la filosofía de las matemáticas" , en Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (  edición de otoño de 2023), Metaphysics Research Lab, Universidad de Stanford , consultado el 22 de marzo de 2024.
• Pelletier, Francis Jeffry; Hazen, Allen (2024), "Sistemas de deducción natural en lógica" , en Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (  edición de primavera de 2024), Metaphysics Research Lab, Universidad de Stanford , consultado el 22 de marzo de 2024.
• Pfenning, Frank; Davies, Rowan (2001). "Una reconstrucción de juicio de la lógica modal" (PDF) . Estructuras matemáticas en informática . 11 (4): 511– 540. CiteSeerX 10.1.1.43.1611 . doi : 10.1017/S0960129501003322 . S2CID 16467268 .  
• Prawitz, Dag (1965). Deducción natural: un estudio de teoría de la prueba . Acta Universitatis Stockholmiensis; Estudios de Filosofía de Estocolmo, 3 . Estocolmo, Gotemburgo, Uppsala: Almqvist & Wiksell . OCLC 912927896 . 
• Prawitz, Dag (2006). Deducción natural: un estudio de teoría de la demostración . Mineola, Nueva York: Dover Publications. ISBN 9780486446554OCLC 61296001​​ 
• 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.
• Restall, Greg (2018), "Lógicas subestructurales" , en Zalta, Edward N. (ed.), La enciclopedia de filosofía de Stanford (  edición de primavera de 2018), Laboratorio de investigación metafísica, Universidad de Stanford , consultado el 22 de marzo de 2024.
• Simpson, Alex K. (1994). La teoría de la demostración y la semántica de la lógica modal intuicionista (PDF) (Tesis). Archivo de Investigación de Edimburgo (ERA) . hdl : 1842/407 .
• Stoll, Robert Roth (1979) [1963]. Teoría de conjuntos y lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-63829-4.
• Stouppa, Phiniki (2004). El diseño de teorías de demostración modales: el caso de S5 . Universidad de Dresde. CiteSeerX 10.1.1.140.1858 . Tesis de maestría.
• Suppes, Patrick Colonel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Dover Publications. ISBN 978-0-486-40687-9.
• Sutcliffe, Geoff. "Lógica proposicional" . www.cs.miami.edu . Universidad de Miami . Consultado el 4 de mayo de 2025 .
• Tennant, Neil (1990) [1978]. Lógica natural (1.ª ed., reimpresión con correcciones  ). Edinburgh University Press . ISBN 0852245793.
• Van Dalen, Dirk (2013) [1980]. Lógica y Estructura . Universitext (5  ed.). Londres, Heidelberg, Nueva York, Dordrecht: Springer . doi : 10.1007/978-1-4471-4558-5 . ISBN 978-1-4471-4558-5.
• von Plato, Jan (2013). Elementos del razonamiento lógico (1.ª  ed. publicada). Cambridge: Cambridge University Press . ISBN 978-1-107-03659-8.
• Weisstein, Eric W. "Conectivo" . mathworld.wolfram.com . Consultado el 22 de marzo de 2024 .