Interpretación dialéctica

En teoría de la demostración , la interpretación de Dialéctica ^[1] es una interpretación de la demostración de la lógica intuicionista ( aritmética de Heyting ) en una extensión de tipo finito de la aritmética recursiva primitiva , el llamado Sistema T. Fue desarrollada por Kurt Gödel para proporcionar una demostración de consistencia de la aritmética. El nombre de la interpretación proviene de la revista Dialéctica , donde el artículo de Gödel se publicó en un número especial de 1958 dedicado a Paul Bernays en su 70 cumpleaños.

Motivación

Mediante la traducción negativa de Gödel–Gentzen , la consistencia de la aritmética clásica de Peano ya se había reducido a la consistencia de la aritmética intuicionista de Heyting . La motivación de Gödel para desarrollar la interpretación dialéctica fue obtener una prueba de consistencia relativa para la aritmética de Heyting (y, por lo tanto, para la aritmética de Peano).

Lógica intuicionista

La interpretación tiene dos componentes: una traducción de fórmula y una traducción de prueba. La traducción de fórmula describe cómo cada fórmula de la aritmética de Heyting se asigna a una fórmula sin cuantificadores del sistema T, donde y son tuplas de variables nuevas (que no aparecen libres en ). Intuitivamente, se interpreta como . La traducción de prueba muestra cómo una prueba de tiene suficiente información para atestiguar la interpretación de , es decir, la prueba de se puede convertir en un término cerrado y una prueba de en el sistema T. ${\estilo de visualización A}$ $Estilo de visualización A_{D}(x;y)}$ ${\estilo de visualización x}$ ${\estilo de visualización y}$ ${\estilo de visualización A}$ ${\estilo de visualización A}$ $\existe x\para todo yA_{D}(x;y)$ ${\estilo de visualización A}$ ${\estilo de visualización A}$ ${\estilo de visualización A}$ ${\estilo de visualización t}$ $Estilo de visualización A_{D}(t;y)}$

Traducción de fórmulas

La fórmula libre de cuantificadores se define inductivamente sobre la estructura lógica de la siguiente manera, donde es una fórmula atómica: $Estilo de visualización A_{D}(x;y)}$ ${\estilo de visualización A}$ ${\estilo de visualización P}$

{\begin{array}{lcl}(P)_{D}&\equiv &P\\(A\wedge B)_{D}(x,v;y,w)&\equiv &A_{D}(x;y)\wedge B_{D}(v;w)\\(A\vee B)_{D}(x,v,z;y,w)&\equiv &(z=0\rightarrow A_{D}(x;y))\wedge (z\neq 0\to B_{D}(v;w))\\(A\rightarrow B)_{D}(f,g;x,w)&\equiv &A_{D}(x;fxw)\rightarrow B_{D}(gx;w)\\(\exists zA)_{D}(x,z;y)&\equiv &A_{D}(x;y)\\(\forall zA)_{D}(f;y,z)&\equiv &A_{D}(fz;y)\end{array}}

Traducción de prueba (solidez)

La interpretación de la fórmula es tal que siempre que sea demostrable en la aritmética de Heyting, entonces existe una secuencia de términos cerrados tal que sea demostrable en el sistema T. La secuencia de términos y la prueba de se construyen a partir de la prueba dada de en la aritmética de Heyting. La construcción de es bastante sencilla, excepto por el axioma de contracción que requiere la suposición de que las fórmulas sin cuantificadores son decidibles. ${\estilo de visualización A}$ ${\estilo de visualización t}$ $Estilo de visualización A_{D}(t;y)}$ ${\estilo de visualización t}$ $Estilo de visualización A_{D}(t;y)}$ ${\estilo de visualización A}$ ${\estilo de visualización t}$ $A\flecha derecha A\cuña A$

Principios de caracterización

También se ha demostrado que la aritmética de Heyting se extendió con los siguientes principios

Axioma de elección
Principio de Markov
Independencia de premisas para fórmulas universales

es necesario y suficiente para caracterizar las fórmulas de HA que son interpretables por la interpretación de Dialéctica. ^{[ cita requerida ]} El axioma de elección aquí se formula para cualquier predicado 2-ario en la premisa y una afirmación de existencia con una variable de tipo función en su conclusión.

Extensiones

La interpretación dialéctica básica de la lógica intuicionista se ha extendido a varios sistemas más fuertes. Intuitivamente, la interpretación dialéctica se puede aplicar a un sistema más fuerte, siempre que la interpretación dialéctica del principio adicional pueda ser atestiguada por términos en el sistema T (o una extensión del sistema T).

Inducción

Dado el teorema de incompletitud de Gödel (que implica que la consistencia de PA no puede probarse por medios finitistas ), es razonable esperar que el sistema T deba contener construcciones no finitistas. De hecho, este es el caso. Las construcciones no finitistas aparecen en la interpretación de la inducción matemática . Para dar una interpretación dialéctica de la inducción, Gödel hace uso de lo que hoy en día se llama funcionales recursivos primitivos de Gödel , que son funciones de orden superior con descripciones recursivas primitivas.

Lógica clásica

Las fórmulas y las pruebas de la aritmética clásica también pueden recibir una interpretación dialéctica mediante una incorporación inicial a la aritmética de Heyting seguida de la interpretación dialéctica de la aritmética de Heyting. Shoenfield , en su libro, combina la traducción negativa y la interpretación dialéctica en una única interpretación de la aritmética clásica.

Comprensión

En 1962, Spector ^[2] extendió la interpretación dialéctica de la aritmética de Gödel al análisis matemático completo, mostrando cómo al esquema de elección contable se le puede dar una interpretación dialéctica extendiendo el sistema T con recursión de barras .

Lógica lineal

La interpretación dialéctica se ha utilizado para construir un modelo del refinamiento de Girard de la lógica intuicionista conocida como lógica lineal , a través de los llamados espacios dialécticos . ^[3] Dado que la lógica lineal es un refinamiento de la lógica intuicionista, la interpretación dialéctica de la lógica lineal también puede verse como un refinamiento de la interpretación dialéctica de la lógica intuicionista.

Aunque la interpretación lineal en la obra de Shirahata ^[4] valida la regla de debilitamiento (en realidad es una interpretación de la lógica afín ), la interpretación de los espacios dialécticos de De Paiva no valida el debilitamiento para fórmulas arbitrarias.

Variantes

Desde entonces se han propuesto varias variantes de la interpretación de la dialéctica, en particular la variante de Diller-Nahm (para evitar el problema de la contracción) y las interpretaciones monótona de Kohlenbach y acotada de Ferreira-Oliva (para interpretar el lema débil de König ). Se pueden encontrar tratamientos completos de la interpretación en ^[5]^[6] y ^{[7] .}

Referencias

^ Kurt Gödel (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes . Dialéctica. págs. 280–287.
^ Clifford Spector (1962). Funcionales recursivos demostrables del análisis: una prueba de consistencia del análisis mediante una extensión de los principios de las matemáticas intuicionistas actuales . Teoría de funciones recursivas: Proc. Simposios sobre matemáticas puras. pp. 1–27.
^ Valeria de Paiva (1991). Las categorías de la dialéctica (PDF) . Universidad de Cambridge, Laboratorio de Computación, Tesis doctoral, Informe técnico 213.
^ Masaru Shirahata (2006). La interpretación dialéctica de la lógica afín clásica de primer orden. Teoría y aplicaciones de categorías, vol. 17, núm. 4, págs. 49-79.
^ Jeremy Avigad y Solomon Feferman (1999). Interpretación funcional ("Dialectica") de Gödel (PDF) . en S. Buss ed., The Handbook of Proof Theory, North-Holland. págs. 337–405.
^ Ulrich Kohlenbach (2008). Teoría de la prueba aplicada: interpretaciones de la prueba y su uso en matemáticas . Springer Verlag, Berlín. pp. 1–536.
^ Anne S. Troelstra (con CA Smoryński, JI Zucker, WA Howard) (1973). Investigación metamatemática de la aritmética y el análisis intuicionistas . Springer Verlag, Berlín. pp. 1–323.{{cite book}}: CS1 maint: varios nombres: lista de autores ( enlace )