Die logische Äquivalenz, die eine Implikation mit konjunktivem Antezedens in eine geschachtelte Implikation überführt: (A ∧ B) → C ist äquivalent zu A → (B → C). In typentheoretischen und rechnerischen Deutungen entspricht dies dem Currying, der Isomorphie zwischen Funktionen zweier Argumente und gekurvten Funktionen.

Prinzip

Antezedenzien lassen sich von einer gemeinsamen Voraussetzung in eine Folge bedingter Annahmen umorganisieren: C aus A und B gemeinsam zu beweisen ist äquivalent dazu zu zeigen, dass A genügt, um zu beweisen, dass B C impliziert.

Demonstration

Hat man einen Beweis für (Regen ∧ Kälte) → Absage, liefert Exportation einen Beweis für Regen → (Kälte → Absage): Man nimmt Regen an, nimmt dann Kälte an und leitet Absage mithilfe der ursprünglichen Regel her. Umgekehrt folgt aus A → (B → C) und A und B C.

Fehlanwendung

Exportation in Kontexten als gültig zu behandeln, in denen die Implikation nicht materiell ist (etwa in manchen substrukturellen, relevanzorientierten oder bestimmten konditionalen Logiken) oder wenn Modalitäten die Reichweite der Voraussetzungen ändern, kann zu fehlerhaften Transformationen führen.

Konsequenz

Vereinfachung der Struktur von Voraussetzungen in Beweisen, Anpassung der logischen Implikation an Funktionstypen in Programmiersprachen und Ermöglichung von Currying-Transformationen, die höhere Abstraktion und Wiederverwendung erleichtern.

Umkehrung

Die Umkehrung — Uncurrying — kombiniert geschachtelte Implikationen zu einer einzigen Implikation mit konjunktivem Antezedens: aus A → (B → C) folgt (A ∧ B) → C und damit die Äquivalenz.

Abgrenzung

Gültig in klassischer und intuitionistischer Aussagen- und Prädikatenlogik unter standardmäßiger materieller Implikation; kann in Logiken mit Relevanzbedingungen, linearer Ressourcensensitivität oder wenn modale Operatoren intervenieren, versagen oder modifiziert werden müssen.

Semantische Spannung

Spannung zwischen der syntaktischen Bequemlichkeit der Exportation und semantischen Kontexten, in denen die Bedeutung von 'wenn' nicht materiell oder kontextabhängig ist: Exportation setzt eine gemeinsame Annahme mit sequentiellen Verpflichtungen gleich, welche in manchen Logiken oder der natürlichen Sprache unterschieden werden.

Synthese

Exportation ist die Äquivalenz, die ein konjunktives Antezedens als geschachtelte Bedingung umformt und damit das Currying-Isomorphismus zwischen Mehrargumentfunktionen und Ketten von Ein-Argument-Funktionen widerspiegelt; gültig unter standardmäßiger materieller Implikation.