Exportation (logic)

${\displaystyle ((P\wedge Q)\to R)\iff (P\to (Q\to R))}$

Where "${\displaystyle \iff }$" is a metalogical symbol representing "can be replaced in a proof with." In strict terminology, ${\displaystyle ((P\wedge Q)\to R)\Rightarrow (P\to (Q\to R))}$ is the law of exportation, for it "exports" a proposition from the antecedent of ${\displaystyle (P\wedge Q)\to R}$ to its consequent. Its converse, the law of importation, ${\displaystyle (P\to (Q\to R))\Rightarrow ((P\wedge Q)\to R)}$, "imports" a proposition from the consequent of ${\displaystyle P\to (Q\to R)}$ to its antecedent.

Formal notation

The exportation rule may be written in sequent notation:

${\displaystyle ((P\wedge Q)\to R)⊣<!--\; -->⊢(P\to (Q\to R))}$

where ${\displaystyle ⊣<!--\; -->⊢}$ is a metalogical symbol meaning that ${\displaystyle (P\to (Q\to R))}$ is a syntactic equivalent of ${\displaystyle ((P\wedge Q)\to R)}$ in some logical system;

or in rule form:

${\displaystyle \frac{(P\wedge Q)\to R}{P\to (Q\to R)}}$, ${\displaystyle \frac{P\to (Q\to R)}{(P\wedge Q)\to R}.}$

where the rule is that wherever an instance of "${\displaystyle (P\wedge Q)\to R}$" appears on a line of a proof, it can be replaced with "${\displaystyle P\to (Q\to R)}$", and vice versa.

Import-export is a name given to the statement as a theorem or truth-functional tautology of propositional logic:

${\displaystyle ((P\wedge Q)\to R)\leftrightarrow (P\to (Q\to R))}$

where ${\displaystyle P}$, ${\displaystyle Q}$, and ${\displaystyle R}$ are propositions expressed in some logical system.