deducción natural

Tipo de cálculo de prueba

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. ^[1] 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 .

Historia

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. ^[2] 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 ahora conocida como notación de Suppes-Lemmon .

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 . ^[3] 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 ^[5] 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. ^[6]

Historia de los estilos de notación.

La deducción natural ha tenido una gran variedad de estilos de notación, ^[7] lo que puede dificultar el reconocimiento de una prueba si no estás familiarizado con uno de ellos. Para ayudar con esta situación, este artículo tiene una sección § Notación que explica cómo leer toda la notación que realmente 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 pública de derechos de autor ; se remite al lector a SEP e IEP para obtener imágenes.

• Gentzen inventó la deducción natural utilizando pruebas en forma de árbol; consulte § Notación de árbol de Gentzen para obtener más detalles.
• Jaśkowski cambió esto por una notación que usaba 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ó dependencias antecedentes mediante números de línea entre corchetes, anticipando 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 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á del todo claro si la notación de asterisco de Quine apareció en la edición original de 1950 o se agregó en una edición posterior).
• 1957: Introducción a la demostración de teoremas de lógica práctica en un libro de texto de Suppes (1999, págs. 25-150). Esto indicaba dependencias (es decir, proposiciones antecedentes) mediante números de línea a la izquierda de cada línea.
• 1963: Stoll (1979, págs. 183–190, 215–219) utiliza conjuntos de números de línea para indicar dependencias antecedentes de las líneas de argumentos lógicos secuenciales basados ​​en reglas de inferencia de deducción natural.
• 1965: El libro de texto completo de Lemmon (1965) es una introducción a las pruebas lógicas utilizando un método basado en el de Suppes , lo que ahora se conoce como notación de Suppes-Lemmon .
• 1967: En un libro de texto, Kleene (2002, págs. 50–58, 128–130) demostró brevemente dos tipos de pruebas lógicas prácticas: un sistema que utiliza citas explícitas de proposiciones antecedentes a la izquierda de cada línea y el otro sistema que utiliza barras verticales. -líneas a la izquierda para indicar dependencias. ^[a]

Notación

El lector debe estar familiarizado con los símbolos comunes de los conectivos lógicos . A continuación se muestra una tabla con las variantes de notación más comunes.

Notación del árbol de Gentzen

Gentzen , quien inventó 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. Digamos que tenemos un argumento de ejemplo simple en lógica proposicional , como, "si está lloviendo, entonces está nublado; está lloviendo; por lo tanto, está nublado". (Esto está en modus ponens ). Representando esto como una lista de proposiciones, como es común, 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 , ^{[11] [12]} separadas por una coma , que indica combinación de premisas. ^[13] La conclusión está escrita debajo de la línea de inferencia. ^[11] La línea de inferencia representa la consecuencia sintáctica , ^[11] a veces llamada consecuencia deductiva , ^[14] que también se simboliza con ⊢. ^{[15] [14]} Entonces, lo anterior también se puede escribir en una línea como . (El torniquete, para las consecuencias sintácticas, tiene menor precedencia que la coma, que representa una combinación de premisas, que a su vez tiene menor precedencia que la flecha, utilizada para implicaciones materiales; por lo que no se necesitan paréntesis para interpretar esta fórmula ⁾ . ^] ${\displaystyle P\to Q,P\vdash Q}$

La consecuencia sintáctica se contrasta con la consecuencia semántica , ^[16] que se simboliza con ⊧. ^{[15] [14]} En este caso, la conclusión se sigue sintácticamente porque la deducción natural es un sistema de prueba sintáctico , que asume 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 se pueden evitar representando las pruebas como un árbol de consecuentes Γ ⊢A en lugar de un árbol de juicios de que A (es verdadero).

Notación Suppes-Lemmon

Muchos libros de texto usan la notación Suppes-Lemmon , ^[7] por lo que este artículo también la brindará, aunque por ahora, esto solo se incluye para la lógica proposicional , y el resto de la cobertura se brinda solo en estilo Gentzen. Una prueba , presentada de acuerdo con el estilo de notación Suppes-Lemmon , es una secuencia de líneas que contienen oraciones, ^[17] donde cada oración es una suposición o el resultado de aplicar una regla de prueba a oraciones anteriores en la secuencia. ^[17] Cada línea de prueba se compone de una oración de prueba , junto con su anotación , su conjunto de supuestos y el número de línea actual . ^[17] El conjunto de supuestos enumera los supuestos de los que depende la oración de prueba dada, a los que se hace referencia mediante los números de línea. ^[17] La ​​anotación especifica qué regla de prueba se aplicó y a qué líneas anteriores, para producir la oración actual. ^[17] Aquí hay un ejemplo de prueba:

Esta prueba quedará más clara cuando se especifiquen las reglas de inferencia y sus anotaciones apropiadas; consulte § Reglas de inferencia proposicional (estilo Suppes-Lemmon).

Sintaxis del lenguaje proposicional

Esta sección define la sintaxis formal de un lenguaje de lógica proposicional , contrastando las formas comunes de hacerlo con una forma de hacerlo al estilo Gentzen.

Estilos de definición comunes

El lenguaje formal de un cálculo proposicional suele definirse mediante una definición recursiva , como ésta, de Bostock : ^[18] ${\displaystyle {\mathcal {L}}}$

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

Hay otras formas de hacerlo, como la gramática BNF . ^{[19] [20]} ${\displaystyle \phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\&~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi }$

Definición al estilo Gentzen

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. ^[20] Por ejemplo, el equivalente de las reglas 3 y 4, de la definición anterior de Bostock, 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 ve la sintaxis del idioma como una gramática categorial con la categoría única "fórmula", denotada por el símbolo . Por lo tanto, cualquier elemento de la sintaxis se introduce mediante categorizaciones, para las cuales la notación es , que significa " es una expresión para un objeto en la categoría ". ^[21] Las letras de las oraciones, entonces, se introducen mediante categorizaciones como ,  ,  , etc.; ^[21] los conectivos, a su vez, se definen mediante enunciados similares a los anteriores, pero usando notación de categorización, como se ve a continuación: ${\displaystyle {\mathcal {F}}}$ ${\displaystyle \varphi :{\mathcal {F}}}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathcal {F}}}$ ${\displaystyle P:{\mathcal {F}}}$ ${\displaystyle Q:{\mathcal {F}}}$ ${\displaystyle R:{\mathcal {F}}}$

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

Lógica proposicional al estilo Gentzen

Reglas de inferencia al estilo Gentzen

La siguiente es una lista completa de reglas de inferencia primitivas para la deducción natural en lógica proposicional clásica: ^[20]

Esta tabla sigue la costumbre de utilizar letras griegas como esquemas , que pueden abarcar cualquier fórmula, en lugar de sólo proposiciones atómicas. El nombre de una regla aparece a la derecha de su árbol de fórmulas. Por ejemplo, la primera regla de introducción se llama , que es la abreviatura de "introducción de conjunción". ${\displaystyle \wedge _{i}}$

Pruebas de ejemplo al estilo Gentzen

Como ejemplo del uso de reglas de inferencia, considere la conmutatividad de la conjunción. Si A ∧ B , entonces B ∧ A ; 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.

${\displaystyle {\cfrac {{\cfrac {A\wedge B}{B{\hbox{ }}}}\ \wedge _{E2}\qquad {\cfrac {A\wedge B}{A}}\ \wedge _{E1}}{B\wedge A}}\ \wedge _{I}}$

Como segundo ejemplo, considere la derivación de " A ⊃ (B ⊃ (A ∧ B)) ":

${\displaystyle {\cfrac {{\cfrac {{\cfrac {}{A}}\ u\quad {\cfrac {}{B}}\ w}{A\wedge B}}\ \wedge _{I}}{{\cfrac {B\supset \left(A\wedge B\right)}{A\supset \left(B\supset \left(A\wedge B\right)\right)}}\ \supset _{I^{u}}}}\ \supset _{I^{w}}}$

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

Lógica proposicional estilo Suppes-Lemmon

Reglas de inferencia estilo Suppes-Lemmon

Las reglas de inferencia de deducción natural, debidas en última instancia a Gentzen , se detallan a continuación. ^[22] Hay diez reglas primitivas de prueba, que son la regla de asunción , más cuatro pares de reglas de introducción y eliminación para las conectivas binarias, y la regla de reductio ad adbsurdum . ^[17] El silogismo disyuntivo se puede utilizar como una alternativa más fácil a la ∨-eliminación adecuada, ^[17] y MTT y DN son reglas comúnmente dadas, ^[22] aunque no son primitivas. ^[17]

Prueba de ejemplo estilo Suppes-Lemmon

Recuerde que ya se dio un ejemplo de prueba al presentar la notación § Suppes-Lemmon. Este es un segundo ejemplo.

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 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.

${\displaystyle {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ }}u\qquad {\cfrac {}{B\ }}w}{A\wedge B\ }}\wedge _{I}}{A\ }}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ }}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. De nuevo para conjunciones:

${\displaystyle {\cfrac {}{A\wedge B\ }}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ }}u}{A\ }}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ }}u}{B\ }}\wedge _{E2}}{A\wedge B\ }}\wedge _{I}\end{aligned}}}$

Estas nociones corresponden exactamente a la reducción β (reducción beta) y a 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, sobre todo en Dag Prawitz en 1961. ^[24] Es mucho más fácil demostrar esto indirectamente por medio de una prueba sin cortes. presentación de cálculo posterior .

Extensiones de primer orden y superiores

Resumen del sistema de primer orden.

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 una nueva categoría, "término", denominada . Fijaremos un conjunto contable de variables , otro conjunto contable de símbolos de funciones y construiremos términos con las siguientes reglas de formación: ${\displaystyle {\mathcal {T}}}$ ${\displaystyle V}$ ${\displaystyle F}$

${\displaystyle {\frac {v\in V}{v:{\mathcal {T}}}}{\hbox{ var}}_{F}}$

y

${\displaystyle {\frac {f\in F\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{f(t_{1},t_{2},\cdots ,t_{n}):{\mathcal {T}}}}{\hbox{ app}}_{F}}$

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:

${\displaystyle {\frac {\phi \in P\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{\phi (t_{1},t_{2},\cdots ,t_{n}):{\mathcal {F}}}}{\hbox{ pred}}_{F}}$

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 la cuantificación universal (∀) y existencial (∃):

${\displaystyle {\frac {x\in V\qquad A:{\mathcal {F}}}{\forall x.A:{\mathcal {F}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A:{\mathcal {F}}}{\exists x.A:{\mathcal {F}}}}\;\exists _{F}}$

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

${\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a:{\mathcal {T}}}}{\text{ u}}\\\vdots \\{}[a/x]A\end{array}}{\forall x.A}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A\qquad t:{\mathcal {T}}}{[t/x]A}}\;\forall _{E}}$

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

${\displaystyle {\frac {[t/x]A}{\exists x.A}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a:{\mathcal {T}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A\quad &C\\\end{array}}{C}}\exists _{E^{a,u,v}}}$

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. ^[c] 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:

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\forall p.A:{\mathcal {F}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\exists p.A:{\mathcal {F}}}}\;\exists _{F^{u}}}$

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 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.

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 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 " a un juicio: "π es una prueba de (A) ", que se escribe simbólicamente como "π : A ". 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.

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 ₁ y ∧E ₂ 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.

Teorema de sustitución

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 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 normalizadora (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 "⊥". 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.

Ejemplo: teoría de tipos dependientes

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.

Lógicas clásicas y modales.

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 :

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

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 ₃ es simplemente XM ₂ 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 A centrado en la verdad 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 similares. 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, ^[5] 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:

Si "A" (es verdadero) sin suponer que "B" (es verdadero), entonces "A es válido".

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:

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 " donde Γ contiene las hipótesis verdaderas como antes, y Ω contiene hipótesis válidas. A la derecha sólo hay una sentencia " A "; La validez no es necesaria aquí ya que "Ω ⊢ A valid " es, por definición, lo mismo que "Ω;⋅ ⊢ A ". 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.

Teorema de sustitución modal

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

Este marco de separación de juicios en distintos conjuntos 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.

Comparación con el cálculo secuencial

El cálculo secuencial 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. ^[25]

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.

Solidez de ⇒ wrt. ⊢

Si Γ ⇒ A , entonces Γ ⊢ A .

Integridad de ⇒ wrt. ⊢

Si Γ ⊢ A , entonces Γ ⇒ A .

De estos teoremas queda claro que el cálculo secuencial 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 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.

Cortar (sustitución)

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

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 : "⋅ ⊢ ⊥" 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.

Ver también

• Portal de filosofía

• Lógica matemática
• Cálculo secuencial
• Gerhard Gentzen
• Sistema L (deducción natural tabular)
• Mapa de argumentos , el término general para la notación lógica en forma de árbol

Notas

1. Una ventaja particular de los sistemas tabulares de deducción natural de Kleene es que demuestra la validez de las reglas de inferencia tanto para el cálculo proposicional como para el cálculo de predicados. Véase Kleene 2002, págs. 44–45, 118–119.
2. Para simplificar el enunciado de la regla, la palabra "negación" aquí se usa de esta manera: la negación de una fórmula que no es una negación es , mientras que una negación , tiene dos negaciones , a saber, y . ^[17] ${\displaystyle \varphi }$ ${\displaystyle -\varphi }$ ${\displaystyle -\varphi }$ ${\displaystyle \varphi }$ ${\displaystyle --\varphi }$
3. Consulte el artículo sobre cálculo lambda para obtener más detalles sobre el concepto de sustitución.

Referencias

Referencias generales

• Barker-Plummer, Dave; Barwise, Jon ; Etchemendy, John (2011). Prueba de lenguaje y lógica (2ª ed.). Publicaciones CSLI. ISBN 978-1575866321.
• Gallier, Jean (2005). "Lógica constructiva. Parte I: Tutorial sobre sistemas de prueba y cálculos λ mecanografiados" . Consultado el 12 de junio de 2014 .
• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift . 39 (2): 176–210. doi :10.1007/BF01201353. S2CID  121546341. (Traducción al inglés Investigations into Logical Deduction en ME Szabo. The Collected Works of Gerhard Gentzen. North-Holland Publishing Company, 1969.)
• Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift . 39 (3): 405–431. doi :10.1007/bf01201363. S2CID  186239837.
• Girard, Jean-Yves (1990). Pruebas y tipos. Tratados de Cambridge sobre informática teórica. Cambridge University Press, Cambridge, Inglaterra. Archivado desde el original el 4 de julio de 2016 . Consultado el 20 de abril de 2006 .Traducido y con apéndices de Paul Taylor e Yves Lafont.
• Jaśkowski, Stanisław (1934). Sobre las reglas de los supuestos en lógica formal .Reimpreso en lógica polaca 1920-1939 , ed. Storrs McCall.
• Kleene, Stephen Cole (1980) [1952]. Introducción a las metamatemáticas (Undécima ed.). Holanda del Norte. ISBN 978-0-7204-2103-3.
• Kleene, Stephen Cole (2009) [1952]. Introducción a las metamatemáticas . Ishi Press Internacional. ISBN 978-0-923891-57-2.
• Kleene, Stephen Cole (2002) [1967]. Lógica matemática . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Lógica inicial . Tomás Nelson. ISBN 978-0-17-712040-4.
• Martin-Löf, Per (1996). «Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas» (PDF) . Revista nórdica de lógica filosófica . 1 (1): 11–60.Apuntes de conferencias de un curso breve en la Università degli Studi di Siena, abril de 1983.
• Pfenning, Frank; Davies, serbal (2001). "Una reconstrucción crítica 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 teórico de prueba . Acta Universitatis Stockholmiensis, Estudios de filosofía de Estocolmo 3. Estocolmo, Göteborg, Uppsala: Almqvist & Wicksell.
• Prawitz, Dag (2006) [1965]. Deducción natural: un estudio teórico de prueba . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-44655-4.
• Quine, Willard Van Orman (1981) [1940]. Lógica matemática (Ed. Revisada). Cambridge, Massachusetts: Prensa de la Universidad de Harvard. ISBN 978-0-674-55451-1.
• Quine, Willard Van Orman (1982) [1950]. Métodos de lógica (Cuarta ed.). Cambridge, Massachusetts: Prensa de la Universidad de Harvard. ISBN 978-0-674-57176-1.
• Simpson, Álex (1993). La teoría de la prueba y la semántica de la lógica modal intuicionista (PDF) . Universidad de Edimburgo.Tesis doctoral.
• Stoll, Robert Roth (1979) [1963]. Teoría y Lógica de Conjuntos . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-63829-4.
• Stouppa, Phiniki (2004). El diseño de teorías de prueba modales: el caso de S5 . Universidad de Dresde. CiteSeerX  10.1.1.140.1858 .Tesis de maestría.
• Suppes, Patrick Coronel (1999) [1957]. Introducción a la lógica . Mineola, Nueva York: Publicaciones de Dover. ISBN 978-0-486-40687-9.
• 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.

Citas en línea

1. "Deducción natural | Enciclopedia de Filosofía de Internet" . Consultado el 1 de mayo de 2024 .
2. Jaśkowski 1934.
3. Caballero 1934, Caballero 1935.
4. Caballero 1934, pag. 176.
5. Prawitz 1965, Prawitz 2006.
6. Martin-Löf 1996.
7. 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.
8. Quine (1981). Véanse en particular las páginas 91 a 93 para conocer la notación de números de línea de Quine para dependencias de antecedentes.
9. Platón, Jan von (2013). Elementos del razonamiento lógico (1. ed. publicada). Cambridge: prensa de la Universidad de Cambridge. pag. 9.ISBN​ 978-1-107-03659-8.
10. Weisstein, Eric W. "Conectivo". mathworld.wolfram.com . Consultado el 22 de marzo de 2024 .
11. Platón, Jan von (2013). Elementos del razonamiento lógico (1. ed. publicada). Cambridge: prensa de la Universidad de Cambridge. págs.9, 32, 121. ISBN 978-1-107-03659-8.
12. "Lógica proposicional". www.cs.miami.edu . Consultado el 22 de marzo de 2024 .
13. Restall, Greg (2018), "Substructural Logics", en Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (edición de primavera de 2018), Metaphysics Research Lab, Universidad de Stanford , consultado el 22 de marzo de 2024.
14. "Compacidad | Enciclopedia de Filosofía de Internet" . Consultado el 22 de marzo de 2024 .
15. "Temas de conferencias para estudiantes de matemáticas discretas". math.colorado.edu . Consultado el 22 de marzo de 2024 .
16. Paseau, Alejandro; Pregel, Fabian (2023), "El 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.
17. Allen, Colin; Mano, Michael (2022). Manual de lógica (3ª ed.). Cambridge, Massachusetts: Prensa del MIT. ISBN 978-0-262-54364-4.
18. Bostock, David (1997). Lógica intermedia . Oxford: Nueva York: Clarendon Press; Prensa de la Universidad de Oxford. pag. 21.ISBN​ 978-0-19-875141-0.
19. Hansson, Sven Ove; Hendricks, Vincent F. (2018). Introducción a la filosofía formal . Textos universitarios de Springer en filosofía. Cham: Springer. pag. 38.ISBN​ 978-3-030-08454-7.
20. 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. págs.2, 20. doi :10.1007/978-3-319-51653-0. ISBN 978-3-319-51651-6.
21. Platón, Jan von (2013). Elementos del razonamiento lógico. Prensa de la Universidad de Cambridge. págs. 12-13. ISBN 978-1-107-03659-8.
22. Lemmon, Edward John (1998). Lógica inicial . Boca Ratón, FL: Chapman & Hall/CRC. págs. passim, especialmente 39-40. ISBN 978-0-412-38090-7.
23. Arthur, Richard TW (2017). Una introducción a la lógica: uso de deducción natural, argumentos reales, un poco de historia y algo de humor (2ª ed.). Peterborough, Ontario: Prensa Broadview. ISBN 978-1-55481-332-2. OCLC  962129086.
24. Véase también su libro Prawitz 1965, Prawitz 2006.
25. Kleene 2009, págs. 440–516. Véase también Kleene 1980.

enlaces externos

• Laboreo, Daniel Clemente (agosto de 2004). «Introducción a la deducción natural» (PDF) .
• "Dominó sobre ácido" . Consultado el 10 de diciembre de 2023 . La deducción natural visualizada como un juego de dominó
• Pelletier, Francis Jeffry. "Libros de texto de historia de la deducción natural y lógica elemental" (PDF) .
• Entrada "Sistemas de deducción natural en lógica" de Pelletier, Francis Jeffry; Hazen, Allen en la Enciclopedia de Filosofía de Stanford , 29 de octubre de 2021
• Levy, Michel. "Un demostrador proposicional".