En la teoría de la prueba , una disciplina dentro de la lógica matemática , la traducción de doble negación , a veces llamada traducción negativa , es un enfoque general para incrustar la lógica clásica en la lógica intuicionista , típicamente traduciendo fórmulas a fórmulas que son clásicamente equivalentes pero intuicionistas no equivalentes. Ejemplos particulares de traducción de doble negación incluyen la traducción de Glivenko para la lógica proposicional y la traducción de Gödel-Gentzen y la traducción de Kuroda para la lógica de primer orden .
Lógica proposicional
La traducción de doble negación más fácil de describir proviene del teorema de Glivenko , probado por Valery Glivenko en 1929. Asigna cada fórmula clásica φ a su doble negación ¬¬φ.
El teorema de Glivenko establece:
- Si φ es una fórmula proposicional, entonces φ es una tautología clásica si y solo si ¬¬φ es una tautología intuicionista.
El teorema de Glivenko implica la declaración más general:
- Si T es un conjunto de fórmulas proposicionales y φ una fórmula proposicional, entonces T ⊢ φ en lógica clásica si y solo si T ⊢ ¬¬φ en lógica intuicionista.
En particular, un conjunto de fórmulas proposicionales es intuicionistamente consistente si y solo si es clásicamente satisfactorio.
Lógica de primer orden
La traducción de Gödel-Gentzen (que lleva el nombre de Kurt Gödel y Gerhard Gentzen ) asocia con cada fórmula a en un lenguaje de primer orden otra fórmula φ N , que se define inductivamente:
- Si φ es atómico, entonces φ N es ¬¬φ
- (φ ∧ θ) N es φ N ∧ θ N
- (φ ∨ θ) N es ¬ (¬φ N ∧ ¬θ N )
- (φ → θ) N es φ N → θ N
- (¬φ) N es ¬φ N
- (∀ x φ) N es ∀ x φ N
- (∃ x φ) N es ¬∀ x ¬φ N
Esta traducción tiene la propiedad de que φ N es clásicamente equivalente a φ. El teorema de la solidez fundamental (Avigad y Feferman 1998, p. 342; Buss 1998 p. 66) establece:
- Si T es un conjunto de axiomas y φ es una fórmula, entonces T prueba φ usando lógica clásica si y solo si T N prueba φ N usando lógica intuicionista.
Aquí T N consta de las traducciones de las fórmulas de la doble negación T .
Una oración φ puede no implicar su traducción negativa φ N en la lógica intuicionista de primer orden. Troelstra y van Dalen (1988, Cap. 2, Sec. 3) dan una descripción (debido a Leivant) de fórmulas que implican su traducción Gödel-Gentzen.
Variantes
Hay varias definiciones alternativas de la traducción negativa. Todos son demostrablemente equivalentes en lógica intuicionista, pero pueden ser más fáciles de aplicar en contextos particulares.
Una posibilidad es cambiar las cláusulas de disyunción y cuantificador existencial a
- (φ ∨ θ) N es ¬¬ (φ N ∨ θ N )
- (∃ x φ) N es ¬¬∃ x φ N
Entonces la traducción se puede describir sucintamente como: prefijo ¬¬ a cada fórmula atómica, disyunción y cuantificador existencial.
Otra posibilidad (conocida como traducción de Kuroda ) es construir φ N a partir de φ poniendo ¬¬ antes de la fórmula completa y después de cada cuantificador universal . Observe que esto se reduce a la simple traducción ¬¬φ si φ es proposicional.
También es posible definir φ N prefijando ¬¬ antes de cada subfórmula de φ, como lo hizo Kolmogorov . Dicha traducción es la contraparte lógica de la traducción de estilo de continuación-paso de llamada por nombre de lenguajes de programación funcionales a lo largo de las líneas de la correspondencia Curry-Howard entre pruebas y programas.
Resultados
Gödel (1933) utilizó la traducción de doble negación para estudiar la relación entre las teorías clásica e intuicionista de los números naturales ("aritmética"). Obtiene el siguiente resultado:
- Si una fórmula φ se puede demostrar a partir de los axiomas de la aritmética de Peano, entonces φ N se puede demostrar a partir de los axiomas de la aritmética de Heyting .
Este resultado muestra que si la aritmética de Heyting es consistente, también lo es la aritmética de Peano. Esto se debe a que una fórmula contradictoria θ ∧ ¬θ se interpreta como θ N ∧ ¬θ N , que sigue siendo contradictoria. Además, la prueba de la relación es completamente constructiva, lo que permite transformar una prueba de θ ∧ ¬θ en la aritmética de Peano en una prueba de θ N ∧ ¬θ N en la aritmética de Heyting. (Combinando la traducción de doble negación con la traducción de Friedman , de hecho es posible probar que la aritmética de Peano es Π 0 2 - conservadora sobre la aritmética de Heyting).
El mapeo proposicional de φ a ¬¬φ no se extiende a una traducción sólida de la lógica de primer orden, porque ∀ x ¬¬φ ( x ) → ¬¬∀ x φ ( x ) no es un teorema de lógica de predicados intuicionista. Esto explica por qué φ N debe definirse de una manera más complicada en el caso de primer orden.
Ver también
Referencias
- J. Avigad y S. Feferman (1998), "Interpretación funcional (" Dialectica ") de Gödel", Manual de teoría de la prueba ", S. Buss, ed., Elsevier. ISBN 0-444-89840-9
- S. Buss (1998), "Introducción a la teoría de la prueba", Manual de la teoría de la prueba , S. Buss, ed., Elsevier. ISBN 0-444-89840-9
- G. Gentzen (1936), "Die Widerspruchfreiheit der reinen Zahlentheorie", Mathematische Annalen , v. 112, págs. 493–565 (alemán). Reproducido en traducción inglesa como "La consistencia de la aritmética" en Los artículos recopilados de Gerhard Gentzen , ME Szabo, ed.
- V. Glivenko (1929), Sur quelques points de la logique de M. Brouwer , Bull. Soc. Matemáticas. Belg. 15, 183-188
- K. Gödel (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines mathischen Kolloquiums , v. 4, págs. 34-38 (alemán). Reproducido en traducción inglesa como "Sobre aritmética intuicionista y teoría de números" en The Undecidable , M. Davis, ed., Págs. 75–81.
- AN Kolmogorov (1925), "O principe tertium non datur" (ruso). Reimpreso en traducción al inglés como "Sobre el principio del medio excluido" en From Frege to Gödel , van Heijenoort, ed., Págs. 414–447.
- AS Troelstra (1977), "Aspectos de las matemáticas constructivas", Manual de lógica matemática ", J. Barwise , ed., Holanda del Norte. ISBN 0-7204-2285-X
- AS Troelstra y D. van Dalen (1988), Constructivismo en Matemáticas. Una introducción , volúmenes 121, 123 de Estudios en lógica y fundamentos de las matemáticas , Holanda del Norte.
enlaces externos
- " Lógica intuicionista ", Enciclopedia de Filosofía de Stanford.