Exportation (logic)¶
Convert an implication from a conjunction, (P ∧ Q) → R, into nested implications, P → (Q → R), under formal conjunction and implication rules.
Core Idea¶
Exportation changes an implication from a joint condition into one with the conditions taken in sequence: from (P ∧ Q) → R, derive P → (Q → R). P, Q, and R keep their roles. Going the other way is importation. In formal propositional or intuitionistic logic, both directions are valid, so the two forms are equivalent. Lean lists this equivalence and calls the nested form “curried.”[^ref-cbb42c9deb44]
Suppose a proof already shows that P and Q together imply R. To export Q, assume P, then Q, combine them into P ∧ Q, and use the original proof to get R. The result is a proof that P implies that Q implies R. This is a formal proof step, not a rule about every conversational use of “if.”[^ref-cbb42c9deb44]
Scope of Application¶
The rule applies where conjunction and implication have the formal introduction and elimination rules needed for the conversion. In Lean propositional proofs, And.intro forms the joint premise and implication introduction turns a proof under assumptions into a nested implication.[^ref-cbb42c9deb44]
A related conversion appears in typed programming. The Haskell 2010 Prelude defines curry to turn a function receiving a pair (a,b) into one receiving a and then b; uncurry reverses the change. Under the propositions-as-types reading, this is the product/function analogue of exportation and importation. A Haskell type is not simply an ordinary-language conditional.[ref-cbb42c9deb44][ref-5c133d8b4ab2]
Clarity¶
Keep the parentheses: (P ∧ Q) → R and P → (Q → R). The expression P → Q → R associates to the right in Lean; it does not mean (P → Q) → R. Exportation travels from joint antecedent to nested antecedents. Importation travels back.[^ref-cbb42c9deb44]
Name the host logic when using the law. A permission to rewrite one of these forms inside a larger formula requires the proof system's replacement or congruence rule. The exportation law alone does not permit arbitrary string substitution in proofs or programs.
Manages Complexity¶
Exportation gives a proof two ways to handle the same assumptions. The joint form accepts a proof of P ∧ Q at once. The nested form accepts P first and then Q. A proof can choose the form that matches the available assumptions without changing the conclusion R.[^ref-cbb42c9deb44]
The equivalent forms do not imply a universal performance advantage. Haskell specifies the pair-to-curried and curried-to-pair functions, but the choice of interface and any runtime cost are separate programming questions.[^ref-5c133d8b4ab2]
Abstract Reasoning¶
Start with h : (P ∧ Q) → R. Temporarily assume hp : P and hq : Q. And.intro hp hq supplies the argument to h, producing R. Discharge hq and hp in sequence. That constructs P → (Q → R). If starting from the nested form, take a proof of P ∧ Q, extract its two parts, and apply the nested implication twice; that is importation.[^ref-cbb42c9deb44]
This reasoning also shows why Logical Operation is the strict parent in the live catalog: the step has a typed formal input, a declared rule, and a determinate output. Exportation adds the specific joint-to-nested implication pattern. A general rule of replacement additionally needs a larger host formula, which this proof does not.[^ref-cbb42c9deb44]
Knowledge Transfer¶
The same role pattern appears in a proof and in a typed function conversion: joint input becomes sequential input while the roles and final result stay aligned. Lean uses propositions P, Q, R and conjunction/implication; Haskell uses types a, b, c and pair/function types. The correspondence helps explain currying, but it does not transfer all logical claims to arbitrary code or all programming behavior to logic.[ref-cbb42c9deb44][ref-5c133d8b4ab2]
Example¶
Lean proof. Given h : (P ∧ Q) → R, form a proof fun hp => fun hq => h (And.intro hp hq). Mapped roles: formal setting → Lean propositions; joint input → h; sequential output → P → Q → R; conversion → conjunction introduction plus implication abstraction; preserved content → the same P, Q, R.[^ref-cbb42c9deb44]
Haskell function. Given f :: (a,b) -> c, the Prelude defines curry f x y = f (x,y). Mapped roles: typed analogue → Haskell function and pair types; joint input → (a,b); sequential output → a -> b -> c; conversion → curry; preserved content → the same input types and result type. This is a programming analogue under Curry–Howard, not another ordinary-language conditional rule.[ref-cbb42c9deb44][ref-5c133d8b4ab2]
Relationships to Other Abstractions¶
Current abstraction Exportation (logic) Domain-specific
Parents (1) — more general patterns this builds on
-
Exportation (logic) is a kind of Logical Operation Domain-specific
Exportation is a particular typed logical transformation from an implication with a joint antecedent to one with nested antecedents.
Hierarchy path (1) — routes to 1 parentless root
- Exportation (logic) → Logical Operation → Transformation → Function (Mapping)
Neighborhood in Abstraction Space¶
Exportation (logic) sits in a sparse region of the domain-specific corpus (89th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Logical Semantics & Many-Valued Systems (11 abstractions)
Nearest neighbors
- Peirce's Law — 0.82
- Boolean Conjunctive Query — 0.81
- Denying the Antecedent — 0.80
- Constructive dilemma — 0.80
- Non-logical symbol — 0.79
Computed from structural-signature embeddings · 2026-10-08
Not to Be Confused With¶
Exportation is not importation, which runs in the reverse direction. It is not the material conditional, which is a connective rather than this relation between two whole formulas. It is not the general Rule of Replacement, which licenses an admitted equivalence at a selected location inside a larger formula. And it does not justify moving premises among arbitrary natural-language conditionals without fixing their logic.[^ref-cbb42c9deb44]
References¶
[^ref-cbb42c9deb44]: Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich et al., Theorem Proving in Lean 4, Chapter 3, “Propositions and Proofs”, §§3.1, 3.3.1, and 3.6 (especially “Other properties,” item 7). Official Lean text. It directly lists the import–export equivalence, explains right-associating implication and the curried reading, and gives conjunction introduction/elimination and the propositions-as-types correspondence. The displayed exportation proof in this entry is reconstructed from those rules.
[^ref-5c133d8b4ab2]: Simon Marlow, ed., Haskell 2010 Language Report, Chapter 9, “Standard Prelude,” printed p. 116 (curry and uncurry type signatures and definitions). Official language report. It directly supports the pair-input and curried-function conversions; applying them as a Curry–Howard analogue is explicitly labelled as an interpretation.