En teoría de la demostración , 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 realiza 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 satisfacible .
La traducción de Gödel–Gentzen (llamada así por Kurt Gödel y Gerhard Gentzen ) asocia con 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. 2, Sec. 3) dan una descripción, debida a Leivant, de fórmulas que sí implican su traducción de Gödel–Gentzen también en 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 las 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 . Una posibilidad puede describirse sucintamente de la siguiente manera: prefijo "¬¬" antes de cada fórmula atómica, pero también de cada disyunción y cuantificador existencial ,
Otro procedimiento, conocido como traducción de Kuroda , consiste en construir una φ traducida colocando "¬¬" 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 "¬¬" a cada subfórmula de φ, como hizo Kolmogorov . Esta traducción es la contraparte lógica de la traducción de estilo de paso de continuación de llamada por nombre de los lenguajes de programación funcional, siguiendo las líneas de la correspondencia de Curry-Howard entre pruebas y programas.
Las fórmulas traducidas por Gödel-Gentzen y Kuroda de cada φ son equivalentes entre sí, y este resultado se cumple ya en la lógica proposicional mínima . Y además, en la lógica proposicional intuicionista, las fórmulas traducidas por Kuroda y Kolmogorov también son equivalentes.
El mero mapeo proposicional de φ a ¬¬φ no se extiende a una traducción sólida de la lógica de primer orden, como el llamado cambio de doble negación.
no es un teorema de lógica de predicados intuicionista. Por lo tanto, las negaciones en φ N deben colocarse de una manera más particular.
Sea T N las traducciones de doble negación de las fórmulas en T .
El teorema de solidez fundamental (Avigad y Feferman 1998, p. 342; Buss 1998, p. 66) establece:
La traducción de doble negación fue utilizada por Gödel (1933) para estudiar la relación entre las teorías clásica e intuicionista de los números naturales ("aritmética"). Obtuvo el siguiente resultado:
Este resultado muestra que si la aritmética de Heyting es consistente, entonces 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 demostrar que la aritmética de Peano es Π 0 2 - conservadora respecto de la aritmética de Heyting.