Exportation (logic)¶

Convert an implication from a conjunction, (P ∧ Q) → R, into nested implications, P → (Q → R), under formal conjunction and implication rules.

Version: v1 · 2026-10-07 · History
Domain-specific #: 13882
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomain: Propositional Logic → Mathematics
Aliases: Exportation, Import-export equivalence

Core Idea¶

Exportation converts a conditional whose antecedent is a conjunction into nested conditionals: from \((P\land Q)\to R\), obtain \(P\to(Q\to R)\). The same propositions occupy the same roles; the two required assumptions are repackaged so that \(P\) is taken first and \(Q\) second. Importation goes the other way. Under ordinary propositional or intuitionistic conjunction and implication rules, both directions hold, giving the import–export equivalence \(((P\land Q)\to R)\leftrightarrow(P\to(Q\to R))\). The Lean theorem-proving text lists this equivalence and calls the nested form “curried.”^[1]

The directional distinction matters in a proof. Given a proof \(h\) of \((P\land Q)\to R\), assume \(P\), then assume \(Q\); form \(P\land Q\) and apply \(h\) to obtain \(R\). Exportation is this joint-to-sequential step. The inverse combines proofs of \(P\) and \(Q\) from a conjunction and applies a nested implication. Nothing here asserts that every ordinary-language “if” or counterfactual conditional obeys the same law.^[1]

Structural Signature¶

Signature: formal implication from joint assumptions \((P\land Q)\to R\) → exportation under conjunction and implication rules → nested assumption form \(P\to(Q\to R)\), with \(P\), \(Q\), and \(R\) preserved.^[1]

Formal setting. The host logic supplies conjunction and implication with rules that license the conversion. A bare English conditional does not fix those rules.^[1]
Joint-antecedent input. \(P\land Q\) occurs as the antecedent of an implication to \(R\). Without this pairing there is no conjunct to export.^[1]
Nested-antecedent output. \(P\to(Q\to R)\) makes the dependence on \(P\) and then \(Q\) explicit. Implication associates to the right in the displayed Lean notation.^[1]
Directional conversion. Conjunction introduction and implication introduction/application construct the output from the input. The reverse proof establishes equivalence but is importation, a separately directed move.^[1]
Role preservation. The result still derives \(R\) from \(P\) and \(Q\). Replacing a proposition or reversing an arrow is a different rule.^[1]

What It Is Not¶

Exportation is not the material conditional itself. That connective supplies one kind of formal arrow; exportation relates two larger formulas built with conjunction and arrow. It is also not the generic Rule of Replacement. The live replacement entry says when an admitted equivalence can rewrite a selected subformula inside a host formula. Exportation identifies this particular equivalence and direction even when no larger host formula is present.^[1]

Nor is it a universal principle about every conditional in speech, probability, or counterfactual reasoning. Its stated scope fixes formal implication and conjunction. A Haskell function on a pair can be curried into a function returning a function; that is a typed-programming analogue under propositions-as-types, not a warrant to rewrite arbitrary source code or to treat a computational type as a truth-functional proposition.^[1]^[2]

Scope of Application¶

In a propositional or intuitionistic proof, exportation can change a theorem stated with joint assumptions into one that accepts assumptions sequentially. Lean lists the biconditional as a propositional validity; its conjunction rules show how to package and unpack the joint assumption. The operation remains the same when \(P\), \(Q\), and \(R\) are replaced by different well-formed propositions.^[1]

Under the Curry–Howard reading, currying supplies a related program transformation. The Haskell 2010 Prelude defines curry from a function of type (a,b) -> c to one of type a -> b -> c, and uncurry in the reverse direction. The pair corresponds to joint input and the returned function to a nested input. Lean explicitly compares conjunction with product types while distinguishing Prop from Type. Thus Haskell gives a second, typed setting for the role map, while the logical law remains specified by its formal connectives.^[1]^[2]

Replacement inside a longer propositional formula requires a suitable congruence or replacement principle in that host proof system. Exportation by itself identifies the two forms and their derivability; it does not grant unrestricted rewriting in intensional or undocumented contexts.^[1]

Clarity¶

Write the parentheses. Because \(\to\) associates to the right, \(P\to Q\to R\) means \(P\to(Q\to R)\), not \((P\to Q)\to R\). The left side is \((P\land Q)\to R\), not \(P\land(Q\to R)\). Keeping the same \(R\) and the same order of \(P\), \(Q\) prevents an accidental claim about converse or reordered implication.^[1]

Name the direction as well as the equivalence. Starting with the joint antecedent and obtaining the nested form is exportation; starting with the nested form and obtaining a joint-antecedent implication is importation. If the purpose is local replacement in a larger formula, separately identify the host formula and the system's permission to replace an equivalent subformula.

Manages Complexity¶

The law lets a proof handle two assumptions either as one conjunction or one at a time. From \(h:(P\land Q)\to R\), the sequential form is built by taking \(hp:P\) and \(hq:Q\), then applying \(h\) to their conjunction. This exposes the order in which assumptions are introduced without changing the final conclusion. Conversely, if the proof already has a nested implication, importation lets a conjunction be supplied as one input.^[1]

This compression has limits. It does not say that \(P\) causes \(Q\), that one assumption is more important, or that a change of proof interface improves runtime performance. The Haskell pair and curried functions have corresponding types and definitions, but the source does not establish a universal performance preference between them.^[2]

Abstract Reasoning¶

To use exportation, first identify a proved or assumed \((P\land Q)\to R\). Introduce \(P\) and then \(Q\). Conjoin their proofs and apply the original implication to derive \(R\); discharge \(Q\), then \(P\). The resulting proof has type \(P\to(Q\to R)\). Each step uses the formal rules of the declared logic, rather than an appeal to how an English conditional sounds.^[1]

For the reverse direction, take \(g:P\to(Q\to R)\) and a proof of \(P\land Q\). Extract its two conjuncts, apply \(g\) to the first and then the second, and obtain \(R\). The availability of both constructions explains the biconditional, while only the first construction is an exportation step.^[1]

Knowledge Transfer¶

The logical construction transfers to typed programming through the product/function correspondence: curry f x y = f (x,y) turns a pair-input function into one receiving inputs successively, and uncurry performs the inverse conversion. The mapping is precise at the interface: \(P,Q,R\) correspond to types a,b,c, conjunction to a pair type, and implication to a function type in the propositions-as-types interpretation.^[1]^[2]

The transfer has a boundary. A Haskell value of type a is not thereby a proof of an arbitrary proposition \(P\); the correspondence explains the shared structure of these conversions. A programming language's evaluation effects, partial functions, or optimization goals are further questions, not consequences of the import–export law as stated.^[1]^[2]

Examples¶

Lean propositional proof. Let \(h:(P\land Q)\to R\). With \(hp:P\) and \(hq:Q\), And.intro hp hq gives the paired premise; h (And.intro hp hq) gives \(R\). Abstracting first over \(hq\) and then \(hp\) yields \(P\to Q\to R\). Mapped roles: the formal setting is Lean's conjunction and implication; the input is \(h\); the nested output takes \(hp\) then \(hq\); the conversion uses conjunction introduction and function abstraction/application; \(P,Q,R\) keep their roles. This proof term is synthesized from the documented constructors and the listed validity.^[1]

Haskell typed function conversion. Given f :: (a,b) -> c, the Standard Prelude defines curry f x y = f (x,y). Mapped roles: a typed pair-function setting supplies the analogue; f takes the joint input; curry f has type a -> b -> c; curry performs the pair-to-sequential conversion; a,b,c retain their places. This is an executable product/function analogue, not a separate logical theorem about all conditionals.^[1]^[2]

Structural Tensions¶

The two equivalent formal expressions make different proof interfaces convenient: one accepts a conjunction, the other accepts assumptions in sequence. The cited sources do not establish an intrinsic opposed-pressure tradeoff or cost that every exportation instance must resolve. Choice of form depends on the proof or function being assembled; it should not be presented as a universal optimization law.^[1]^[2]

Structural–Framed Character¶

This entry is structural within formal logic. The same three proposition roles and the joint-to-nested conversion recur regardless of the particular propositions filling them. Its recognition does not depend on whether the conclusion is useful, surprising, or ethically desirable. The formal rules, not the subject matter of \(P\), \(Q\), and \(R\), determine whether the conversion is licensed.^[1]

Its human-practice dependence lies in the chosen formal language and proof conventions. Lean supplies one explicit system; Haskell supplies a related typed interface. Its institutional origin is the development and teaching of formal proof systems and language specifications: these communities choose notation and publish the rules, while the validity of the conversion is checkable once those rules are fixed. The vocabulary travels to programming through an explicit product/function correspondence. That transfer recognizes a mapped structure; it does not make an ordinary-language “if” or any arbitrary program rewrite a new literal instance. Its character: a formal equivalence with one named direction of conversion, bounded by the semantics of conjunction, implication, and typed analogy.^[1]^[2]

Structural Core vs. Domain Accent¶

The core is the exportation direction from \((P\land Q)\to R\) to \(P\to(Q\to R)\), with the same \(P,Q,R\) and formal rules that justify it. Delete the conjunction, change the consequent, or abandon the stated implication rules and the identity is lost. Lean proof syntax, the letters chosen for propositions, and Haskell's names curry/uncurry are accents or analogue vocabulary. Importation completes the equivalence but is not an operation each exportation instance must perform.^[1]^[2]

The live Logical Operation entry supplies a domain-level genus: typed input, declared formal rule, determinate output. Exportation adds this particular conjunction/implication pattern and preserved proposition roles, so the proposed edge is strict subsumption. The wider portable skeleton is already represented by the live Transformation Prime: an input is restructured by a rule while relevant invariants are preserved. Logical Operation is itself a strict child of that Prime in the live DAG. Exportation keeps formal conjunction and implication as its domain residual, so no new Prime is proposed here and a direct Prime edge would bypass the nearer typed parent.

This entry is a kind of Logical Operation.

Logical Operation — proposed strict subsumption parent. Joint-antecedent formula in, nested formula out, under a declared proof rule. Other logical operations need not export a premise.
Rule of Replacement — related, declined as parent. Exportation can be one equivalence schema used by a replacement rule. That live entry additionally requires a selected occurrence inside a larger host formula; the bare exportation law does not.
Material Conditional — related, declined as parent. It defines one arrow's classical truth condition. Exportation concerns the relation of compound formulas and also has an intuitionistic proof.
Equivalence-Preserving Rewriting — tested Prime neighbor, declined. Its live identity includes choosing among equivalent rewrites by an orthogonal cost criterion. Exportation need not make such a choice, so the Prime's full identity is not a strict parent here.

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 (89^th 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

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

Exportation takes \((P\land Q)\to R\) toward \(P\to(Q\to R)\); importation travels back. Neither is conjunction elimination alone, which extracts \(P\) or \(Q\) from a paired proof without changing the implication's packaging. Neither is unrestricted substitution: an equivalence can support local rewriting only under a host system's rules. Currying in typed programming shows a mapped product/function conversion, but its computational behavior and the logical theorem should be described at their respective levels.^[1]^[2]

References¶

[1] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y ↩z

[2] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j