Équivalence logique qui transforme une condition dont l'antécédent est une conjonction en une condition imbriquée : (A ∧ B) → C est équivalent à A → (B → C). Dans les interprétations typées et computationnelles, cela correspond au currying, l'isomorphisme entre fonctions de deux arguments et fonctions curryfiées.

Principe

Les antécédents peuvent être réorganisés d'une exigence conjointe en une séquence d'assomptions conditionnelles : prouver C à partir de A et B ensemble revient à prouver que A suffit pour montrer que B implique C.

Démonstration

Si l'on dispose d'une preuve que (pluie ∧ froid) → annuler, l'exportation donne une preuve de pluie → (froid → annuler) : supposez pluie, puis supposez froid, déduisez annuler en utilisant la règle originale. Réciproquement, donné A → (B → C) et A et B, on obtient C.

Mauvaise application

Traiter l'exportation comme valide dans des contextes où l'implication n'est pas matérielle (par exemple dans certaines logiques substructurales, de pertinence ou conditionnelles) ou lorsque des modalités changent la portée des antécédents peut conduire à des transformations incorrectes.

Conséquence

Simplifie la structure des antécédents dans les preuves, aligne l'implication logique avec les types de fonctions en programmation et permet des transformations de currying facilitant l'abstraction et la réutilisation en niveau supérieur.

Inversion

La transformation inverse — décurrification — combine des implications imbriquées en une seule implication à antécédent conjonctif : de A → (B → C) on déduit (A ∧ B) → C, complétant la paire d'équivalence.

Limite

Valide en logique propositionnelle et prédicative classique et intuitionniste sous l'implication matérielle standard ; peut échouer ou nécessiter une modification dans des logiques à contraintes de pertinence, sensibles aux ressources (linéaires) ou lorsque des opérateurs modaux interviennent entre antécédents et conséquent.

Tension sémantique

Tension entre la commodité syntaxique de l'exportation et des contextes sémantiques où le sens du « si » n'est pas matériel ou depende du contexte : l'exportation confond une hypothèse conjointe et des engagements séquentiels, qui peuvent être distincts dans certaines logiques ou dans le langage naturel.

Synthèse

L'Exportation est l'équivalence qui réinterprète un antécédent conjonctif comme une condition imbriquée, reflétant l'isomorphisme du currying entre fonctions à plusieurs arguments et chaînes de fonctions unaires, et valide sous l'implication matérielle standard.