stringtranslate.com

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 .

Lógica proposicional

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 ¬¬φ.

Resultados

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 .

Lógica de primer orden

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).

Variantes equivalentes

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.

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.

Resultados

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.

Aritmética

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

Véase también

Referencias

Enlaces externos