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 incorporar la lógica clásica a la lógica intuicionista . Por lo general, se hace traduciendo fórmulas a fórmulas que son clásicamente equivalentes pero intuicionistamente inequivalentes. Ejemplos particulares de traducciones 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 .
La traducción de doble negación más fácil de describir proviene del teorema de Glivenko , demostrado por Valery Glivenko en 1929. Asigna cada fórmula clásica φ a su doble negación ¬¬φ.
El teorema de Glivenko establece:
El teorema de Glivenko implica la afirmación más general:
En particular, un conjunto de fórmulas proposicionales es intuicionistamente consistente si y sólo si es clásicamente satisfactoria .
La traducción Gödel-Gentzen (que lleva el nombre de Kurt Gödel y Gerhard Gentzen ) asocia a cada fórmula φ en un lenguaje de primer orden otra fórmula φ N , que se define inductivamente:
como arriba, pero además
y de otra manera
Esta traducción tiene la propiedad de que φ N es clásicamente equivalente a φ. Troelstra y Van Dalen (1988, capítulo 2, sección 3) dan una descripción, debida a Leivant, de fórmulas que implican su traducción de Gödel-Gentzen también en la lógica intuicionista de primer orden. En este caso, este no es el caso para todas las fórmulas. (Esto está relacionado con el hecho de que las proposiciones con dobles negaciones adicionales pueden ser más fuertes que su variante más simple. Por ejemplo, ¬¬φ → θ siempre implica φ → θ, pero el esquema en la otra dirección implicaría la eliminación de la doble negación.)
Debido a equivalencias constructivas, existen varias definiciones alternativas de la traducción. Por ejemplo, una ley de De Morgan válida permite reescribir una disyunción negada . Por lo tanto, una posibilidad se puede describir sucintamente de la siguiente manera: prefijo "¬¬" antes de cada fórmula atómica, pero también para cada disyunción y cuantificador existencial ,
Otro procedimiento, conocido como traducción de Kuroda , consiste en construir una φ traducida poniendo "¬¬" antes de toda la fórmula y después de cada cuantificador universal . Este procedimiento se reduce exactamente a la traducción proposicional siempre que φ sea proposicional.
En tercer lugar, se puede anteponer "¬¬" antes de cada subfórmula de φ, como lo hizo Kolmogorov . Tal traducción es la contraparte lógica de la traducción de estilo de llamada por nombre de lenguajes de programación funcionales siguiendo las líneas de la correspondencia Curry-Howard entre pruebas y programas.
Las fórmulas traducidas de Gödel-Gentzen y Kuroda de cada φ son demostrablemente equivalentes entre sí, y este resultado ya se cumple en la lógica proposicional mínima . Y además, en lógica proposicional intuicionista, las fórmulas traducidas por Kuroda y Kolmogorov también son equivalentes.
La mera asignación proposicional de φ a ¬¬φ no se extiende a una traducción sólida de la lógica de primer orden, como ocurre con el llamado cambio de doble negación.
no es un teorema de la lógica de predicados intuicionista. Por tanto, las negaciones en φ N deben ubicarse de una manera más particular.
Sea T N las traducciones de doble negación de las fórmulas en T .
El teorema fundamental de solidez (Avigad y Feferman 1998, p. 342; Buss 1998 p. 66) establece:
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:
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 aritmética de Peano en una prueba de θ N ∧ ¬θ N en aritmética de Heyting.
Combinando la traducción de doble negación con la traducción de Friedman , es de hecho posible demostrar que la aritmética de Peano es Π 0 2 - conservadora sobre la aritmética de Heyting.