En lógica y teoría de la prueba , la deducción natural es una especie de cálculo de prueba en el que el razonamiento lógico se expresa mediante reglas de inferencia estrechamente relacionadas con la forma "natural" de razonamiento. Esto contrasta con los sistemas de estilo Hilbert , que en cambio utilizan axiomas tanto como sea posible para expresar las leyes lógicas del razonamiento deductivo .
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, Sistema de Hilbert ). Estas axiomatizaciones fueron las más famosas utilizadas por Russell y Whitehead en su tratado matemático Principia Mathematica . Impulsado por una serie de seminarios en Polonia en 1926 impartidos por Łukasiewicz que defendían 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 utilizando una notación esquemática y luego actualizando su propuesta en una secuencia. de artículos en 1934 y 1935. [1] Sus propuestas llevaron a diferentes notaciones como el cálculo estilo Fitch (o diagramas de Fitch) o el método de Suppes 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 1933, en una disertación presentada en la facultad de ciencias matemáticas de la Universidad de Göttingen . [2] El término deducción natural (o más bien, su equivalente alemán natürliches Schließen ) fue acuñado en ese artículo:
Gentzen estaba motivado por el deseo de establecer la coherencia de la teoría de números . No pudo demostrar el resultado principal requerido para el resultado de consistencia, el teorema de eliminación por corte (el Hauptsatz), directamente para la deducción natural. Por esta razón introdujo su sistema alternativo, el cálculo secuente , para el cual demostró el Hauptsatz tanto para la lógica clásica como para la intuicionista . En una serie de seminarios en 1961 y 1962, Prawitz ofreció un resumen completo de los cálculos de deducción natural y trasladó 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 prueba [4] 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 a partir de un conjunto de premisas aplicando reglas de inferencia repetidamente. El sistema presentado en este artículo es una variación menor de la formulación de Gentzen o Prawitz, pero con una mayor adherencia a la descripción de Martin-Löf de juicios lógicos y conectivos. [5]
Un juicio es algo cognoscible, es decir, un objeto de conocimiento. Es evidente si uno realmente lo sabe. [6] Así, " está lloviendo " es un juicio, que es evidente para quien sabe que en realidad está lloviendo; en este caso uno puede encontrar fácilmente pruebas para la sentencia mirando por la ventana o saliendo de la casa. Sin embargo, en 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 de ello.
Los juicios más importantes en lógica son los de la forma " A es verdadero ". La letra A representa cualquier expresión que represente una proposición ; los juicios de verdad requieren pues un juicio más primitivo: " A es una proposición ". Se han estudiado muchas otras sentencias; por ejemplo, " A es falso " (ver lógica clásica ), " A es verdadero en el momento t " (ver lógica temporal ), " A es necesariamente verdadero " o " A es posiblemente verdadero " (ver lógica modal ), " el programa M tiene el tipo τ " (ver lenguajes de programación y teoría de tipos ), " A se puede lograr a partir de 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 verdadera ", abreviados como " A prop" y " A true", respectivamente.
El juicio " A prop" define la estructura de las pruebas válidas de A , que a su vez define la estructura de las proposiciones. Por este motivo, las reglas de inferencia para este juicio se conocen en ocasiones 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 compuesta A y B , escrita simbólicamente como " ". Podemos escribir esto en forma de regla de inferencia:
donde se omiten los paréntesis para que la regla de inferencia sea más concisa:
Esta regla de inferencia es esquemática : A y B pueden instanciarse con cualquier expresión. La forma general de una regla de inferencia es:
donde cada uno es un juicio y la regla de inferencia se denomina "nombre". Los juicios encima de la línea se conocen como premisas , y los que están debajo de la línea son conclusiones . Otras proposiciones lógicas comunes son la disyunción ( ), la negación ( ), la implicación ( ) y las constantes lógicas verdad ( ) y falsedad ( ). Sus reglas de formación se encuentran a continuación.
Ahora discutimos el juicio " Un verdadero". Las reglas de inferencia que introducen un conectivo lógico en la conclusión se conocen como reglas de introducción . Para introducir conjunciones, es decir , para concluir que " A y B son verdaderos" para las proposiciones A y B , se requiere evidencia de " A verdadero" y " B verdadero". Como regla de inferencia:
Debe entenderse que en tales reglas los objetos son proposiciones. Es decir, la regla anterior es en realidad una abreviatura de:
Esto también se puede escribir:
De esta forma, la primera premisa puede satisfacerse mediante la regla de formación, dando las dos primeras premisas de la forma anterior. En este artículo omitiremos los juicios de "apoyo" cuando se entiendan. En el caso nulo, no se puede derivar la verdad a partir de ninguna premisa.
Si la verdad de una proposición puede establecerse 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 , para la falsedad, no existen reglas de introducción. Por tanto, nunca se puede inferir falsedad a partir de juicios más simples.
Las reglas duales de introducción son reglas de eliminación para describir cómo deconstruir 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 realizar 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 cifras de inferencia que hemos visto hasta ahora no son suficientes para establecer las reglas de introducción de implicaciones o eliminación de disyunciones ; para estos, necesitamos una noción más general de derivación hipotética .
Una operación omnipresente en la lógica matemática es el razonamiento 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:
En lógica, se dice " asumiendo que A ∧ (B ∧ C) es verdadero, demostramos 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 verdadero" de " A ∧ (B ∧ C) verdadero", pero en general es posible que no conozcamos la derivación a priori . 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 ) escrita en la línea superior y un juicio sucesor ( J ) escrito 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 premisas).
La noción de juicio hipotético se internaliza como el 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. Se trata de un mecanismo para delimitar el alcance de la hipótesis: su única razón de existencia 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ética con el 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" tanto de " A verdadero" como de " B verdadero", entonces C es efectivamente verdadero. Tenga en cuenta que esta regla no se compromete ni a " A verdadero" ni a " B verdadero". En el caso ceroario, es decir , para la 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 verdaderas, entonces hay una contradicción, en cuyo caso toda proposición C es verdadera. Debido a que las reglas para la implicación y la negación son tan similares, debería ser bastante fácil ver que A y A ⊃ ⊥ no son equivalentes, es decir, cada uno es derivable del otro.
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 utilizando las reglas de inferencia de la lógica. Estas son declaraciones sobre toda la lógica y, por lo general, están vinculadas a alguna noción de modelo . Sin embargo, existen nociones locales de coherencia e integridad que son comprobaciones puramente sintácticas de las reglas de inferencia y no requieren apelaciones 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 de su eliminación puede convertirse en una derivación equivalente sin este desvío. Es un control de la solidez de las reglas de eliminación: no deben ser tan estrictas como para incluir conocimientos que no estén ya contenidos en sus premisas. Como ejemplo, consideremos las conjunciones.
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. De nuevo para conjunciones:
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 se puede convertir en una derivación equivalente donde se introduce el conectivo principal. De hecho, si toda la derivación obedece a este ordenamiento de eliminaciones seguidas de introducciones, entonces se dice que es normal . En una derivación normal, todas las eliminaciones ocurren antes de las introducciones. En la mayoría de las lógicas, cada derivación tiene una derivación normal equivalente, llamada forma normal . La existencia de formas normales es generalmente difícil de probar utilizando únicamente la deducción natural, aunque tales explicaciones existen en la literatura, más notablemente por Dag Prawitz en 1961. [7] Es mucho más fácil demostrar esto indirectamente por medio de una prueba sin cortes. presentación de cálculo posterior .
La lógica de la sección anterior es un ejemplo de lógica de orden único , es decir , una lógica con un solo tipo de objeto: proposiciones. Se han propuesto muchas extensiones de este marco simple; en este apartado 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 funciones y construiremos términos con las siguientes reglas de formación:
y
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:
Las dos primeras reglas de formación proporcionan una definición de un término que es efectivamente la misma que la definida en álgebra de términos y 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 éstas se añaden un par de reglas de formación, que definen la notación para proposiciones cuantificadas ; uno para cuantificación universal (∀) y existencial (∃):
El cuantificador universal tiene las reglas de introducción y eliminación:
El cuantificador existencial tiene las reglas de introducción y eliminación:
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. [8] Como antes, los superíndices del nombre representan los componentes que se descargan: el término a no puede aparecer en la conclusión de ∀I (tales términos se conocen como variables propias 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 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 sobre 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:
Una discusión de las formas de introducción y eliminación de 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 lógicas de orden superior. Por ejemplo, la lógica de segundo orden tiene dos tipos de proposiciones: un tipo que cuantifica términos y el segundo que cuantifica proposiciones del primer tipo.
Las anotaciones de descarga de Gentzen utilizadas para internalizar juicios hipotéticos se pueden evitar representando las pruebas como un árbol de consecuentes Γ ⊢A en lugar de un árbol de A juicios verdaderos .
Las representaciones de Jaśkowski de la deducción natural dieron lugar a diferentes notaciones como el cálculo al estilo de Fitch (o diagramas de Fitch) o el método de Suppes , del cual Lemmon dio una variante llamada sistema L. Dichos sistemas de presentación, que se describen más exactamente como tabulares, incluyen los siguientes.
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 prueba . Para formalizar la noción de prueba, modificamos 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 sucesor con la prueba real. Los antecedentes o hipótesis se separan del sucesor mediante un torniquete (⊢). Esta modificación recibe en ocasiones el nombre de hipótesis localizadas . El siguiente diagrama resume el cambio.
El conjunto de hipótesis se escribirá como Γ cuando su composición exacta no sea relevante. Para hacer las pruebas explícitas, pasamos del juicio sin pruebas " A verdadero " a un juicio: "π es una prueba de (A verdadero) ", que se escribe simbólicamente como "π : A verdadero ". Siguiendo el enfoque estándar, las pruebas se especifican con sus propias reglas de formación para el juicio " prueba π ". La prueba más sencilla posible es el uso de una hipótesis etiquetada; en este caso la evidencia es la propia etiqueta.
Por brevedad, dejaremos de lado la etiqueta de juicio verdadero en el resto de este artículo, es decir , escribiremos "Γ ⊢ π : A ". Reexaminemos algunos de los conectivos con pruebas explícitas. Para la conjunción, nos fijamos en la regla de introducción ∧I para descubrir la forma de las pruebas de conjunción: deben ser un par de pruebas de las dos conjunciones. De este modo:
Las reglas de eliminación ∧E 1 y ∧E 2 seleccionan la conjunción izquierda o derecha; por tanto, las pruebas son un par de proyecciones: la primera ( fst ) y la segunda ( snd ).
Por implicación, el formulario de introducción localiza o vincula la hipótesis, escrita utilizando una λ; esto corresponde a la etiqueta descargada. En la regla, "Γ, u : A " representa el conjunto de hipótesis Γ, junto con la hipótesis adicional u .
Con 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 un supuesto utilizado en otra prueba. Esto se conoce comúnmente como teorema de sustitución y puede demostrarse mediante inducción sobre la profundidad (o estructura) del segundo juicio.
Hasta ahora la sentencia "Γ ⊢ π : A " ha tenido una interpretación puramente lógica. En la teoría de tipos , la visión lógica se cambia por una visión más computacional de los objetos. Las proposiciones en la interpretación lógica ahora se consideran 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 conectivos lógicos también se les da una lectura diferente: la conjunción se ve como producto (×), la implicación como la flecha de función (→), etc. Sin embargo, las diferencias son sólo 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 tipos simples 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, existen programas canónicos de ese tipo que son irreductibles; éstas 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 normalizante (o débilmente normalizante ). Si la forma canónica es única, entonces se dice que la teoría es fuertemente normalizadora . La normalización es una característica rara de la mayoría de las teorías de tipos no triviales, lo que supone una gran desviación del mundo lógico. (Recuerde 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 reduzcan a un valor; Estos programas de bucle generalmente pueden tener cualquier tipo. En particular, el programa de bucle tiene el tipo ⊥, aunque no hay una prueba lógica de "⊥ verdadero ". Por ello, las proposiciones como tipos; El paradigma de las pruebas como programas solo funciona en una dirección, en todo caso: interpretar una teoría de tipos como una lógica generalmente da una lógica inconsistente.
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 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 de flecha y de producto, respectivamente, como lo atestiguan sus reglas de introducción y eliminación.
La teoría de tipos dependientes en toda su generalidad 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: o la verificación de tipos es indecidible ( teoría de tipos extensionales ) o el razonamiento extensional es más difícil ( teoría de tipos intensional ). 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 determinado , por ejemplo, números enteros, cadenas o programas lineales.
Dado que las teorías de tipos dependientes permiten que los tipos dependan de programas, una pregunta natural es si es posible que los programas dependan de tipos o de cualquier otra combinación. Hay muchos tipos de respuestas a estas preguntas. Un enfoque popular en la teoría de tipos es permitir que los programas se cuantifiquen según los tipos, también conocido como polimorfismo paramétrico ; Hay dos tipos principales de esto: si los tipos y los programas se mantienen separados, entonces se obtiene un sistema de comportamiento algo mejor llamado polimorfismo predicativo ; Si la distinción entre programa y tipo es borrosa, se obtiene el análogo teórico 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 entorno 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 decidibilidad 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.
Para simplificar, las lógicas presentadas hasta ahora han sido intuicionistas . La lógica clásica amplía la lógica intuicionista con un axioma o principio adicional del tercero excluido :
Esta afirmación no es obviamente ni una introducción ni una eliminación; de hecho, involucra 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 :
(XM 3 es simplemente XM 2 expresado en términos de E.) Este tratamiento del tercero excluido, además de ser objetable desde el punto de vista 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 únicamente 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 , por una noción más clásica, que recuerda al cálculo secuente : en forma localizada, en lugar de Γ ⊢ A , usó Γ ⊢ Δ, siendo Δ una colección de proposiciones. similar a Γ. Γ se trató como una conjunción y Δ como una disyunción. Esta estructura se tomó 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 callcc o un mecanismo de lanzamiento/captura visto en LISP y sus descendientes. (Ver también: control de primera clase).
Otra extensión importante fue para las lógicas modales y de otro tipo que necesitan algo más que el juicio básico de la 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, [4] y desde entonces han acumulado una gran cantidad de trabajos relacionados. Para dar un ejemplo sencillo, la lógica modal S4 requiere un nuevo juicio, " A válido ", que sea categórico respecto de la verdad:
Este juicio categórico se interioriza como un conectivo unario ◻ A (léase " necesariamente A ") con las siguientes reglas de introducción y eliminación:
Tenga en cuenta que la premisa " A valid " no tiene reglas que la definan; en cambio, se utiliza en su lugar 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 true " donde Γ contiene las hipótesis verdaderas como antes, y Ω contiene hipótesis válidas. A la derecha sólo hay una sentencia " A true "; La validez no es necesaria aquí ya que "Ω ⊢ A valid " es, por definición, lo mismo que "Ω;⋅ ⊢ A true ". Las formas de introducción y eliminación son entonces:
Las hipótesis modales tienen su propia versión de la regla de hipótesis y el teorema de sustitución.
Este marco de separación de juicios en distintas colecciones de hipótesis, también conocido como contextos multizona o poliádicos , es muy poderoso y extensible; se ha aplicado a muchas lógicas modales diferentes, y también a 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, se utilizan extensiones como el etiquetado o los 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 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 los hipersecuentes de Avron y Pottinger y la lógica de visualización de Belnap , a lógicas modales como S5 y B.
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 mediante deconstrucción, y las reglas de introducción hacen fluir la información hacia arriba mediante ensamblaje. Por lo tanto, una prueba de deducción natural no tiene una lectura puramente ascendente o descendente, lo que la hace inadecuada para la automatización en la búsqueda de pruebas. Para abordar este hecho, Gentzen propuso en 1935 su cálculo secuente , aunque inicialmente lo pensó como un dispositivo técnico para aclarar la consistencia de la lógica de predicados . Kleene , en su libro fundamental de 1952 Introducción a las metamatemáticas , dio la primera formulación del cálculo secuente en el estilo moderno. [11]
En el cálculo siguiente, 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 estructuralmente muy similares. Las reglas de eliminación, por otro lado, se convierten en reglas de izquierda en el cálculo siguiente. Para dar un ejemplo, consideremos la disyunción; las reglas correctas son familiares:
A la izquierda:
Recuerde la regla ∨E de deducción natural en forma localizada:
La proposición A ∨ B , que es sucesora de una premisa en ∨E, se convierte en hipótesis de la conclusión en la regla izquierda ∨L. Por tanto, las reglas de izquierda pueden verse como una especie de regla de eliminación invertida. Esta observación se puede ilustrar de la siguiente manera:
En el cálculo del secuente, las reglas izquierda y derecha se realizan al mismo tiempo 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 siguiente describen una transposición o un apretón de manos de una proposición izquierda y derecha:
La correspondencia entre el cálculo secuente y la deducción natural es un par de teoremas de solidez y completitud, ambos demostrables mediante un argumento inductivo.
Por estos teoremas queda claro que el cálculo siguiente no cambia la noción de verdad, porque el mismo conjunto de proposiciones siguen siendo verdaderas. Por lo tanto, se pueden utilizar los mismos objetos de prueba que antes en derivaciones de cálculo posteriores. Como ejemplo, consideremos las conjunciones. La regla correcta es prácticamente idéntica a la regla de introducción.
La regla de la izquierda, sin embargo, realiza algunas sustituciones adicionales que no se realizan en las reglas de eliminación correspondientes.
Por tanto, los tipos de demostraciones generadas en el cálculo secuencial son bastante diferentes de las de la deducción natural. El cálculo secuencial produce pruebas en lo que se conoce como 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 utilizando la propia deducción natural, obtiene lo que se llama cálculo de intercalación (descrito por primera vez por John Byrnes), que puede usarse para definir formalmente la noción de una forma normal 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.
En la mayoría de las lógicas que se comportan bien, 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; normalmente resulta extremadamente tedioso probar ciertas propiedades directamente en la deducción natural debido al número ilimitado de casos. Por ejemplo, considere demostrar que una proposición dada no es demostrable 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 secuente es completo con respecto a la deducción natural, por lo que basta con mostrar esta imposibilidad de demostrarlo en el cálculo secuente. Ahora bien, si el corte no está disponible como regla de inferencia, entonces todas las reglas secuenciales introducen una conectiva a la derecha o a la izquierda, por lo que la profundidad de una derivación secuencial está completamente limitada por las conectivas en la conclusión final. Por tanto, demostrar la imposibilidad de demostrarlo es mucho más fácil, porque sólo hay un número finito de casos a considerar, y cada caso está compuesto enteramente 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 siguiente, esto es manifiestamente cierto porque no existe 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.
La deducción natural visualizada como un juego de dominó
![{\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a{\text{ term}}}}{\text{ u}}\\\vdots \\{}[a/x ]A{\text{ verdadero}}\end{array}}{\forall xA{\text{ verdadero}}}}\;\forall _{I^{u,a}}\qquad \qquad {\frac { \forall xA{\text{ true}}\qquad t{\text{ término}}}{[t/x]A{\text{ true}}}}\;\forall _{E}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc5195d9b291c69b6559144bef68bd2a37999128)
![{\displaystyle {\frac {[t/x]A{\hbox{ true}}}{\exists xA{\hbox{ true}}}}\;\exists _ {I}\qquad \qquad {\cfrac { \begin{array}{cc}&\underbrace {\,{\cfrac {}{a{\hbox{ term}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x] A{\hbox{ true}}}}{\hbox{ v}}\,} \\&\vdots \\\exists xA{\hbox{ true}}\quad &C{\hbox{ true}}\\\ end{array}}{C{\hbox{ true}}}}\exists _{E^{a,u,v}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41809c5097384d4f64d22a0e1294992f3bae0b9e)
