La equivalencia lógica que transforma una implicación cuyo antecedente es una conjunción en una implicación anidada: (A ∧ B) → C equivale a A → (B → C). En lecturas tipadas y computacionales esto corresponde al currying, el isomorfismo entre funciones de dos argumentos y funciones curryficadas.

Principio

Los antecedentes pueden reorganizarse desde un requisito conjunto a una secuencia de supuestos condicionales: demostrar C a partir de A y B juntos es equivalente a demostrar que A basta para mostrar que B implica C.

Demostración

Si se tiene una prueba de (lluvia ∧ frío) → cancelar, la exportación produce una prueba de lluvia → (frío → cancelar): suponga lluvia, luego suponga frío, derive cancelar usando la regla original. A la inversa, dada A → (B → C) y A y B, se deriva C.

Aplicación incorrecta

Tratar la exportación como válida en contextos donde la implicación no es material (por ejemplo en ciertas lógicas subestructurales, de relevancia o condicionales) o cuando modalidades cambian el alcance de los antecedentes puede conducir a transformaciones incorrectas.

Consecuencia

Simplifica la estructura de los antecedentes en las pruebas, alinea la implicación lógica con tipos de función en lenguajes de programación y permite transformaciones de currying que facilitan la abstracción y la reutilización de orden superior.

Inversión

La transformación inversa — desacurrificación — combina implicaciones anidadas en una sola implicación con antecedente conjuntivo: de A → (B → C) inferir (A ∧ B) → C completa el par de equivalencias.

Límite

Válida en la lógica proposicional y de predicados clásica e intuicionista bajo la implicación material estándar; puede fallar o requerir modificación en lógicas con restricciones de relevancia, sensibilidad a recursos (lineales) o cuando operadores modales interfieren entre antecedente y consecuente.

Tensión semántica

Tensión entre la conveniencia sintáctica de la exportación y contextos semánticos donde el significado de 'si' no es material o depende del contexto: la exportación confunde un supuesto conjunto con compromisos secuenciales, que pueden ser distintos en algunas lógicas o en el lenguaje natural.

Síntesis

La Exportación es la equivalencia que reinterpreta un antecedente conjuntivo como una condicional anidada, reflejando el isomorfismo del currying entre funciones de varios argumentos y cadenas de funciones unarias, válida bajo la implicación material estándar.