## [Exportación (Currying)](/es/node/60944) Definición 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 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 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 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 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 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 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 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 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.