Una transformación entre sistemas sintácticos, conjuntos de fórmulas o modelos que preserva la consecuencia lógica: siempre que una fórmula se deduce de un conjunto de premisas en la fuente (Γ ⊨ φ o Γ ⊢ φ), las imágenes de esas premisas implican la imagen de la conclusión en el objetivo (mapped(Γ) ⊨ mapped(φ) o mapped(Γ) ⊢ mapped(φ)).

Principio

La preservación de consecuencias significa que el mapeo respeta la relación de consecuencia pertinente (entailment semántico o derivabilidad sintáctica). Suele exigir que pruebas o entailments semánticos en la fuente puedan traducirse en pruebas o entailments en el objetivo, a menudo mediante un mapeo mecánico de reglas y fórmulas.

Demostración

Una traducción sintáctica que mapea cada regla de inferencia de un sistema de pruebas a un esquema demostrable en otro sistema proporciona un mapeo que preserva consecuencias; por ejemplo, una incrustación de un cálculo de prueba en otro que convierte pruebas fuente en pruebas objetivo preserva la consecuencia en sentido sintáctico.

Aplicación incorrecta

Suponer que la preservación de consecuencias implica preservación de la verdad de fórmulas individuales, o confundir la preservación del entailment clásico con la preservación de relaciones de consecuencia no monótonas o revisables sin verificar la noción de consecuencia del objetivo.

Consecuencia

Los mapeos que preservan consecuencias permiten transferir teoremas, obligaciones de prueba y argumentos de corrección entre formalismos; favorecen el razonamiento modular, la reutilización de derivaciones y el establecimiento de resultados de conservatividad o inclusión entre sistemas.

Inversión

La noción inversa es la reflexión de consecuencias: si mapped(Γ) implica mapped(φ) entonces Γ implica φ; la reflexión junto con la preservación proporciona equivalencia de consecuencias entre fuente y objetivo.

Límite

Se aplica sólo respecto de la noción de consecuencia especificada (semántica vs sintáctica, monótona vs no monótona); puede requerir ajustar el sistema de pruebas destino o enriquecer premisas para recuperar completitud, y excluye mapeos que sólo preservan satisfacibilidad o verdad de fórmulas sueltas pero no el entailment entre conjuntos.

Tensión semántica

Tensión entre preservación de consecuencias y restricciones prueba‑teóricas: un mapeo puede preservar entailment pero disparar la longitud o complejidad de las pruebas, o preservar entailment sólo a costa de cambiar la semántica de prueba prevista (p. ej. clásico a constructivo).

Síntesis

Un mapeo que preserva consecuencias es una traducción que respeta la estructura y transporta la consecuencia lógica de una fuente a un objetivo, permitiendo el traslado correcto de la derivabilidad y el estatus de teorema mientras exige una especificación precisa de qué noción de consecuencia se preserva.