Deducción natural

En lógica y teoría de la demostración, la deducción natural es un tipo de cálculo de demostración en el que el razonamiento lógico se expresa mediante reglas de inferencia estrechamente relacionadas con las reglas "naturales" manera de razonar. Esto contrasta con los sistemas de estilo Hilbert, que en su lugar utilizan axiomas tanto como sea posible para expresar las leyes lógicas del razonamiento deductivo.

Motivación

La deducción natural surgió de un contexto de insatisfacción con las axiomatizaciones del razonamiento deductivo comunes a los sistemas de Hilbert, Frege y Russell (ver, por ejemplo, el sistema de Hilbert). Tales axiomatizaciones fueron las más conocidas por Russell y Whitehead en su tratado matemático Principia Mathematica. Estimulado por una serie de seminarios en Polonia en 1926 por Łukasiewicz que defendía un tratamiento más natural de la lógica, Jaśkowski hizo los primeros intentos de definir una deducción más natural, primero en 1929 usando una notación esquemática y luego actualizando su propuesta en una secuencia de artículos en 1934 y 1935. Sus propuestas llevaron a diferentes notaciones como el cálculo al estilo de Fitch (o diagramas de Fitch) o Suppes' método para el cual Lemmon dio una variante llamada sistema L.

La deducción natural en su forma moderna fue propuesta de forma independiente por el matemático alemán Gerhard Gentzen en 1934, en una disertación presentada en la facultad de ciencias matemáticas de la Universidad de Göttingen. El término deducción natural (o mejor dicho, su equivalente alemán natürliches Schließen) fue acuñado en ese artículo:

Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. Así ergab sich ein "Kalkül des natürlichen Schließens".
(Primero deseaba construir un formalismo que se acerca lo más posible al razonamiento real. Así surgió un "calculus de deducción natural".)

Gentzen estaba motivado por el deseo de establecer la consistencia de la teoría de números. No pudo probar el resultado principal requerido para el resultado de consistencia, el teorema de eliminación de cortes, el Hauptsatz, directamente para la deducción natural. Por esta razón introdujo su sistema alternativo, el cálculo secuente, para el cual probó el Hauptsatz tanto para la lógica clásica como para la lógica intuicionista. En una serie de seminarios en 1961 y 1962, Prawitz dio un resumen completo de los cálculos de deducción natural y transportó gran parte del trabajo de Gentzen con cálculos secuenciales al marco de la deducción natural. Su monografía de 1965 Deducción natural: un estudio teórico de la demostración se convertiría en una obra de referencia sobre la deducción natural e incluía aplicaciones para la lógica modal y de segundo orden.

En la deducción natural, una proposición se deduce de un conjunto de premisas mediante la aplicación repetida de reglas de inferencia. El sistema presentado en este artículo es una variación menor de la formulación de Gentzen o de Prawitz, pero con una adhesión más cercana a la descripción de juicios lógicos y conectivos de Martin-Löf.

Juicios y proposiciones

Un juicio es algo cognoscible, es decir, objeto de conocimiento. Es evidente si uno de hecho lo sabe. Así "está lloviendo" es un juicio, que es evidente para el que sabe que en realidad está lloviendo; en este caso, uno puede encontrar fácilmente pruebas para el juicio mirando por la ventana o saliendo de la casa. Sin embargo, en la lógica matemática, la evidencia a menudo no es tan directamente observable, sino que se deduce de juicios evidentes más básicos. El proceso de deducción es lo que constituye una prueba; en otras palabras, un juicio es evidente si se tiene una prueba para ello.

Los juicios más importantes en lógica son de la forma "A es verdadero". La letra A representa cualquier expresión que represente una proposición; los juicios de verdad requieren un juicio más primitivo: "A es una proposición". Se han estudiado muchos otros juicios; por ejemplo, "A es falso" (ver lógica clásica), "A es verdadero en el tiempo t" (ver lógica temporal), "A es necesariamente cierto" o "A es posiblemente cierto" (ver lógica modal), "el programa M tiene tipo τ" (ver lenguajes de programación y teoría de tipos), "A se puede lograr con los recursos disponibles" (ver lógica lineal), y muchos otros. Para empezar, nos ocuparemos de los dos juicios más simples "A es una proposición" y "A es verdadero", abreviado como "A prop" y "A verdadero" respectivamente.

El juicio "A prop" define la estructura de pruebas válidas de A, que a su vez define la estructura de las proposiciones. Por esta razón, las reglas de inferencia para este juicio son a veces conocidas como Reglas de formación. Para ilustrar, si tenemos dos proposiciones A y B (es decir, los juicios "A prop" y "B prop" son evidentes), entonces formamos la proposición compuesto A y B, escrito simbólicamente como "A∧ ∧ B{displaystyle Awedge B}". Podemos escribir esto en forma de una regla de inferencia:

ApropBprop()A∧ ∧ B)prop∧ ∧ F{displaystyle {frac {hbox{ prop}qquad B{hbox{ prop}{(Awedge B){hbox{ prop}}}} ¿Qué?

donde se omiten los paréntesis para que la regla de inferencia sea más sucinta:

ApropBpropA∧ ∧ Bprop∧ ∧ F{displaystyle {frac {hbox{ prop}qquad B{ prop}{Awedge B{hbox{ prop}}}} ¿Qué?

Esta regla de inferencia es esquemática: A y B se pueden instanciar con cualquier expresión. La forma general de una regla de inferencia es:

J1J2⋯ ⋯ JnJNombre{displaystyle {frac {J_{1}qquad J_{2}qquad cdots qquad - ¿Qué?

donde cada Ji{displaystyle J_{i} es un juicio y la regla de la inferencia se llama "nombre". Los juicios por encima de la línea son conocidos como locales, y los que están debajo de la línea conclusiones. Otras proposiciones lógicas comunes son la disyunción (AAlternativa Alternativa B{displaystyle Avee B}), negación (¬ ¬ A{displaystyle neg A}), implicación (A.. B{displaystyle Asupset B}), y las constantes lógicas verdad (⊤ ⊤ {displaystyle top }) y falsedad (⊥ ⊥ {displaystyle bot }). Sus reglas de formación están abajo.

ApropBpropAAlternativa Alternativa BpropAlternativa Alternativa FApropBpropA.. Bprop.. F{displaystyle {frac {hbox{ prop}qquad B{hbox{ prop}{Avee B{hbox{ prop}}} vee _{F}qquad {frac {A{hbox{ prop}qquad B{hbox{ prop}{Asupset B{hbox{ prop}}}}} supset _{F}

⊤ ⊤ prop⊤ ⊤ F⊥ ⊥ prop⊥ ⊥ FAprop¬ ¬ Aprop¬ ¬ F{displaystyle {frac {hbox{}}{top {hbox{ prop}} ¿Qué? bot _{F}qquad {frac {hbox{hbox{}} {neg} {fn}} {fn}}}} {neg}}} {neg}}}}}}} {neg} ¿Qué?

Introducción y eliminación

Ahora discutimos el "A verdadero" juicio. Las reglas de inferencia que introducen un conectivo lógico en la conclusión se conocen como reglas de introducción. Introducir conjunciones, es decir, concluir "A y B verdaderos" para las proposiciones A y B, se requiere evidencia de "A verdadera" y "B verdadero". Como regla de inferencia:

Debe entenderse que en tales reglas los objetos son proposiciones. Es decir, la regla anterior es realmente una abreviatura de:

Esto también se puede escribir:

En esta forma, la primera premisa puede ser satisfecha por la ∧ ∧ F{displaystyle wedge _{F} regla de formación, dando los dos primeros locales de la forma anterior. En este artículo eliminaremos los juicios "prop" donde se entiendan. En el caso nulo, uno puede derivar la verdad de ningún local.

Si la verdad de una proposición se puede establecer de más de una manera, el conectivo correspondiente tiene múltiples reglas de introducción.

Tenga en cuenta que en el caso nulo, es decir,, por falsedad, no hay reglas de introducción. Así, uno nunca puede inferir falsedad de juicios más simples.

Las reglas duales de introducción son reglas de eliminación para describir cómo deconstruir la información sobre una proposición compuesta en información sobre sus constituyentes. Así, de "A ∧ B verdadero", podemos concluir "A verdadero" y "B verdadero":

Como ejemplo del uso de reglas de inferencia, considere la conmutatividad de la conjunción. Si A ∧ B es verdadero, entonces B ∧ A es verdadero; esta derivación se puede extraer componiendo reglas de inferencia de tal manera que las premisas de una inferencia inferior coincidan con la conclusión de la siguiente inferencia superior.

Las figuras de inferencia que hemos visto hasta ahora no son suficientes para enunciar las reglas de introducción de implicación o eliminación de disyunción; para estos, necesitamos una noción más general de derivación hipotética.

Derivaciones hipotéticas

Una operación omnipresente en la lógica matemática es razonar a partir de suposiciones. Por ejemplo, considere la siguiente derivación:

Esta derivación no establece la verdad de B como tal; más bien, establece el siguiente hecho:

Si Una ∧ (B ∧ C) es verdad entonces B es verdad.

En lógica, uno dice "asumiendo que A ∧ (B ∧ C) es verdadero, mostramos que B es verdadero"; en otras palabras, el juicio "B verdadero" depende del juicio asumido "A ∧ (B ∧ C) verdadero". Esta es una derivación hipotética, que escribimos de la siguiente manera:

La interpretación es: "B verdadero es derivable de A ∧ (B ∧ C) verdadero". Por supuesto, en este ejemplo específico conocemos la derivación de "B true" de "A ∧ (B ∧ C) verdadero", pero en general no podemos a priori conocer la derivación. La forma general de una derivación hipotética es:

Cada derivación hipotética tiene una colección de derivaciones antecedentes (la D_i) escritas en la línea superior y una sucesora sentencia (J) escrita en la línea inferior. Cada una de las premisas puede ser en sí misma una derivación hipotética. (Para simplificar, tratamos un juicio como una derivación sin premisa).

La noción de juicio hipotético se internaliza como conectivo de implicación. Las reglas de introducción y eliminación son las siguientes.

En la regla de introducción, el antecedente denominado u se descarga en la conclusión. Este es un mecanismo para delimitar el alcance de la hipótesis: su única razón de ser es establecer "B verdadero"; no se puede utilizar para ningún otro propósito y, en particular, no se puede utilizar debajo de la introducción. Como ejemplo, considere la derivación de "A ⊃ (B ⊃ (A ∧ B)) verdadero":

Esta derivación completa no tiene premisas insatisfechas; sin embargo, las subderivaciones son hipotéticas. Por ejemplo, la derivación de "B ⊃ (A ∧ B) verdadero" es hipotético con antecedente "A verdadero" (llamado u).

Con derivaciones hipotéticas, ahora podemos escribir la regla de eliminación para la disyunción:

En palabras, si A ∨ B es verdadero, y podemos derivar "C verdadero" ambos de "A verdadero" y de "B verdadero", entonces C es ciertamente verdadero. Tenga en cuenta que esta regla no se compromete con "A true" o "B verdadero". En el caso cero-ario, es decir por falsedad, obtenemos la siguiente regla de eliminación:

Esto se lee como: si la falsedad es verdadera, entonces cualquier proposición C es verdadera.

La negación es similar a la implicación.

La regla de introducción descarga tanto el nombre de la hipótesis u como el sucedente p, es decir, la proposición p no debe aparecer en la conclusión A. Dado que estas reglas son esquemáticas, la interpretación de la regla de introducción es: si de "A verdadero" podemos derivar para cada proposición p que "p verdadero", entonces A debe ser falso, es decir, "no A verdadero". Para la eliminación, si se demuestra que tanto A como no A son verdaderos, entonces hay una contradicción, en cuyo caso toda proposición C es verdadero. Debido a que las reglas para la implicación y la negación son tan similares, debería ser bastante fácil ver que no A y A ⊃ ⊥ son equivalentes, es decir, cada uno es derivable del otro.

Coherencia, integridad y formas normales

Se dice que una teoría es consistente si la falsedad no es demostrable (sin suposiciones) y es completa si cada teorema o su negación es demostrable usando las reglas de inferencia de la lógica. Estas son declaraciones sobre toda la lógica y generalmente están vinculadas a alguna noción de modelo. Sin embargo, existen nociones locales de consistencia y completitud que son controles puramente sintácticos de las reglas de inferencia y no requieren recurrir a modelos. El primero de ellos es la consistencia local, también conocida como reducibilidad local, que dice que cualquier derivación que contenga una introducción de un conectivo seguida inmediatamente por su eliminación puede convertirse en una derivación equivalente sin este desvío. Es una verificación de la fortaleza de las reglas de eliminación: no deben ser tan fuertes como para incluir conocimientos que no estén ya contenidos en sus premisas. Como ejemplo, considere las conjunciones.

AverdaderouBverdaderowA∧ ∧ Bverdadero∧ ∧ IAverdadero∧ ∧ E1⇒ ⇒ Averdaderou{displaystyle {begin{aligned}{cfrac {cHFFFF} {cH00FF} {cH00FFFF} {cH00FFFF} {cH00FFFFFF} {cH00FFFF} {cHFF} {cH00} {cH00} {cH00} {} {fnK} {fnK}} {fnK}} {f}}}} {fn}}} {fn}}}}}} {f}} {fnK}}}}}}}} {fn}}}}}}} {f} {f}} {f}}}} {f}}}}}} {f}}}}} {f}}}}}}}}}}} {f}}}}}} {f} {f}}}} {f}}}}} {f}}}}} {f} {f}}}}} {f}}}}} {f} {f} {f}}} {f}}}}}}}}}}}}}}}}}f}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} B {text{true}w}w}{Awedge B {text{true}}wedge {fnK} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} ## {E1}end{aligned}quad Rightarrow quad {cfrac {fnMicrosoft}}u}

Dualmente, la completitud local dice que las reglas de eliminación son lo suficientemente fuertes como para descomponer un conectivo en las formas adecuadas para su regla de introducción. Nuevamente para conjunciones:

A∧ ∧ Bverdaderou⇒ ⇒ A∧ ∧ BverdaderouAverdadero∧ ∧ E1A∧ ∧ BverdaderouBverdadero∧ ∧ E2A∧ ∧ Bverdadero∧ ∧ I{displaystyle {cfrac {fnMicrosoft} {fnMicrosoft} {fnMicrosoft}} {fnK}}} {fn}}} {fnMicrosoft}}} {f}}}} {fn}}}} {fn}}}}}f}} {f}}}}}f}}}} Rightarrow quad {begin{aligned}{cfrac {cHFFFF} {cH00FF} {cH00FFFF} {cH00FFFF} {cH00FFFFFF} {cH00FFFF} {cHFF} {cH00} {cH00} {cH00} {fnMicrosoft} {fnMicrosoft}}} {fnMicrosoft}} {fnMicrosoft}} {f}} {fn}}} {f}}}} {f}}}} {fnK}}}}} {f}} {f}}}} {f}}}}}}}}}}}}} {f}}}}}}}}}}}}}} {f}}}}}}}}}}}}}}} {f}}}}}}}}}}}}}}}}}}}} {f}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} {f}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} { {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} ¿Qué? - ¿Qué? B {text{true}}wedge ¿Qué?

Estas nociones corresponden exactamente a la reducción β (reducción beta) y la conversión η (conversión eta) en el cálculo lambda, utilizando el isomorfismo de Curry-Howard. Por completitud local, vemos que cada derivación puede convertirse en una derivación equivalente donde se introduce el conectivo principal. De hecho, si toda la derivación obedece a este orden de eliminaciones seguidas de introducciones, entonces se dice que es normal. En una derivación normal todas las eliminaciones ocurren por encima de las introducciones. En la mayoría de las lógicas, cada derivación tiene una derivación normal equivalente, llamada forma normal. Por lo general, es difícil probar la existencia de formas normales usando solo la deducción natural, aunque tales explicaciones existen en la literatura, sobre todo por Dag Prawitz en 1961. Es mucho más fácil demostrar esto indirectamente por medio de una presentación de cálculo secuencial sin cortes..

Extensiones de primer orden y de orden superior

Resumen del sistema de primera orden

La lógica de la sección anterior es un ejemplo de una lógica de clasificación única, es decir,, una lógica con un solo tipo de objeto: proposiciones. Se han propuesto muchas extensiones de este marco simple; en esta sección lo ampliaremos con un segundo tipo de individuos o términos. Más precisamente, agregaremos un nuevo tipo de juicio, "t es un término" (o "t término") donde t es esquemático. Fijaremos un conjunto contable V de variables, otro conjunto contable F de símbolos de función, y construiremos términos con las siguientes reglas de formación:

v▪ ▪ VvmandatoVarF{displaystyle {frac {fnfnfnfnfnfnfn\fnccccccccccccccc\c\\ccc\ccc\c\cc\\\\\\\\\c\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\ - ¿Qué? - Sí.

y

f▪ ▪ Ft1mandatot2mandato⋯ ⋯ tnmandatof()t1,t2,⋯ ⋯ ,tn)mandatoappF{displaystyle {frac {fnfnfnMicrosoftfnfn\fnfncccccc\c\\\ccc\c\\c\\\\\\cc\\\c\\\\\\c\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\ Fqquad t_{1}{qquad t_{2}{hbox{ term}qquad cdots qquad t_{n}{hbox{ term}}{f(t_{1},t_{2},cdotst_{n}){hbox{ term}}}{hbox{hbox{}}}}}}} {}}}}{h}} {hqqqqqqqqqqqqqqqqqqqqqqqqqquad}}}} {} {} {}}}}} {}} {}} {} {}}}}} {}} {}}}}}} {c_} {} {c}}} {c} {hqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqquad}}} {} {} {} {} {}}}}} {} { - ¿Qué?

Para las proposiciones, consideramos un tercer conjunto contable P de predicados, y definimos predicados atómicos sobre términos con la siguiente regla de formación:

φ φ ▪ ▪ Pt1mandatot2mandato⋯ ⋯ tnmandatoφ φ ()t1,t2,⋯ ⋯ ,tn)proppredF{displaystyle {frac {phi in Pqquad t_{1}{hbox{ term}qquad t_{2}{hbox{ term}}qquad cdots qquad t_{n}{hbox{ term}}{fphidcdots (t_{1},t_{2},cdotst_{n}{hbox{}} {hbox{} {fnK}

Las dos primeras reglas de formación brindan una definición de un término que es efectivamente la misma que se define en el álgebra de términos y la teoría de modelos, aunque el enfoque de esos campos de estudio es bastante diferente de la deducción natural. La tercera regla de formación define efectivamente una fórmula atómica, como en la lógica de primer orden, y nuevamente en la teoría de modelos.

A estas se añaden un par de reglas de formación, definiendo la notación para proposiciones cuantificadas; uno para cuantificación universal (∀) y existencial (∃):

x▪ ▪ VApropО О x.ApropО О Fx▪ ▪ VAprop∃ ∃ x.Aprop∃ ∃ F{displaystyle {frac {xin Vqquad A{hbox{ prop} {forall x.A{hbox{ prop};forall {fnK}} {fnMicroc {xin Vqquad A{hbox{ prop}}}{exists x.A{hbox{ prop}}};exists ¿Qué?

El cuantificador universal tiene las reglas de introducción y eliminación:

amandatou⋮ ⋮ [a/x]AverdaderoО О x.AverdaderoО О Iu,aО О x.Averdaderotmandato[t/x]AverdaderoО О E{displaystyle {cfrac {begin{array}{c}{cfrac {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans {fnMicrosoft Sans Serif}}\fnMicrosoft Sans {fnMicrosoft Sans Serif}}}}}}}}fnMinMientras tantos#fnMientras tanto, uh} {fnMinMientras tantos#fnMientras tanto, uh} {fnMientras tantos {fnMinMientras más #fnMinMientras más ## {fnMientras tantosoyasentras tantosoyasentras más, uh}fnMientras me siento que yo no me siento que no me siento que me siento que no me siento que me siento que me siento que me gustassssoyasentras que me siento que me siento que me ¿Por qué? ¿Qué?

El cuantificador existencial tiene las reglas de introducción y eliminación:

[t/x]Averdadero∃ ∃ x.Averdadero∃ ∃ Iamandatou[a/x]Averdaderov⏟ ⏟ ⋮ ⋮ ∃ ∃ x.AverdaderoCverdaderoCverdadero∃ ∃ Ea,u,v{displaystyle {frac {fnMicrosoft Sans Serif}} {exists x.A{hbox{ true}}};exists ################################################################################################################################################################################################################################################################ {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {} {} {fnMicrosoft Sans Serif} {} {} {fnMicrosoft Sans Serif} {} {} {}} {}} {f}} {fnMicrox}} {f} {f}}} {f}}}} {f}f}} {f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f}f} {f}f}f}f}f}f}f}f}fnKfnfnfnfnfnKf}f}f}f}fn

En estas reglas, la notación [t/x] A representa la sustitución de t por cada instancia (visible) de x en A, evitando la captura. Como antes, los superíndices en el nombre representan los componentes que se descargan: el término a no puede aparecer en la conclusión de ∀I (dichos términos se conocen como eigenvariables o parámetros), y las hipótesis denominadas u y v en ∃E se localizan en la segunda premisa en una derivación hipotética. Aunque la lógica proposicional de las secciones anteriores era decidible, agregar los cuantificadores hace que la lógica sea indecidible.

Hasta ahora, las extensiones cuantificadas son de primer orden: distinguen las proposiciones de los tipos de objetos cuantificados. La lógica de orden superior adopta un enfoque diferente y tiene un solo tipo de proposiciones. Los cuantificadores tienen como dominio de cuantificación el mismo tipo de proposiciones, como se refleja en las reglas de formación:

ppropu⋮ ⋮ ApropО О p.ApropО О Fuppropu⋮ ⋮ Aprop∃ ∃ p.Aprop∃ ∃ Fu{displaystyle {cfrac {begin{Matrix}{cfrac {\fnMicrosoft Sans Serif}\fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {\fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans}}\fnMicrosoft Sans Ser}}\fnMicrosoft Sans {fnMicrosoft Sans Ser}}}}\fnMicrosoft Sans Ser}}}}\fnMicros}\fnMicros}\fnMicrosoft}}}}\\\\\\fnMicrob}}\\\\fnMicrob}fnMicrob}fnMicrob}\\fnMicrob}fnMicrob}fnMicrob}\\fnMicrob}\\\fnMicrob}fnMicrob}fnMicrob}\fnMicrosoftfnMicros}\fnMicrob}fnMicrob}\fnMicrob}fnMicrob}\\\\ {f}qquad qquad {cfrac {begin{matrix}{cfrac {\fnMicrosoft Sans Serif}\fnMicrosoft Sans Serif}\fnMicrosoft Sans Serif}}\\\\\\\fnMicrosoft Sans Serif}\\\\\fnMicros}\\\\fnMicrox}}\\\\\\fnMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinMinK}}}}}}}}}}}}}}}\\\\\\\ ¿Qué?

Una discusión de las formas de introducción y eliminación para la lógica de orden superior está más allá del alcance de este artículo. Es posible estar entre lógicas de primer orden y de orden superior. Por ejemplo, la lógica de segundo orden tiene dos tipos de proposiciones, un tipo que cuantifica sobre términos y el segundo tipo que cuantifica sobre proposiciones del primer tipo.

Distintas presentaciones de la deducción natural

Presentaciones en forma de árbol

Las anotaciones de descarga de Gentzen utilizadas para internalizar juicios hipotéticos se pueden evitar representando las pruebas como un árbol de secuencias Γ ⊢A en lugar de un árbol de A verdadero juicios

Presentaciones secuenciales

Las representaciones de la deducción natural de Jaśkowski dieron lugar a diferentes notaciones, como el cálculo al estilo de Fitch (o los diagramas de Fitch) o el cálculo de Suppes. método, del cual Lemmon dio una variante llamada sistema L. Dichos sistemas de presentación, que se describen con mayor precisión como tabulares, incluyen los siguientes.

• 1940: En un libro de texto, Quine indicó dependencias anteriores por números de línea entre corchetes, anticipando la notación de números de línea 1957 de Suppes.
• 1950: En un libro de texto, Quine (1982, págs. 241 a 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 equivale a las barras verticales de Kleene. (No está totalmente claro si la notación asterisco de Quine apareció en la edición original de 1950 o fue agregada en una edición posterior.)
• 1957: Una introducción al teorema lógico práctico probando en un libro de texto de Suppes (1999, págs. 25 a 150). Esto indicó dependencias (es decir, proposiciones anteriores) por 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 anteriores 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, págs. 50 a 58, 128 a 130) demostró brevemente dos tipos de pruebas lógicas prácticas, un sistema que utiliza citas explícitas de propuestas anteriores a la izquierda de cada línea, el otro sistema que utiliza barras verticales de la izquierda para indicar dependencias.

Pruebas y teoría de tipos

La presentación de la deducción natural hasta ahora se ha concentrado en la naturaleza de las proposiciones sin dar una definición formal de una prueba. Para formalizar la noción de prueba, alteramos ligeramente la presentación de las derivaciones hipotéticas. Etiquetamos los antecedentes con variables de prueba (de algún conjunto contable V de variables), y decoramos el sucedente con la prueba real. Los antecedentes o hipótesis se separan del sucedente mediante un torniquete (⊢). Esta modificación a veces recibe el nombre de hipótesis localizadas. El siguiente diagrama resume el cambio.

- Sí.1 - Sí.2- Sí.nJ1 J2 Jn⋮
J

u1J1, u2J2,... unJn ⊢ J

El conjunto de hipótesis se escribirá como Γ cuando su composición exacta no sea relevante. Para hacer explícitas las pruebas, pasamos del juicio sin pruebas "A true" a un juicio: "π es una prueba de (A verdadero)", que se escribe simbólicamente como "π: A verdadero& #34;. Siguiendo el enfoque estándar, las pruebas se especifican con sus propias reglas de formación para el juicio "π prueba". La prueba más simple posible es el uso de una hipótesis etiquetada; en este caso la evidencia es la propia etiqueta.

u otro
- Sí.
u prueba

- No. hyp
U: Un verdadero ⊢ u: Un verdadero

Para abreviar, dejaremos de lado la etiqueta crítica verdadero en el resto de este artículo, es decir, escriba "Γ ⊢ π: A ". Reexaminemos algunos de los conectores con pruebas explícitas. Para la conjunción, observamos la regla de introducción ∧I para descubrir la forma de las pruebas de conjunción: deben ser un par de pruebas de los dos conjuntos. De este modo:

π1 prueba π2 prueba
- Sí.
(π1, π2Prueba

Γ π1: Una luminaria ⊢ π2B
- ¡No!
}1, π2) A ∧ B

Las reglas de eliminación ∧E₁ y ∧E₂ seleccionan la conjunción izquierda o derecha; por tanto, las demostraciones son un par de proyecciones: la primera (fst) y la segunda (snd).

Prueba π
- No. f-F
f Prueba π

Γ π: A ∧ B
- ¡Fuera!1} f π: A

Prueba π
- No. Snd-F
Snd Prueba π

Γ π: A ∧ B
- ¡Fuera!2} Snd π: B

Por implicación, la forma de introducción localiza o vincula la hipótesis, escrita con λ; esto corresponde a la etiqueta descargada. En la regla, "Γ, u:A" representa el conjunto de hipótesis Γ, junto con la hipótesis adicional u.

Prueba π
- No. λ-F
λu. Prueba π

Dimensiones, u:A ⊢ π: B
- No.
Γ λu. π: A

π1 prueba π2 prueba
- No.
π1 π2 prueba

Γ π1: A нел B не н не π π2A
- No.
Γ π1 π2B

Con las pruebas disponibles explícitamente, uno puede manipular y razonar sobre las pruebas. La operación clave en las pruebas es la sustitución de una prueba por una suposición utilizada en otra prueba. Esto se conoce comúnmente como teorema de sustitución, y puede probarse por inducción sobre la profundidad (o estructura) del segundo juicio.

Substitution theorem

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

Hasta ahora la sentencia "Γ ⊢ π: A" ha tenido una interpretación puramente lógica. En la teoría de tipos, la vista lógica se cambia por una vista más computacional de los objetos. Las proposiciones en la interpretación lógica ahora se ven como tipos y las pruebas como programas en el cálculo lambda. Así, la interpretación de "π: A" es "el programa π tiene tipo A". A los conectores lógicos también se les da una lectura diferente: la conjunción se ve como el producto (×), la implicación como la función flecha (→), etc. Sin embargo, las diferencias son solo cosméticas. La teoría de tipos tiene una presentación de deducción 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 tipo simple de las secciones anteriores.

La diferencia entre la lógica y la teoría de tipos es principalmente un cambio de enfoque de los tipos (proposiciones) a los programas (pruebas). La teoría de tipos está principalmente interesada en la convertibilidad o reducibilidad de los programas. Para cada tipo, hay programas canónicos de ese tipo que son irreductibles; estos se conocen como formas canónicas o valores. Si cada programa se puede reducir a una forma canónica, entonces se dice que la teoría de tipos está normalizando (o débilmente normalizando). 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, que es una gran desviación del mundo lógico. (Recuerde que casi todas las derivaciones lógicas tienen 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; tales programas de bucle generalmente se pueden dar de cualquier tipo. En particular, el programa de bucle tiene tipo ⊥, aunque no hay prueba lógica de "⊥ verdadero". Por eso, las proposiciones como tipos; El paradigma de las pruebas como programas solo funciona en una dirección, si es que lo hace: interpretar una teoría de tipos como una lógica generalmente da una lógica inconsistente.

Ejemplo: teoría del tipo dependiente

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

Dimensiones ⊢ Un tipo de carga, x:A ⊢ Tipo B
- No. LOG-F
Dimensiones:A. Tipo B

Dimensiones ⊢ Un tipo de carga, x:A ⊢ Tipo B
- No. Governing-F
Dimensiones:A. Tipo B

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

Dimensiones, x:A ⊢ π: B
- No. LOGI
Γ λx. π: A. B

Γ π1: ■x:A. B2A
- No. LOGE
Γ π1 π2[π]2B

Γ π1: Una luminaria, x:A ⊢ π2B
- No. CEPI
}1, π2) A. B

Γ π: A. B
- No. CEPE1} f π: A

Γ π: A. B
- No. CEPE2} Snd π: [f π/x] B

La teoría de tipos dependientes en general es muy poderosa: es capaz de expresar casi cualquier propiedad concebible de los programas directamente en los tipos del programa. Esta generalidad tiene un alto precio: la verificación de tipos es indecidible (teoría de tipos extensional) o el razonamiento extensional es más difícil (teoría de tipos intencional). Por esta razón, 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, números enteros, cadenas o programas lineales.

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

La intersección de la lógica y la teoría de tipos es un área de investigación amplia y activa. Las nuevas lógicas suelen formalizarse en un marco teórico de tipo general, conocido como marco lógico. Los marcos lógicos modernos populares, como el cálculo de construcciones y LF, se basan en la teoría de tipos dependientes de orden superior, con varias compensaciones en términos de capacidad de decisión y poder expresivo. Estos marcos lógicos siempre se especifican como sistemas de deducción natural, lo que es un testimonio de la versatilidad del enfoque de deducción natural.

Lógica clásica y modal

Para simplificar, las lógicas presentadas hasta ahora han sido intuicionistas. La lógica clásica extiende la lógica intuicionista con un axioma o principio adicional de tercero excluido:

Para cualquier proposición p, la proposición p ∨ ¬p es verdad.

Obviamente, esta declaración no es ni una introducción ni una eliminación; de hecho, implica dos conectivos distintos. El tratamiento original de Gentzen del tercero excluido prescribía una de las siguientes tres formulaciones (equivalentes), que ya estaban presentes en formas análogas en los sistemas de Hilbert y Heyting:

- No.1Una latitud ¬

¬ Un verdadero
- Sí.2Un verdadero

- No. u¬ Un verdadero
⋮
p verdadero
- Sí.3u, pUn verdadero

(XM₃ es simplemente XM₂ expresado en términos de E.) Este tratamiento del tercero excluido, además de ser objetable desde el punto de vista de un purista, introduce complicaciones adicionales en la definición de formas normales.

Parigot propuso por primera vez en 1992 un tratamiento comparativamente más satisfactorio de la deducción natural clásica en términos de reglas de introducción y eliminación en forma de un cálculo lambda clásico llamado λμ. La idea clave de su enfoque fue reemplazar un juicio centrado en la verdad A verdadero con una noción más clásica, que recuerda al cálculo secuencial: en forma localizada, en lugar de Γ ⊢ A, usó Γ ⊢ Δ, con Δ una colección de proposiciones similares a Γ. Γ se trató como una conjunción y Δ como una disyunción. Esta estructura se extrae esencialmente directamente de los cálculos secuenciales clásicos, pero la innovación en λμ fue dar un significado computacional a las pruebas de deducción natural clásicas en términos de un mecanismo callcc o throw/catch visto en LISP y sus descendientes. (Ver también: control de primera clase).

Otra extensión importante fue para modal y otras lógicas que necesitan más que solo el juicio básico de verdad. Estos fueron descritos por primera vez, para las lógicas modales aléticas S4 y S5, en un estilo de deducción natural por Prawitz en 1965, y desde entonces han acumulado una gran cantidad de trabajo relacionado. Para dar un ejemplo simple, la lógica modal S4 requiere un nuevo juicio, "A válido", que es categórico con respecto a la verdad:

Si "A true" bajo ninguna suposición de la forma "B true", entonces "A valid".

Este juicio categórico se internaliza como un conectivo unario ◻A (léase "necesariamente A") con las siguientes reglas de introducción y eliminación:

Una válida
- Entendido.
⋅ A true

⋅ A true
- Entendido.
Un verdadero

Tenga en cuenta que la premisa "A valid" no tiene reglas definitorias; en su lugar, se utiliza la definición categórica de validez. Este modo se vuelve más claro en la forma localizada cuando las hipótesis son explícitas. Escribimos "Ω;Γ ⊢ A verdadero" donde Γ contiene las hipótesis verdaderas como antes, y Ω contiene hipótesis válidas. A la derecha hay un único juicio "A true"; la validez no es necesaria aquí ya que "Ω ⊢ A valid" es por definición lo mismo que "Ω;⋅ ⊢ A verdadero". Las formas de introducción y eliminación son entonces:

Ω;⋅ π π: Un verdadero
- No.
Ω;⋅ ⊢ caja π: latitud Un verdadero

Ω; ancho ⊢ π: Ø Un verdadero
- No.
Ω; Unbox π: Un verdadero

Las hipótesis modales tienen su propia versión de la regla de hipótesis y el teorema de sustitución.

- No. valid-hyp
Ω, u: (A valid); Ω ⊢ u: A true

Modal substitution theorem

Si Ω;⋅ π π₁: Un verdadero y Ω, u#Una válida)₂: C true, entonces Ω; ancho ⊢ [π₁/uπ₂: C true.

Este marco de separación de juicios en distintas colecciones de hipótesis, también conocido como contextos multizona o poliádico, es muy poderoso y extensible; se ha aplicado para muchas lógicas modales diferentes, y también para lógicas lineales y otras lógicas subestructurales, por dar algunos ejemplos. Sin embargo, relativamente pocos sistemas de lógica modal pueden formalizarse directamente en deducción natural. Para dar caracterizaciones teóricas de prueba de estos sistemas, extensiones tales como 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 técnicas más flexibles de cuadros 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 (1993) presenta una técnica influyente para convertir las condiciones de marco de la lógica modal 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 prueba, como las hipersecuencias de Avron y Pottinger y la lógica de visualización de Belnap a lógicas modales como S5 y B.

Comparación con otros enfoques fundamentales

Cálculo secuencial

El cálculo secuente es la principal alternativa a la deducción natural como fundamento de la lógica matemática. En la deducción natural, el flujo de información es bidireccional: las reglas de eliminación hacen fluir la información hacia abajo por deconstrucción, y las reglas de introducción hacen fluir la información hacia arriba por ensamblaje. Por lo tanto, una prueba de deducción natural no tiene una lectura puramente de abajo hacia arriba o de arriba hacia abajo, lo que la hace inadecuada para la automatización en la búsqueda de pruebas. Para abordar este hecho, Gentzen en 1935 propuso su cálculo secuencial, aunque inicialmente lo pensó como un dispositivo técnico para aclarar la consistencia de la lógica de predicados. Kleene, en su libro seminal de 1952 Introducción a las metamatemáticas, dio la primera formulación del cálculo secuente en el estilo moderno.

En el cálculo secuencial, todas las reglas de inferencia tienen una lectura puramente ascendente. Las reglas de inferencia se pueden aplicar a elementos en ambos lados del torniquete. (Para diferenciar de la deducción natural, este artículo utiliza una flecha doble ⇒ en lugar de la tachuela derecha ⊢ para los secuentes). Las reglas de introducción de la deducción natural se consideran reglas correctas en el cálculo de secuentes, y son muy similar. Las reglas de eliminación, por otro lado, se convierten en reglas de izquierda en el cálculo secuente. Para dar un ejemplo, considere la disyunción; las reglas correctas son familiares:

⇒ A
- Entendido.1⇒ ⇒ A ∨

⇒ B
- Entendido.2⇒ ⇒ A ∨

A la izquierda:

Dimensiones, u:A ⇒ C lumina, v:B ⇒ C
- No.
⇒ C

Recuerde la regla ∨E de deducción natural en forma localizada:

Dimensiones ∨ A Alternativa B, u:A ⊢ C, v:B ⊢ C
- No, no, no, no. AlternativaE
Γ C

La proposición A ∨ B, que es el sucedente de una premisa en ∨E, se convierte en una hipótesis de la conclusión en la regla de la izquierda ∨L. Por lo tanto, las reglas de la izquierda pueden verse como una especie de regla de eliminación invertida. Esta observación se puede ilustrar de la siguiente manera:

 - Sí.
Silencio
TENIENDO ELIM.
Silencio
↓
- No.
↑
Silencio
Silencio intro. reglas
Silencio
conclusión

 - No.
↑
Silencio
reglas izquierdas, reglas derechas
Silencio
conclusión

En el cálculo de secuentes, las reglas izquierda y derecha se ejecutan al unísono hasta llegar al secuente inicial, que corresponde al punto de encuentro de las reglas de eliminación e introducción en la deducción natural. Estas reglas iniciales son superficialmente similares a la regla de hipótesis de la deducción natural, pero en el cálculo secuencial describen una transposición o un apretón de manos de una proposición izquierda y otra derecha:

- Sí.
, u:A ⇒ A

La correspondencia entre el cálculo secuente y la deducción natural es un par de teoremas de solidez y completitud, ambos demostrables por medio de un argumento inductivo.

Sonido del ⇒ wrt. ⊢

Si ⇒ A, entonces } A.

Completeness of ⇒ wrt. ⊢

Si } A, entonces ⇒ A.

De acuerdo con estos teoremas, queda claro que el cálculo de secuencias no cambia la noción de verdad, porque la misma colección de proposiciones sigue siendo verdadera. Por lo tanto, se pueden usar los mismos objetos de prueba que antes en las derivaciones de cálculo secuencial. Como ejemplo, considere las conjunciones. La regla correcta es virtualmente idéntica a la regla de introducción.

⇒ π1: Un ⇒ π2B
- No, no, no, no.
⇒ (π)1, π2) A ∧ B

Γ π1: Una luminaria ⊢ π2B
- ¡No!
}1, π2) A ∧ B

La regla de la izquierda, sin embargo, realiza algunas sustituciones adicionales que no se realizan en las reglas de eliminación correspondientes.

, u:A ⇒ π: C
- No. ∧L1(A ∧ B) ⇒f v/u] π: C

Γ π: A ∧ B
- ¡Fuera!1} f π: A

Dimensiones, u:B ⇒ π: C
- No. ∧L2(A ∧ B) ⇒Snd v/u] π: C

Γ π: A ∧ B
- ¡Fuera!2} Snd π: B

Los tipos de pruebas generadas en el cálculo secuencial son, por lo tanto, bastante diferentes de las de la deducción natural. El cálculo de secuencias produce pruebas en lo que se conoce como la forma β-normal η-larga, que corresponde a una representación canónica de la forma normal de la prueba de deducción natural. Si uno intenta describir estas pruebas usando la deducción natural misma, obtiene lo que se llama el cálculo de intercalación (descrito por primera vez por John Byrnes), que puede usarse para definir formalmente la noción de un normal formulario para la deducción natural.

El teorema de sustitución de la deducción natural toma la forma de una regla estructural o teorema estructural conocido como corte en el cálculo secuente.

Corte (sustitución)

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

En la mayoría de las lógicas de buen comportamiento, el corte es innecesario como regla de inferencia, aunque sigue siendo demostrable como metateorema; la superfluidad de la regla de corte suele presentarse 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 probar ciertas propiedades directamente en la deducción natural debido a un número ilimitado de casos. Por ejemplo, considere mostrar que una proposición dada no es comprobable en 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 secuencias es completo con respecto a la deducción natural, por lo que basta con mostrar esta indemostrabilidad en el cálculo de secuencias. Ahora, si el corte no está disponible como regla de inferencia, entonces todas las reglas de secuente introducen un conectivo a la derecha o a la izquierda, por lo que la profundidad de una derivación de secuente está completamente limitada por los conectivos en la conclusión final. Por lo tanto, mostrar la indemostrabilidad es mucho más fácil, porque solo hay un número finito de casos a considerar, y cada caso se compone completamente de subproposiciones de la conclusión. Un ejemplo simple de esto es el teorema de consistencia global: "⋅ ⊢ ⊥ verdadero" no es demostrable. En la versión de cálculo secuente, esto es manifiestamente cierto porque no hay ninguna regla que pueda tener "⋅ ⇒ ⊥" ¡como conclusión! Los teóricos de la prueba a menudo prefieren trabajar en formulaciones de cálculo secuencial sin cortes debido a tales propiedades.