Un mapeo especificado mecánicamente desde fórmulas y pruebas de un lenguaje formal o sistema de pruebas a fórmulas y pruebas de otro, definido por reglas sobre la sintaxis (símbolos, conectivos, formación de términos) y destinado a preservar la derivabilidad sintáctica y propiedades pruebas‑teóricas relacionadas.

Principio

La traducción sintáctica se construye por recursión estructural sobre la sintaxis y por el mapeo de reglas de inferencia o construcciones de prueba de modo que las derivaciones en la fuente generen derivaciones en el objetivo; es algorítmica, a menudo composicional, y se orienta a preservar la demostrabilidad más que la única verdad semántica.

Demostración

La traducción negativa de Gödel–Gentzen transforma pruebas clásicas en pruebas intuicionistas mediante una transformación sintáctica recursiva de las fórmulas y una justificación a nivel de reglas que asegura que las derivaciones fuente producen derivaciones objetivo, embebiendo así la demostrabilidad clásica en la constructiva para una clase restringida de fórmulas.

Aplicación incorrecta

Asumir que una traducción sintáctica preserva automáticamente la semántica como la verdad modelo‑teórica, o que preserva la complejidad y la longitud de las pruebas; también aplicar indebidamente una traducción sintáctica diseñada para una noción deductiva a un sistema de destino incompatible sin ajustes.

Consecuencia

Una traducción sintáctica correcta garantiza la solidez del traslado de pruebas: si Γ ⊢_S φ entonces mapped(Γ) ⊢_T mapped(φ). Esto apoya el transporte mecanizado de pruebas, meta‑teoremas sobre conservatividad y embebidos formales de un cálculo en otro.

Inversión

Las traducciones semánticas (modelo‑teóricas) se centran en mapear modelos y condiciones de verdad en lugar de pruebas; un embebido puramente semántico no necesariamente proporciona una traducción sintáctica que convierta pruebas fuente en pruebas objetivo.

Límite

Requiere gramáticas formales explícitas y sistemas de prueba para fuente y objetivo y una descripción efectiva de la traducción; excluye la paráfrasis informal, codificaciones no efectivas o transformaciones que sólo preserven satisfacibilidad o verdad individual sin producir derivaciones en el objetivo.

Tensión semántica

Tensión entre traducciones sintácticas y embebidos semánticos: una traducción sintácticamente fiel puede ser semánticamente opaca (cambiar el comportamiento de los modelos) y, a la inversa, un embebido semántico puede no inducir una traducción sintáctica práctica de pruebas.

Síntesis

Una traducción sintáctica es un mapeo algorítmico y preservador de estructura sobre fórmulas y derivaciones que transporta la demostrabilidad de un sistema formal a otro; es el instrumento prueba‑teórico para embebidos, pruebas de conservatividad y migración automatizada de pruebas.