# Exportation (logic)

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

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

### Truth values

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.

### Example

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

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

## References

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