Interpretación dialéctica

En la teoría de la prueba , la interpretación Dialectica ^[1] es una interpretación de prueba 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 desarrollado por Kurt Gödel para proporcionar una prueba de consistencia de la aritmética. El nombre de la interpretación proviene de la revista Dialectica , donde se publicó el artículo de Gödel en un número especial de 1958 dedicado a Paul Bernays en su 70 cumpleaños.

Motivación

A través de 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 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 la 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 la prueba muestra cómo una prueba de tiene suficiente información para presenciar la interpretación de , es decir, la prueba de puede convertirse en un término cerrado y una prueba de en el sistema T. $A$ $A_{D}(x;y)$ $x$ $y$ $A$ $A$ $\existe x\forall yA_{D}(x;y)$ $A$ $A$ $A$ $t$ $A_{D}(t;y)$

Traducción de fórmulas

La fórmula sin cuantificadores se define inductivamente en la estructura lógica de la siguiente manera, donde es una fórmula atómica: $A_{D}(x;y)$ $A$ $P$

{\begin{array}{lcl}(P)_{D}&\equiv &P\\(A\wedge B)_{D}(x,v;y,w)&\equiv &A_{D }(x;y)\cuña 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 es demostrable en la aritmética de Heyting, entonces existe una secuencia de términos cerrados tal que es 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. $A$ $t$ $A_{D}(t;y)$ $t$ $A_{D}(t;y)$ $A$ $t$ $A\rightarrow 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 premisa 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 necesaria ]} 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 sólidos. 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 del 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 llaman funcionales recursivos primitivos de Gödel , que son funciones de orden superior con descripciones recursivas primitivas.

Lógica clásica

A las fórmulas y pruebas en aritmética clásica también se les puede dar una interpretación Dialectica mediante una incorporación inicial en la aritmética de Heyting seguida de la interpretación Dialectica de la aritmética de Heyting. Shoenfield , en su libro, combina la traducción negativa y la interpretación Dialectica en una única interpretación de la aritmética clásica.

Comprensión

En 1962, Spector ^[2] amplió 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 de Dialectica se ha utilizado para construir un modelo del refinamiento de la lógica intuicionista de Girard conocido como lógica lineal , a través de los llamados espacios de Dialectica . ^[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 Dialectica, en particular la variante de Diller-Nahm (para evitar el problema de la contracción) y las interpretaciones monótonas de Kohlenbach y acotadas 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 de análisis demostrablemente recursivos: una prueba de coherencia del análisis mediante una extensión de principios en las matemáticas intuicionistas actuales . Teoría de la función recursiva: proc. Simposios de Matemática Pura. págs. 1–27.
↑ Valeria de Paiva (1991). Las categorías de Dialéctica (PDF) . Universidad de Cambridge, Laboratorio de Computación, Tesis Doctoral, Informe Técnico 213.
^ Masaru Shirahata (2006). La interpretación Dialectica 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). La interpretación funcional de Gödel ("Dialéctica") (PDF) . en S. Buss ed., The Handbook of Proof Theory, Holanda Septentrional. 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. págs. 1–536.
^ Anne S. Troelstra (con CA Smoryński, JI Zucker, WAHoward) (1973). Investigación metamatemática de análisis y aritmética intuicionista . Springer Verlag, Berlín. págs. 1–323.{{cite book}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )