En teoría de la prueba , la interpretación Dialectica [1] es una interpretación prueba de aritmética intuicionista ( Heyting aritmética ) en una extensión de tipo finito de aritmética recursiva primitiva , el denominado T System . Fue desarrollado por Kurt Gödel para proporcionar una prueba de coherencia 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 coherencia relativa para la aritmética de Heyting (y, por tanto, para la aritmética de Peano).
Interpretación dialéctica de la 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 libre de 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 presenciar 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.
Traducción de fórmulas
La fórmula sin cuantificadores se define inductivamente en la estructura lógica de de la siguiente manera, donde es una fórmula atómica:
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 aritmética de Heyting. La construcción de es bastante sencillo, excepto por el axioma de contracción lo que requiere la suposición de que las fórmulas libres de cuantificadores son decidibles.
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 Dialectica. [ cita requerida ]
Extensiones de interpretación básica
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 extra 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 ser probada por medios finitistas ) es razonable esperar que el sistema T debe 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 denominan 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 demostraciones en aritmética clásica también se les puede dar una interpretación dialéctica mediante una incrustación inicial en 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 de la 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 el esquema de elección contable puede recibir una interpretación dialéctica extendiendo el sistema T con recursividad de barras .
Interpretación dialéctica de la 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 el trabajo de Shirahata [4] valida la regla del 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 de las fórmulas arbitrarias.
Variantes de la interpretación de Dialectica
Desde entonces se han propuesto varias variantes de la interpretación de Dialectica. Más notablemente, la variante Diller-Nahm (para evitar el problema de la contracción) y las interpretaciones monótona de Kohlenbach y Ferreira-Oliva acotada (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 . Dialectica. 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 los principios de la matemática intuicionista actual . 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 Dialectica (PDF) . Universidad de Cambridge, Laboratorio de Computación, Tesis de Doctorado, 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, 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 Aritmética y Análisis intuicionista . Springer Verlag, Berlín. págs. 1–323.CS1 maint: varios nombres: lista de autores ( enlace )