Traducción de doble negación

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:

Si φ es una fórmula proposicional, entonces φ es una tautología clásica si y sólo si ¬¬φ es una tautología intuicionista.

El teorema de Glivenko implica la afirmació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 sólo si T ⊢ ¬¬φ en lógica intuicionista.

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:

• Si φ es atómico, entonces φ ^N es ¬¬φ

Como arriba, pero además

• (φ ∨ θ) ^N es ¬(¬φ ^N ∧ ¬θ ^N )
• (∃ x φ) ^N es ¬(∀ x ¬φ ^N )

y de otra manera

• (φ ∧ θ) ^N es φ ^N ∧ θ ^N
• (φ → θ) ^N es φ ^N → θ ^N
• (¬φ) ^N es ¬φ ^N
• (∀ x φ) ^N es ∀ x φ ^N

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 ,

• (φ ∨ θ) ^N es ¬¬(φ ^N ∨ θ ^N )
• (∃ x φ) ^N es ¬¬∃ x φ ^N

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.

∀ x ¬¬φ( x ) → ¬¬∀ x φ( x )

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:

Si T es un conjunto de axiomas y φ es una fórmula, entonces T demuestra φ usando la lógica clásica si y sólo si T ^N demuestra φ ^N usando la lógica intuicionista.

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:

Si una fórmula φ es demostrable a partir de los axiomas de la aritmética de Peano , entonces φ ^N es demostrable a partir de los axiomas de la aritmética de Heyting .

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 Π ⁰ ₂ - conservadora respecto de la aritmética de Heyting.

• Interpretación dialéctica
• Compañero modal

• J. Avigad y S. Feferman (1998), "La interpretación funcional ("dialéctica") de Gödel", Handbook of Proof Theory, S. Buss, ed., Elsevier. ISBN  0-444-89840-9
• S. Buss (1998), "Introducción a la teoría de la prueba", Handbook of Proof Theory , 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). Reimpreso en traducción al inglés como "La consistencia de la aritmética" en The Collected Papers of Gerhard Gentzen , ME Szabo, ed.
• V. Glivenko (1929), Sur quelques point de la logique de M. Brouwer , Bull. Soc. Matemáticas. Belga. 15, 183-188
• K. Gödel (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines mathematischen Kolloquiums , v. 4, págs. 34-38 (alemán). Reimpreso en traducción al inglés como "Sobre la aritmética intuicionista y la teoría de números" en The Undecidable , M. Davis, ed., págs.
• 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 Septentrional. ISBN 0-7204-2285-X 
• AS Troelstra y D. van Dalen (1988), Constructivismo en matemáticas. Introducción , volúmenes 121 y 123 de Estudios de lógica y fundamentos de las matemáticas , Holanda Septentrional.

• "Lógica intuicionista", Enciclopedia de Filosofía de Stanford.
• Moot, Richard; Retoré, Christian (2016). "Lógica clásica y lógica intuicionista: formulaciones equivalentes en la deducción natural, traducción de Gödel-Kolmogorov-Glivenko". arXiv : 1602.07608 [math.LO].