Exportation (logic)

From Wikipedia, the free encyclopedia
Jump to: navigation, search

Exportation[1][2][3][4] is a valid rule of replacement in propositional logic. The rule allows conditional statements having conjunctive antecedents to be replaced by statements having conditional consequents and vice-versa in logical proofs. It is the rule that:

((P \and Q) \to R) \Leftrightarrow (P \to (Q \to R))

Where "\Leftrightarrow" is a metalogical symbol representing "can be replaced in a proof with."

Formal notation[edit]

The exportation rule may be written in sequent notation:

((P \and Q) \to R) \vdash (P \to (Q \to R))

where \vdash is a metalogical symbol meaning that (P \to (Q \to R)) is a syntactic consequence of ((P \and Q) \to R) in some logical system;

or in rule form:

\frac{(P \and Q) \to R}{P \to (Q \to R)}.

where the rule is that wherever an instance of "(P \and Q) \to R" appears on a line of a proof, it can be replaced with "P \to (Q \to R)";

or as the statement of a truth-functional tautology or theorem of propositional logic:

((P \and Q) \to R)) \to (P \to (Q \to R)))

where P, Q, and R are propositions expressed in some logical system.

Natural language[edit]

Truth values[edit]

At any time, if P→Q is true, it can be replaced by P→(P∧Q).
One possible case for P→Q is for P to be true and Q to be true; thus P∧Q is also true, and P→(P∧Q) is true.
Another possible case sets P as false and Q as true. Thus, P∧Q is false and P→(P∧Q) is false; false→false is true.
The last case occurs when both P and Q are false. Thus, P∧Q is false and P→(P∧Q) is true.


It rains and the sun shines implies that there is a rainbow.
Thus, if it rains, then the sun shines implies that there is a rainbow.

Relation to functions[edit]

Exportation is associated with Currying via the Curry–Howard correspondence.


  1. ^ Hurley, Patrick (1991). A Concise Introduction to Logic 4th edition. Wadsworth Publishing. pp. 364–5. 
  2. ^ Copi, Irving M.; Cohen, Carl (2005). Introduction to Logic. Prentice Hall. p. 371. 
  3. ^ Moore and Parker
  4. ^ http://www.philosophypages.com/lg/e11b.htm