Un mapeo sintáctico de fórmulas y demostraciones de una teoría a otra que pretende preservar la consecuencia lógica, la demostrabilidad u otras relaciones estructurales proof-teóricas, de modo que las derivaciones en la fuente correspondan a derivaciones en el destino.

Principio

Una traducción se especifica por una regla que asigna a cada símbolo, fórmula o paso de demostración de la teoría fuente un homólogo en el lenguaje objetivo, típicamente preservando la consecuencia: si Γ ⊢_S φ entonces τ(Γ) ⊢_T τ(φ), donde τ es la función de traducción entre los lenguajes de S y T.

Demostración

La traducción negativa de Gödel envía cada fórmula clásica a una contraparte intuicionista insertando sistemáticamente dobles negaciones; esta traducción preserva la demostrabilidad en el sentido de que si la lógica clásica prueba φ entonces la lógica intuicionista prueba la traducida τ(φ), permitiendo el traslado de información proof-teórica entre sistemas.

Aplicación incorrecta

Suponer que cualquier traducción que mapee teoremas a teoremas constituye una equivalencia de teorías. Una traducción puede preservar la demostrabilidad en una dirección mientras falla en ser invertible o en respetar otros desiderata (complejidad, modelos pretendidos), por lo que considerarla una equivalencia total malinterpreta su alcance.

Consecuencia

Una traducción fiel permite comparar poder expresivo y fuerza de consistencia, transferir pruebas y resultados de consistencia, y construir interpretaciones; formaliza cómo una teoría puede ser embebida en otra para análisis sintáctico.

Inversión

El fracaso de la traducción es la incapacidad de hallar un mapeo sistemático que preserve la consecuencia, lo que indica una inconmensurabilidad genuina entre los recursos inferenciales de las dos teorías o la necesidad de ampliar el lenguaje destino o cambiar los criterios de traducción.

Límite

Las traducciones son dispositivos sintácticos y pueden no preservar rasgos semánticos como propiedades model-theóricas, interpretaciones pretendidas o complejidad computacional. La adecuación de una traducción depende de qué criterios de preservación se exijan (demostrabilidad, preservación de consecuencia, conservación de modelos, etc.).

Tensión semántica

La tensión radica entre traducción e interpretación: las traducciones actúan sobre objetos sintácticos y buscan preservar la derivabilidad, mientras que las interpretaciones semánticas actúan sobre modelos y estructuras; puede existir una traducción sin una interpretación model-theórica correspondiente y viceversa.

Síntesis

La traducción entre teorías es el procedimiento formal de mapear símbolos, fórmulas y demostraciones de una teoría a otra para preservar la estructura inferencial, permitiendo la comparación sintáctica, la inserción y el traslado de resultados según los criterios de preservación escogidos.